OAI/Geometry/Arnold/Factors.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArnoldCounterexample.Factors.moment line 12

   Source documentation

   Oriented-plane coordinates of a unit isotropic vector.

   def moment (a b : Fin 5) (z : CV) : ℝ := 2 * (star (z a) * z b).im

   Mentions: OAI.ArnoldCounterexample.CV

2. def OAI.ArnoldCounterexample.Factors.planeMatrix line 14
3. lemma OAI.ArnoldCounterexample.Factors.moment_real line 16
4. lemma OAI.ArnoldCounterexample.Factors.moment_skew line 20
5. lemma OAI.ArnoldCounterexample.Factors.moment_phase line 24
6. lemma OAI.ArnoldCounterexample.Factors.moment_smooth line 32
7. def OAI.ArnoldCounterexample.Factors.leftSphere line 37

   Source documentation

   The two sphere factors, in self-dual / anti-self-dual plane coordinates.

   def leftSphere (z : CV) : R3 :=
   …

   Mentions: OAI.ArnoldCounterexample.CV

8. def OAI.ArnoldCounterexample.Factors.rightSphere line 41
9. def OAI.ArnoldCounterexample.Factors.sphereFactors line 45
10. def OAI.ArnoldCounterexample.Factors.fourNorm line 47
11. def OAI.ArnoldCounterexample.Factors.fourPolynomial line 48
12. lemma OAI.ArnoldCounterexample.Factors.sphere_norm_identity line 50
13. lemma OAI.ArnoldCounterexample.Factors.sphereFactors_mem line 61
14. lemma OAI.ArnoldCounterexample.Factors.sphereFactors_smooth line 74
15. lemma OAI.ArnoldCounterexample.Factors.planeMatrix_of_sphereFactors line 82
16. def OAI.ArnoldCounterexample.Factors.hermitian line 118
17. def OAI.ArnoldCounterexample.Factors.complexDot line 120
18. lemma OAI.ArnoldCounterexample.Factors.hermitian_self line 122
19. lemma OAI.ArnoldCounterexample.Factors.complexDot_self line 130
20. lemma OAI.ArnoldCounterexample.Factors.moment_complex line 133
21. lemma OAI.ArnoldCounterexample.Factors.matrix_apply line 138
22. lemma OAI.ArnoldCounterexample.Factors.planeMatrix_project_injective line 147
23. lemma OAI.ArnoldCounterexample.Factors.sphereFactors_project_injective line 180