Deformation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ArnoldCounterexample.CriticalBound.unit_phase line 15
lemma OAI.ArnoldCounterexample.CriticalBound.project_phase line 21
lemma OAI.ArnoldCounterexample.CriticalBound.project_eq_phase line 26
lemma OAI.ArnoldCounterexample.CriticalBound.extension_phase line 34
lemma OAI.ArnoldCounterexample.CriticalBound.local_lift_derivative_eq line 42
Source documentation
Every local lift has the same horizontal derivative as a global extension; this follows from the explicit curves in the actual quadric.
```
lemma local_lift_derivative_eq {h : Q3 → ℝ} {G : CV → ℝ}
    (hG : ContDiff ℝ ∞ G) (hGagree : ∀ z : UnitQuadric, G z = h (project z))
    (z : UnitQuadric) (U : Set CV) (g : CV → ℝ)
    (hg : LocalFunctionLift h z U g) (v : CV) (hv : Horizontal z v) :
    fderiv ℝ g z v = fderiv ℝ G z v := by
…
```
Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.project, OAI.ArnoldCounterexample.LocalFunctionLift, OAI.ArnoldCounterexample.Horizontal
lemma OAI.ArnoldCounterexample.CriticalBound.stationary_isCritical line 63
theorem OAI.ArnoldCounterexample.CriticalBound.exists_smooth_descent line 83
Source documentation
Smooth phase-equivariant, strictly descending discrete deformation of the literal quadric. This supplies the deformation step for arbitrary smooth functions, including highly degenerate ones, without assuming an ODE existence theorem.
```
theorem exists_smooth_descent {h : Q3 → ℝ} {G : CV → ℝ}
    (hG : ContDiff ℝ ∞ G) (hGagree : ∀ z : UnitQuadric, G z = h (project z)) :
    ∃ D : CV → CV, ContDiff ℝ ∞ D ∧
      (∀ z : UnitQuadric, IsUnitQuadric (D z)) ∧
      (∀ z : UnitQuadric, ∀ a : ℂ, Complex.normSq a = 1 → D (a • (z : CV)) = a • D z) ∧
      (∀ z : UnitQuadric, G (D z) ≤ G z) ∧
      (∀ z : UnitQuadric, G (D z) = G z → IsCritical h (project z)) := by
…
```
Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.project, OAI.ArnoldCounterexample.IsUnitQuadric, OAI.ArnoldCounterexample.IsCritical
lemma OAI.ArnoldCounterexample.CriticalBound.critical_chart line 117
lemma OAI.ArnoldCounterexample.CriticalBound.contDiff_iterate line 133
lemma OAI.ArnoldCounterexample.CriticalBound.iterate_preserves line 139
lemma OAI.ArnoldCounterexample.CriticalBound.iterate_phase line 146
theorem OAI.ArnoldCounterexample.CriticalBound.cover_map line 158
Source documentation
Three or fewer critical points yield three nonvanishing-coordinate descent charts, on the literal quadric, with no Morse or nondegeneracy hypotheses.
```
theorem cover_map (h : SmoothFunction) (hsmall : (criticalSet h).encard ≤ 3) :
    ∃ F : CV → CSpace 3, ContDiff ℝ ∞ F ∧
      (∀ z : UnitQuadric, F z ≠ 0) ∧
      (∀ z : UnitQuadric, ∀ a : ℂ, Complex.normSq a = 1 → F (a • (z : CV)) = a • F z) := by
…
```
Mentions: OAI.ArnoldCounterexample.SmoothFunction, OAI.ArnoldCounterexample.criticalSet, OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric

theorem OAI.ArnoldCounterexample.CriticalBound.normalize_cover_map line 217

Source documentation

Normalization has a globally smooth ambient extension, even away from K. The positive complement bump prevents spurious singularities off K.

theorem normalize_cover_map {F : CV → CSpace 3} (hF : ContDiff ℝ ∞ F)
    (hne : ∀ z : UnitQuadric, F z ≠ 0)
    (hphase : ∀ z : UnitQuadric, ∀ a : ℂ, Complex.normSq a = 1 → F (a • (z : CV)) = a • F z) :
    ∃ F' : CV → CSpace 3, ContDiff ℝ ∞ F' ∧
      (∀ z : UnitQuadric, normSq 3 (F' z) = 1) ∧
      (∀ z : UnitQuadric, ∀ a : ℂ, Complex.normSq a = 1 → F' (a • (z : CV)) = a • F' z) := by
…

Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric