OAI/Geometry/Arnold/Volume.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArnoldCounterexample.CriticalBound.haar_homotopy_invariant line 23

   Source documentation

   The Haar integral of a closed horizontal cylinder form is independent of its slice. The bracket condition is algebraic.

   theorem haar_homotopy_invariant
       (Θ : ℝ × RM → (ℝ × RM) [⋀^Fin 6]→L[ℝ] ℝ)
       (hΘ : ContDiff ℝ ∞ Θ) (hclosed : ∀ p, extDeriv Θ p = 0)
       (hvertical : ∀ (t : ℝ) (A : O5) (i j : Fin 5),
         sliceContraction Θ t A
           (Matrix.vecCons ((A : RM) * (generators i.castSucc * generators j.succ -
             generators j.succ * generators i.castSucc))
             (j.removeNth (i.castSucc.removeNth (fun k ↦ (A : RM) * generators k)))) = 0)
       (a b : ℝ) :
       (∫ A : O5, Θ (a, A) (fun i ↦ (0, (A : RM) * generators i)) ∂haar) =
       (∫ A : O5, Θ (b, A) (fun i ↦ (0, (A : RM) * generators i)) ∂haar) := by
   …

   Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CriticalBound.O5, OAI.ArnoldCounterexample.CriticalBound.generators, OAI.ArnoldCounterexample.CriticalBound.haar

2. lemma OAI.ArnoldCounterexample.CriticalBound.symplectic_velocities line 76
3. lemma OAI.ArnoldCounterexample.CriticalBound.cubeForm_velocities line 84
4. abbrev OAI.ArnoldCounterexample.Forms.ProductSpace line 94
5. def OAI.ArnoldCounterexample.Forms.productSymplectic line 96
6. lemma OAI.ArnoldCounterexample.Forms.productSymplectic_apply line 100
7. lemma OAI.ArnoldCounterexample.Forms.productSymplectic_skew line 103
8. def OAI.ArnoldCounterexample.Forms.productNormSq line 109
9. lemma OAI.ArnoldCounterexample.Forms.productNormSq_contDiff line 111
10. lemma OAI.ArnoldCounterexample.Forms.productNormSq_fderiv line 114
11. lemma OAI.ArnoldCounterexample.Forms.productNormSq_curve_orthogonal line 126
12. lemma OAI.ArnoldCounterexample.Forms.normSq_real_smul line 137
13. lemma OAI.ArnoldCounterexample.Forms.fderiv_circle_equivariant line 144

    Source documentation

    Differentiating honest circle equivariance, rather than assuming its infinitesimal consequence.

    lemma fderiv_circle_equivariant {m n : ℕ} (F : CSpace m → CSpace n)
        (hF : Differentiable ℝ F) (z : CSpace m)
        (hphase : ∀ a : ℂ, Complex.normSq a = 1 → F (a • z) = a • F z) :
        fderiv ℝ F z (Complex.I • z) = Complex.I • F z := by
    …

    Mentions: OAI.ArnoldCounterexample.Forms.CSpace

14. lemma OAI.ArnoldCounterexample.Forms.time_slice_hasDerivAt line 166
15. lemma OAI.ArnoldCounterexample.Forms.productNormSq_time_tangent line 173
16. lemma OAI.ArnoldCounterexample.Forms.alternating_eq_zero_on_kernel line 185
17. lemma OAI.ArnoldCounterexample.Forms.six_form_vanishes_on_unit_sphere line 206

    Source documentation

    Six tangent vectors of the unit five-sphere are necessarily dependent.

    lemma six_form_vanishes_on_unit_sphere
        (θ : CSpace 3 [⋀^Fin 6]→L[ℝ] ℝ) (z : CSpace 3) (hz : normSq 3 z = 1)
        (v : Fin 6 → CSpace 3) (hv : ∀ i, fderiv ℝ (normSq 3) z (v i) = 0) :
        θ v = 0 := by
    …

    Mentions: OAI.ArnoldCounterexample.Forms.CSpace, OAI.ArnoldCounterexample.Forms.normSq

18. lemma OAI.ArnoldCounterexample.Forms.cubeForm_second_radical_on line 226