OAI/Geometry/Arnold/Orbit.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.CriticalBound.complexMat line 16

    Source documentation

    Complexification of a real matrix, with the actual complex-linear action.

    def complexMat (A : RM) : Matrix (Fin 5) (Fin 5) ℂ := A.map Complex.ofReal

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM

  2. def OAI.ArnoldCounterexample.CriticalBound.act line 18
  3. lemma OAI.ArnoldCounterexample.CriticalBound.complexMat_mul line 20
  4. lemma OAI.ArnoldCounterexample.CriticalBound.complexMat_star line 24
  5. lemma OAI.ArnoldCounterexample.CriticalBound.complexMat_one line 28
  6. lemma OAI.ArnoldCounterexample.CriticalBound.act_mul line 32
  7. lemma OAI.ArnoldCounterexample.CriticalBound.act_smul line 35
  8. lemma OAI.ArnoldCounterexample.CriticalBound.act_sub_left line 38
  9. lemma OAI.ArnoldCounterexample.CriticalBound.act_preserves_hermitian line 42
  10. lemma OAI.ArnoldCounterexample.CriticalBound.omega_act line 52
  11. def OAI.ArnoldCounterexample.CriticalBound.rotGen line 57

    Source documentation

    Elementary skew matrix rotating the (a,b) coordinate plane.

    def rotGen (a b : Fin 5) : RM := Matrix.single b a 1 - Matrix.single a b 1

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM

  12. lemma OAI.ArnoldCounterexample.CriticalBound.rotGen_skew line 59
  13. lemma OAI.ArnoldCounterexample.CriticalBound.rotGen_act line 63
  14. def OAI.ArnoldCounterexample.CriticalBound.baseScale line 79
  15. lemma OAI.ArnoldCounterexample.CriticalBound.baseScale_sq line 81
  16. lemma OAI.ArnoldCounterexample.CriticalBound.baseScale_pos line 83
  17. def OAI.ArnoldCounterexample.CriticalBound.base line 85
  18. lemma OAI.ArnoldCounterexample.CriticalBound.base_unit line 87
  19. def OAI.ArnoldCounterexample.CriticalBound.generators line 94
  20. def OAI.ArnoldCounterexample.CriticalBound.velocities line 97
  21. lemma OAI.ArnoldCounterexample.CriticalBound.generators_skew line 102
  22. lemma OAI.ArnoldCounterexample.CriticalBound.generators_base line 105
  23. def OAI.ArnoldCounterexample.CriticalBound.bracketCoefficient line 108
  24. lemma OAI.ArnoldCounterexample.CriticalBound.generators_bracket_base line 116
  25. lemma OAI.ArnoldCounterexample.CriticalBound.act_add_left line 129
  26. lemma OAI.ArnoldCounterexample.CriticalBound.act_real_smul_left line 133
  27. def OAI.ArnoldCounterexample.CriticalBound.orbitProjection line 143

    Source documentation

    The orbit map at the literal unit isotropic vector, extended linearly.

    def orbitProjection : RM →L[ℝ] CV :=
…

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CV

  28. lemma OAI.ArnoldCounterexample.CriticalBound.orbitProjection_apply line 148
  29. lemma OAI.ArnoldCounterexample.CriticalBound.act_star line 150
  30. lemma OAI.ArnoldCounterexample.CriticalBound.act_preserves_bilinear line 154
  31. lemma OAI.ArnoldCounterexample.CriticalBound.act_preserves_quadricPolynomial line 158
  32. lemma OAI.ArnoldCounterexample.CriticalBound.normSquared_eq_re line 162
  33. lemma OAI.ArnoldCounterexample.CriticalBound.act_preserves_normSquared line 165
  34. lemma OAI.ArnoldCounterexample.CriticalBound.act_unit line 169
  35. lemma OAI.ArnoldCounterexample.CriticalBound.orbitProjection_unit line 173
  36. def OAI.ArnoldCounterexample.CriticalBound.IsBasic line 177

    Source documentation

    A basic form annihilates the genuine circle-fiber direction.

    def IsBasic {n : ℕ} (η : CV → CV [⋀^Fin (n + 1)]→L[ℝ] ℝ) : Prop :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  37. theorem OAI.ArnoldCounterexample.CriticalBound.integral_extDeriv_basic_eq_zero line 183

    Source documentation

    Stokes evaluation for basic 5-forms on Q^3, proved by Haar integration rather than assuming a manifold integration or cohomology theorem.

    theorem integral_extDeriv_basic_eq_zero
    (η : CV → CV [⋀^Fin 5]→L[ℝ] ℝ) (hη : ContDiff ℝ ∞ η) (hbasic : IsBasic η) :
    ∫ A : O5, extDeriv η (orbitProjection A) (fun i ↦ act A (velocities i)) ∂haar = 0 := by
…

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.CriticalBound.IsBasic, OAI.ArnoldCounterexample.CriticalBound.O5, OAI.ArnoldCounterexample.CriticalBound.orbitProjection, OAI.ArnoldCounterexample.CriticalBound.act, OAI.ArnoldCounterexample.CriticalBound.velocities, OAI.ArnoldCounterexample.CriticalBound.haar