OAI/Geometry/Arnold/Sphere.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArnoldCounterexample.ThreePoints.E3 line 15
  2. abbrev OAI.ArnoldCounterexample.ThreePoints.S2 line 16
  3. def OAI.ArnoldCounterexample.ThreePoints.coords line 20
  4. def OAI.ArnoldCounterexample.ThreePoints.sphereEmbed line 22
  5. def OAI.ArnoldCounterexample.ThreePoints.spherePairEmbed line 24
  6. def OAI.ArnoldCounterexample.ThreePoints.sphereF line 26
  7. lemma OAI.ArnoldCounterexample.ThreePoints.inner_coords line 28
  8. lemma OAI.ArnoldCounterexample.ThreePoints.norm_sq_coords line 33
  9. lemma OAI.ArnoldCounterexample.ThreePoints.sphereEmbed_mem line 36
  10. lemma OAI.ArnoldCounterexample.ThreePoints.spherePairEmbed_mem line 41
  11. lemma OAI.ArnoldCounterexample.ThreePoints.sphereEmbed_injective line 44
  12. lemma OAI.ArnoldCounterexample.ThreePoints.spherePairEmbed_injective line 48
  13. lemma OAI.ArnoldCounterexample.ThreePoints.exists_sphereEmbed line 51
  14. lemma OAI.ArnoldCounterexample.ThreePoints.range_spherePairEmbed line 60
  15. lemma OAI.ArnoldCounterexample.ThreePoints.sphereEmbed_smooth line 70
  16. lemma OAI.ArnoldCounterexample.ThreePoints.spherePairEmbed_smooth line 73
  17. theorem OAI.ArnoldCounterexample.ThreePoints.sphereF_smooth line 78
  18. def OAI.ArnoldCounterexample.ThreePoints.sphereEmbedDeriv line 81
  19. lemma OAI.ArnoldCounterexample.ThreePoints.sphereEmbed_mfderiv line 85
  20. lemma OAI.ArnoldCounterexample.ThreePoints.sphereEmbedDeriv_range line 94
  21. lemma OAI.ArnoldCounterexample.ThreePoints.spherePairEmbed_mfderiv line 115
  22. lemma OAI.ArnoldCounterexample.ThreePoints.sphereF_mfderiv line 127
  23. lemma OAI.ArnoldCounterexample.ThreePoints.sphereF_critical_iff line 139
  24. theorem OAI.ArnoldCounterexample.ThreePoints.sphereF_critical_encard line 164

    Source documentation

    The critical count on the smooth sphere-product manifold.

    theorem sphereF_critical_encard :
    {q : S2 × S2 | mfderiv ((𝓡 2).prod (𝓡 2)) 𝓘(ℝ, ℝ) sphereF q = 0}.encard = 3 := by
…

    Mentions: OAI.ArnoldCounterexample.ThreePoints.S2, OAI.ArnoldCounterexample.ThreePoints.sphereF