OAI/Analysis/AffineBernstein/FiniteProjectiveCharts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.projectiveAxis line 18
2. lemma OAI.AffineBernstein.projectiveAxis_norm line 21
3. lemma OAI.AffineBernstein.projectiveAxis_inner line 25
4. def OAI.AffineBernstein.projectiveFrameAt line 32
5. lemma OAI.AffineBernstein.projectiveFrameAt_axis line 36
6. def OAI.AffineBernstein.signedProjectiveFrame line 42
7. lemma OAI.AffineBernstein.signedProjectiveFrame_cover line 49

   Source documentation

   A concrete finite full covering by positive projective hemispheres; there is no discarded equator in this pointwise statement.

   lemma signedProjectiveFrame_cover (b : OrthonormalBasis τ ℝ E)
       (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E) {v : E} (hv : v ≠ 0) :
       ∃ j : τ × Bool, 0 < inner ℝ v (projectiveAxis (signedProjectiveFrame b f j)) := by
   …

   Mentions: OAI.AffineBernstein.projectiveAxis, OAI.AffineBernstein.signedProjectiveFrame