OAI/Geometry/Arnold/Hessian.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArnoldCounterexample.ThreePoints.ambientHessian line 13
2. lemma OAI.ArnoldCounterexample.ThreePoints.ambientHessian_apply line 21
3. lemma OAI.ArnoldCounterexample.ThreePoints.df_eq_affine line 26
4. lemma OAI.ArnoldCounterexample.ThreePoints.df_hasFDerivAt line 33
5. lemma OAI.ArnoldCounterexample.ThreePoints.f_secondFDeriv line 39
6. lemma OAI.ArnoldCounterexample.ThreePoints.df_qzero line 45
7. def OAI.ArnoldCounterexample.ThreePoints.IsTangent line 51

   Source documentation

   The full tangent in the two ambient factors.

   def IsTangent (q r : Pair) : Prop := q.1 ⬝ᵥ r.1 = 0 ∧ q.2 ⬝ᵥ r.2 = 0

   Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair

8. lemma OAI.ArnoldCounterexample.ThreePoints.tangent_qzero_iff line 53
9. lemma OAI.ArnoldCounterexample.ThreePoints.ambientHessian_at_qzero_on_tangent line 56
10. theorem OAI.ArnoldCounterexample.ThreePoints.qzero_degenerate_hessian line 65

    Source documentation

    There is a genuine nonzero tangent in the kernel of the Hessian at q0.

    theorem qzero_degenerate_hessian :
        ∃ r : Pair, r ≠ 0 ∧ IsTangent qzero r ∧
          ∀ s : Pair, IsTangent qzero s → fderiv ℝ (fderiv ℝ f) qzero r s = 0 := by
    …

    Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair, OAI.ArnoldCounterexample.ThreePoints.IsTangent, OAI.ArnoldCounterexample.ThreePoints.qzero, OAI.ArnoldCounterexample.ThreePoints.f

11. def OAI.ArnoldCounterexample.ThreePoints.tangentCoordinates line 81

    Source documentation

    In coordinates (u,v,a,b) on the tangent the Hessian is va'+av'.

    def tangentCoordinates (w : Fin 4 → ℝ) : Pair :=
    …

    Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair

12. lemma OAI.ArnoldCounterexample.ThreePoints.tangentCoordinates_mem line 84
13. lemma OAI.ArnoldCounterexample.ThreePoints.hessian_tangentCoordinates line 88
14. lemma OAI.ArnoldCounterexample.ThreePoints.tangent_hessian_kernel line 95