OAI/Analysis/AffineBernstein/ParametricChoices.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.parametricFrame_decomposition line 13
2. lemma OAI.AffineBernstein.parametric_conormal_unique line 27
3. lemma OAI.AffineBernstein.parametric_kernel_is_tangent line 38
4. theorem OAI.AffineBernstein.parametricAreaDensity_choices line 51

   Source comment

   The literal affine area is independent of both allowed choices of conormal and transverse vector. All transversality and orientation properties are explicit; no intrinsic-area object is postulated.

   theorem parametricAreaDensity_choices {n : ℕ}
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E) {U : Set (Space n)} (hU : IsOpen U)
       {X : Space n → E} (hX : ContDiffOn ℝ ∞ X U) {x : Space n} (hx : x ∈ U)
       (ν ν' : E →L[ℝ] ℝ) (ξ ξ' : E)
       (hd : b.det (parametricFrame X ξ x) ≠ 0)
       (hν : ν.comp (fderiv ℝ X x) = 0) (hν' : ν'.comp (fderiv ℝ X x) = 0)
       (hξ : ν ξ = 1) (hξ' : ν' ξ' = 1) (hc : 0 < ν' ξ)
       (hH : 0 ≤ (parametricSecondForm X ν x).det) :
       parametricAreaDensity b X ν' ξ' x = parametricAreaDensity b X ν ξ x := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.parametricFrame, OAI.AffineBernstein.parametricSecondForm, OAI.AffineBernstein.parametricAreaDensity

5. lemma OAI.AffineBernstein.parametricAreaDensity_congr line 73