Revision #2415 → #3562 · back to history
modifiedSchwarzian derivative (complex)b543d81ff517
| Field | From #2415 | To #3562 |
|---|
| note | No Schwarzian derivative definition appears in Mathlib4 (grep for 'Schwarzian' returns no files). | Grep for 'Schwarzian' in Mathlib returns no files, so no such definition exists. |
modifiedSchwarzian derivative (real C^3)ff8f67d0ef87
| Field | From #2415 | To #3562 |
|---|
| note | No real-variable Schwarzian derivative is defined in Mathlib4. | No real-variable Schwarzian derivative appears in Mathlib (grep 'Schwarzian' empty). |
modifiedMöbius transformations characterized by vanishing Schwarzian664823e9e135
| Field | From #2415 | To #3562 |
|---|
| note | No Schwarzian characterization of Möbius maps in Mathlib4. | No Schwarzian-based characterization of Möbius maps in Mathlib. |
modifiedChain rule for Schwarzian derivative830caf9bcf31
| Field | From #2415 | To #3562 |
|---|
| note | No Schwarzian derivative and so no chain rule for it in Mathlib4. | No Schwarzian derivative, so no chain rule for it in Mathlib. |
modifiedSign of Schwarzian preserved under iteration31922a6e9714
| Field | From #2415 | To #3562 |
|---|
| note | Not present in Mathlib4. | Not present in Mathlib (no Schwarzian defined). |
modifiedAuxiliary function of two complex variablesd21bf809eb8c
| Field | From #2415 | To #3562 |
|---|
| note | This Schwarzian-related auxiliary function is not defined in Mathlib4. | This Schwarzian-related auxiliary function is not defined in Mathlib. |
addedSchwarzian via second mixed partial derivativea9d384a92e53
modifiedInversion formula for the Schwarzian502732f5ab01
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized; no Schwarzian in Mathlib4. | Not formalized; no Schwarzian in Mathlib. |
modifiedThurston's geometric interpretation433f7a39383b
| Field | From #2415 | To #3562 |
|---|
| note | Thurston's interpretation is not in Mathlib4. | Thurston's interpretation is not in Mathlib. |
modifiedImage of circle under conformal map92b4de4eb6a0
| Field | From #2415 | To #3562 |
|---|
| note | Not present in Mathlib4. | Not present in Mathlib. |
modifiedCross-ratio transformation and Möbius invariance87df3c65f3f8
| Field | From #2415 | To #3562 |
|---|
| note | No cross-ratio definition or Möbius invariance lemma found in Mathlib4. | No cross-ratio definition or Möbius invariance lemma found in Mathlib (grep 'crossRatio' empty). |
modifiedLinear second-order ODE associated to Schwarzian555849fdad46
| Field | From #2415 | To #3562 |
|---|
| note | This specific ODE setup is not formalized in Mathlib4. | This specific ODE setup is not formalized in Mathlib. |
modifiedSchwarzian of evaluation kernel equals coefficient411fcd2b1fa4
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedEqual Schwarzians implies fractional linear relationd23d2df64178
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedRatio of solutions satisfies Schwarzian equatione94258ac0666
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedConverse: holomorphic g determines pair of solutionsb2690b77d50e
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedQ-value of a second-order ODEe2d4692c47f0
| Field | From #2415 | To #3562 |
|---|
| note | Q-value terminology is not defined in Mathlib4. | Q-value terminology is not defined in Mathlib. |
modifiedGaussian hypergeometric ODEf8b49c8a45e4
| Field | From #2415 | To #3562 |
|---|
| note | Mathlib has the hypergeometric series (`ordinaryHypergeometric`) but not the associated ODE in Schwarzian form. | Mathlib has the hypergeometric series (`ordinaryHypergeometric`, verified) but not the associated ODE in Schwarzian form. |
modifiedKraus–Nehari necessary condition for univalenceb67988483f25
| Field | From #2415 | To #3562 |
|---|
| note | No Kraus–Nehari univalence bound in Mathlib4. | No Kraus–Nehari univalence bound in Mathlib (grep 'Nehari' empty). |
modifiedNehari sufficient condition for univalence6bb41a066ce5
| Field | From #2415 | To #3562 |
|---|
| note | Nehari's sufficient univalence condition is not formalized in Mathlib4. | Nehari's sufficient univalence condition is not formalized in Mathlib. |
modifiedParticular sufficient condition for univalence3f03a31cc998
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedConformal map from Schwarzian to circular-arc polygon77002d220d3d
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedSchwarzian extends to rational function with double polescb72d56babae
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedAccessory parameters8ff1f1cf2010
| Field | From #2415 | To #3562 |
|---|
| note | Accessory parameters are not defined in Mathlib4. | Accessory parameters are not defined in Mathlib. |
modifiedTriangle case (Schwarz triangle function)a82fce92321c
| Field | From #2415 | To #3562 |
|---|
| note | Schwarz triangle function is not in Mathlib4. | Schwarz triangle function is not in Mathlib. |
modifiedQuadrilateral case as Sturm–Liouvillec3d68c9fa6bf
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4; no Sturm–Liouville theory either. | Not in Mathlib; no Sturm–Liouville theory either. |
modifiedLowest-eigenvalue condition via Sturm separation9be6d953995c
| Field | From #2415 | To #3562 |
|---|
| note | Sturm separation theorem is not in Mathlib4. | Sturm separation theorem is not in Mathlib. |
modifiedUniversal Teichmüller spaceb4074767096d
| Field | From #2415 | To #3562 |
|---|
| note | Mathlib's 'Teichmuller' files concern Witt vectors, not Teichmüller spaces. | Mathlib's 'Teichmuller' files concern Witt vectors and Teichmüller–Tukey, not Teichmüller spaces of Riemann surfaces. |
addedBeltrami differential equation6a4f4c607771
modifiedBers embedding via Schwarziana09b03796319
| Field | From #2415 | To #3562 |
|---|
| note | Bers embedding is not in Mathlib4. | Bers embedding is not in Mathlib. |
modifiedGehring's characterization of the Bers image88b28aad4e21
| Field | From #2415 | To #3562 |
|---|
| note | Gehring's theorem is not formalized in Mathlib4. | Gehring's theorem is not formalized in Mathlib. |
modifiedTeichmüller space of compact surface as quadratic differentials4d06ef5e850f
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedSchwarzian as 1-cocycle of Diff(S^1)3084b7982d83
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedVanishing of higher cohomology for compact group action6e3429cf373e
| Field | From #2415 | To #3562 |
|---|
| note | Continuous cohomology vanishing for compact groups on topological vector spaces is not in Mathlib4. | Continuous cohomology vanishing for compact groups on topological vector spaces is not in Mathlib. |
modifiedInfinitesimal 1-cocycle on Vect(S^1)081140f96ec2
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedUniqueness of non-zero 1-cocycle solution7fe2f1b9e008
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedVirasoro algebra as central extension042f6c56de4c
| Field | From #2415 | To #3562 |
|---|
| note | Virasoro algebra is not in Mathlib4. | Virasoro algebra is not in Mathlib (grep 'Virasoro' empty). |
modifiedQuasisymmetric homeomorphisms from quasiconformal self-maps73bce0c2fd89
| Field | From #2415 | To #3562 |
|---|
| note | Quasiconformal/quasisymmetric theory is absent from Mathlib4. | Quasiconformal/quasisymmetric theory is absent from Mathlib (grep empty). |
modifiedDual of Lie algebra as Hill's operatorsb2abee7296dc
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedSchwarzian in coadjoint action of Diff(S^1)fd532277b666
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedHolomorphic pseudogroup3ea60eee2d2b
| Field | From #2415 | To #3562 |
|---|
| note | Holomorphic pseudogroups are not defined in Mathlib4. | Holomorphic pseudogroups are not defined in Mathlib. |
modifiedPseudogroup defined by differential equations7e91228095f6
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedClassification of flat pseudogroups via affine/Möbiusaf96d2b3dc27
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedSchwarzian as 1-cocycle for biholomorphism pseudogroupb7aa439c8a75
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedAffine and projective structures on Riemann surfaces394c3aed4671
| Field | From #2415 | To #3562 |
|---|
| note | Affine/projective structures on Riemann surfaces are not formalized in Mathlib4. | Affine/projective structures on Riemann surfaces are not formalized in Mathlib. |
modifiedGunning's projective connection result1761b9c7460e
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedOsgood–Stowe Schwarzian on conformal manifoldsbec6b07d2077
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedCocycle law for conformal-manifold Schwarzianac4392b24183
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedMöbius transformations have vanishing Schwarzian conformal factor04ac46d651e8
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |
modifiedSolutions of Schwarzian equation on Euclidean space16680a1f79d7
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedLagrangian Schwarzian for positive curvesd905acda20b3
| Field | From #2415 | To #3562 |
|---|
| note | Lagrangian Grassmannian and Lagrangian Schwarzian are not defined in Mathlib4. | Lagrangian Grassmannian and Lagrangian Schwarzian are not defined in Mathlib. |
modifiedVanishing Lagrangian Schwarzian characterizes symplectic equivalencec50fbfc62574
| Field | From #2415 | To #3562 |
|---|
| note | Not in Mathlib4. | Not in Mathlib. |
modifiedLagrangian Schwarzian via second-order ODE0fdc992c40b9
| Field | From #2415 | To #3562 |
|---|
| note | Not formalized in Mathlib4. | Not formalized in Mathlib. |