The sphere eversion project #
The goal of this project was to formalize Gromov's flexibility theorem for open and ample partial differential relation. A famous corollary of this theorem is Smale's sphere eversion theorem: you can turn a sphere inside-out. Let us state this corollary first.
Equations
- «termℝ³» = Lean.ParserDescr.node `«termℝ³» 1024 (Lean.ParserDescr.symbol "ℝ³")
Instances For
Equations
- «term𝕊²» = Lean.ParserDescr.node `«term𝕊²» 1024 (Lean.ParserDescr.symbol "𝕊²")
Instances For
theorem
Smale :
∃ (f : ℝ → ↑(Metric.sphere 0 1) → ℝ³),
ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (ℝ^2))) (modelWithCornersSelf ℝ ℝ³) ↑⊤ ↿f ∧ (f 0 = fun (x : ↑(Metric.sphere 0 1)) => ↑x) ∧ (f 1 = fun (x : ↑(Metric.sphere 0 1)) => -↑x) ∧ ∀ (t : ℝ), Immersion (modelWithCornersSelf ℝ (ℝ^2)) (modelWithCornersSelf ℝ ℝ³) (f t) ↑⊤
theorem
Gromov
(n n' d : ℕ)
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (ℝ^n) M]
[IsManifold (modelWithCornersSelf ℝ (ℝ^n)) (↑⊤) M]
[T2Space M]
[SigmaCompactSpace M]
{M' : Type u_2}
[MetricSpace M']
[ChartedSpace (ℝ^n') M']
[IsManifold (modelWithCornersSelf ℝ (ℝ^n')) (↑⊤) M']
[SigmaCompactSpace M']
{P : Type u_3}
[TopologicalSpace P]
[ChartedSpace (ℝ^d) P]
[IsManifold (modelWithCornersSelf ℝ (ℝ^d)) (↑⊤) P]
[T2Space P]
[SigmaCompactSpace P]
{R : RelMfld (modelWithCornersSelf ℝ (ℝ^n)) M (modelWithCornersSelf ℝ (ℝ^n')) M'}
(hRample : R.Ample)
(hRopen : IsOpen R)
{C : Set (P × M)}
(hC : IsClosed C)
{ε : M → ℝ}
(ε_pos : ∀ (x : M), 0 < ε x)
(ε_cont : Continuous ε)
(𝓕₀ : FamilyFormalSol (modelWithCornersSelf ℝ (ℝ^d)) P R)
(hhol : ∀ᶠ (p : P × M) in nhdsSet C, (𝓕₀ p.1).IsHolonomicAt p.2)
:
∃ (𝓕 : FamilyFormalSol ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (ℝ^d))) (ℝ × P) R),
(∀ (p : P) (x : M), (𝓕 (0, p)) x = (𝓕₀ p) x) ∧ (∀ (p : P), (𝓕 (1, p)).IsHolonomic) ∧ (∀ᶠ (p : P × M) in nhdsSet C, ∀ (t : ℝ), (𝓕 (t, p.1)) p.2 = (𝓕₀ p.1) p.2) ∧ ∀ (t : ℝ) (p : P) (x : M), dist ((𝓕 (t, p)).bs x) ((𝓕₀ p).bs x) ≤ ε x
Gromov's flexibility theorem for open and ample first order partial differential relations for maps between manifolds.