Topological sphere theorem (Berger–Klingenberg–Rauch)

sphere_theorem_topological

Submitter: Kim Morrison.

Notes: A closed, simply-connected, strictly quarter-pinched (sectional curvature in (1,4]) smooth Riemannian d-manifold (d ≥ 2) is homeomorphic to the standard d-sphere. Trusted helpers IsMetricCompatible, curv (Riemann curvature tensor), QuarterPinched (non-holes); following §38 the Levi-Civita connection is hypothesized as a smooth torsion-free metric-compatible covariant derivative (Mathlib has the interface but does not construct Levi-Civita). Mathlib has no Riemann/sectional curvature or pinching. Candidate from §121 of the Knill survey.

Source: M. Berger; W. Klingenberg; H. E. Rauch (topological sphere theorem, 1951–1961). Knill, *Some fundamental theorems in mathematics*, §121.

Informal solution: Classical sphere theorem via Toponogov/Klingenberg. From strict quarter-pinching, Klingenberg's injectivity-radius estimate gives inj(M) ≥ π/√(max K). Cover M by two metric balls around a point and its farthest point; Toponogov's triangle comparison shows each is a disk and they glue along a sphere, exhibiting M as a twisted sphere, hence homeomorphic to Sᵈ (Brown's theorem / Reeb). Needs the curvature comparison geometry (Toponogov, Rauch, Klingenberg injectivity radius) absent from Mathlib.

theorem declaration uses `sorry`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 ≃ₜ 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 ≃ₜ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.