OAI/Geometry/Arnold/Tangent.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArnoldCounterexample.Quadric.normSquaredDiff line 10
2. lemma OAI.ArnoldCounterexample.Quadric.normSquared_hasFDerivAt line 13
3. lemma OAI.ArnoldCounterexample.Quadric.normSquaredDiff_apply line 23
4. lemma OAI.ArnoldCounterexample.Quadric.normSquared_smooth line 36
5. lemma OAI.ArnoldCounterexample.Quadric.quadricPolynomial_smooth line 41
6. def OAI.ArnoldCounterexample.Quadric.normalize line 46

   Source documentation

   Normalizing a nonzero isotropic vector gives a legitimate unit representative.

   def normalize (w : CV) : CV := (Real.sqrt (normSquared w))⁻¹ • w

   Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.normSquared

7. lemma OAI.ArnoldCounterexample.Quadric.normalize_unit line 48
8. lemma OAI.ArnoldCounterexample.Quadric.normalize_unit_self line 60
9. def OAI.ArnoldCounterexample.Quadric.rawTangentCurve line 64

   Source documentation

   A polynomial curve on the nonzero isotropic cone realizing a horizontal vector.

   def rawTangentCurve (z v : CV) (t : ℝ) : CV :=
   …

   Mentions: OAI.ArnoldCounterexample.CV

10. lemma OAI.ArnoldCounterexample.Quadric.rawTangentCurve_eq line 67
11. lemma OAI.ArnoldCounterexample.Quadric.rawTangentCurve_zero line 75
12. lemma OAI.ArnoldCounterexample.Quadric.rawTangentCurve_hasDerivAt_zero line 78
13. lemma OAI.ArnoldCounterexample.Quadric.rawTangentCurve_ne_zero line 86
14. lemma OAI.ArnoldCounterexample.Quadric.rawTangentCurve_polynomial line 91
15. def OAI.ArnoldCounterexample.Quadric.tangentCurve line 97

    Source documentation

    A genuine curve in the unit cone, not an assumed tangent parametrization.

    def tangentCurve (z : UnitQuadric) (v : CV) (hv : Horizontal z v) (t : ℝ) : UnitQuadric :=
    …

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

16. lemma OAI.ArnoldCounterexample.Quadric.tangentCurve_zero line 101
17. theorem OAI.ArnoldCounterexample.Quadric.tangentCurve_hasDerivAt_zero line 108

    Source documentation

    Every declared horizontal tangent is realized by an actual differentiable curve in the literal unit isotropic cone.

    theorem tangentCurve_hasDerivAt_zero (z : UnitQuadric) (v : CV) (hv : Horizontal z v) :
        HasDerivAt (fun t ↦ (tangentCurve z v hv t : CV)) v 0 := by
    …

    Mentions: OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.Horizontal, OAI.ArnoldCounterexample.Quadric.tangentCurve

18. theorem OAI.ArnoldCounterexample.Quadric.smoothFunction_continuous_pullback line 129

    Source documentation

    Smoothness in the local-lift definition implies actual continuity on the compact unit cone. No topology on a substitute finite model is used.

    theorem smoothFunction_continuous_pullback {h : Q3 → ℝ} (hh : IsSmoothFunction h) :
        Continuous (h ∘ project) := by
    …

    Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.IsSmoothFunction, OAI.ArnoldCounterexample.project

19. theorem OAI.ArnoldCounterexample.Quadric.isCritical_of_global_min line 143

    Source documentation

    The criticality definition is nonvacuous: every global minimum is critical with respect to every local ambient lift.

    theorem isCritical_of_global_min {h : Q3 → ℝ} {q : Q3}
        (hmin : ∀ r, h q ≤ h r) : IsCritical h q := by
    …

    Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.IsCritical

20. theorem OAI.ArnoldCounterexample.Quadric.isClosed_unitQuadric line 167
21. lemma OAI.ArnoldCounterexample.Quadric.unitQuadric_norm_le line 171
22. theorem OAI.ArnoldCounterexample.Quadric.isCompact_unitQuadric line 181

    Source documentation

    Compactness of the literal unit cone, obtained from finite-dimensional Heine--Borel and the exact polynomial constraints.

    theorem isCompact_unitQuadric : IsCompact {z : CV | IsUnitQuadric z} := by
    …

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.IsUnitQuadric

23. instance OAI.ArnoldCounterexample.Quadric.unitQuadric_compactSpace line 186
24. def OAI.ArnoldCounterexample.Quadric.baseVector line 189
25. lemma OAI.ArnoldCounterexample.Quadric.baseVector_ne_zero line 191
26. lemma OAI.ArnoldCounterexample.Quadric.baseVector_polynomial line 196
27. def OAI.ArnoldCounterexample.Quadric.basePoint line 200
28. instance OAI.ArnoldCounterexample.Quadric.unitQuadric_nonempty line 203
29. theorem OAI.ArnoldCounterexample.Quadric.criticalSet_nonempty line 206

    Source documentation

    Every smooth function on the actual quadric attains a critical minimum.

    theorem criticalSet_nonempty (h : SmoothFunction) : (criticalSet h).Nonempty := by
    …

    Mentions: OAI.ArnoldCounterexample.SmoothFunction, OAI.ArnoldCounterexample.criticalSet