Differentiable sphere theorem (Brendle–Schoen)

sphere_theorem_differentiable

Submitter: Kim Morrison.

Notes: Under the same hypotheses as the topological sphere theorem (closed, simply-connected, strictly quarter-pinched, d ≥ 2), the manifold is diffeomorphic to the standard d-sphere (Brendle–Schoen 2007, via Ricci flow). Shares the §121 trusted helpers (IsMetricCompatible, curv, QuarterPinched). Mathlib has no Ricci flow or curvature. Candidate from §121 of the Knill survey (additional 1).

Source: S. Brendle & R. Schoen, *Manifolds with 1/4-pinched curvature are space forms*, J. AMS 22 (2009). Knill, *Some fundamental theorems in mathematics*, §121.

Informal solution: Brendle–Schoen via Hamilton's Ricci flow. Run the normalized Ricci flow ġ = −2Ric(g) + (2/d)r̄ g from the quarter-pinched metric. The key analytic input is that the strict quarter-pinching condition (more precisely, nonnegative isotropic curvature on M × ℝ²) is preserved by the flow (Brendle–Schoen's curvature-pinching estimates via the maximum principle for the curvature-tensor reaction–diffusion equation), and the flow converges, after rescaling, to a constant-curvature round metric. Hence M is diffeomorphic to the round sphere. Requires Ricci flow and the pinching-preservation estimates, none in Mathlib.

theorem declaration uses `sorry`differentiable_sphere_theorem [I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
    (hdim : 2 ≤ Module.finrank ℝ E)
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : LeanEval.Geometry.SphereTheorem.IsMetricCompatible cov)
    (_hpinch : LeanEval.Geometry.SphereTheorem.QuarterPinched cov) :
    Nonempty
      (M ≃ₘ⟮I, 𝓡 (Module.finrank ℝ E)⟯
        (sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1)) := byE:Type u_1inst✝¹⁴:NormedAddCommGroup Einst✝¹³:NormedSpace ℝ Einst✝¹²:FiniteDimensional ℝ Einst✝¹¹:CompleteSpace EH:Type u_2inst✝¹⁰:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁹:TopologicalSpace Minst✝⁸:ChartedSpace H Minst✝⁷:IsManifold I ∞ Minst✝⁶:RiemannianBundle fun x => TangentSpace I xinst✝⁵:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xinst✝⁴:I.Boundarylessinst✝³:T2Space Minst✝²:CompactSpace Minst✝¹:SimplyConnectedSpace Mhdim:2 ≤ Module.finrank ℝ Ecov:CovariantDerivative I E (TangentSpace I)inst✝:cov.ContMDiffCovariantDerivative ∞_htor:cov.torsion = 0_hmet:IsMetricCompatible cov_hpinch:QuarterPinched cov⊢ Nonempty (M ≃ₘ⟮I, 𝓡 Module.finrank ℝ E⟯ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.