OAI/Geometry/Arnold/Obstruction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArnoldCounterexample.CriticalBound.actCLM line 20

   Source documentation

   The literal orthogonal action, bundled as a real continuous linear map.

   def actCLM (A : RM) : CV →L[ℝ] CV :=
   …

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

2. lemma OAI.ArnoldCounterexample.CriticalBound.actCLM_apply line 23
3. lemma OAI.ArnoldCounterexample.CriticalBound.symplectic_act line 25
4. lemma OAI.ArnoldCounterexample.CriticalBound.cubeForm_orbit line 31
5. def OAI.ArnoldCounterexample.CriticalBound.joinHomotopy line 39

   Source documentation

   Standard join homotopy of the two equivariant sphere maps.

   def joinHomotopy (F : CV → CSpace 3) (p : ℝ × RM) : ProductSpace :=
   …

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

6. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_contDiff line 42
7. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_unit line 47
8. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_fderiv_spatial line 55
9. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_spatial_tangent line 71
10. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_time_tangent line 83
11. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_bracket line 90
12. lemma OAI.ArnoldCounterexample.CriticalBound.haar_mass_pos line 114
13. lemma OAI.ArnoldCounterexample.CriticalBound.productSymplectic_inl line 121
14. lemma OAI.ArnoldCounterexample.CriticalBound.productSymplectic_inr line 127
15. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_zero_cube line 133
16. lemma OAI.ArnoldCounterexample.CriticalBound.sphere_map_tangent line 143
17. lemma OAI.ArnoldCounterexample.CriticalBound.joinHomotopy_half_pi_cube line 162
18. theorem OAI.ArnoldCounterexample.CriticalBound.no_unit_equivariant_map line 181

    Source documentation

    The concrete cup-length obstruction: there is no smooth circle-equivariant map from the literal unit isotropic cone in C5 into the unit sphere in C3. The obstruction is the nonzero third symplectic power.

    theorem no_unit_equivariant_map (F : CV → CSpace 3) (hF : ContDiff ℝ ∞ F)
        (hunit : ∀ z : UnitQuadric, normSq 3 (F z) = 1)
        (hphase : ∀ z : UnitQuadric, ∀ a : ℂ, Complex.normSq a = 1 → F (a • (z : CV)) = a • F z) :
        False := by
    …

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

19. theorem OAI.ArnoldCounterexample.four_le_criticalSet line 229

    Source documentation

    The lower bound for every smooth function, including all possible degenerate critical points. No Morse assumption is made.

    theorem four_le_criticalSet (h : SmoothFunction) : 4 ≤ (criticalSet h).encard := by
    …

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

20. theorem OAI.ArnoldCounterexample.four_le_criticalNumber line 238

    Source documentation

    The critical-number half of the exact main theorem.

    theorem four_le_criticalNumber : 4 ≤ criticalNumber :=
    …

    Mentions: OAI.ArnoldCounterexample.criticalNumber