OAI/Analysis/AffineBernstein/ParametricNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.parametricFrame_smul_det line 14
2. lemma OAI.AffineBernstein.parametricSecondForm_smul line 29
3. theorem OAI.AffineBernstein.parametricAreaDensity_normalize line 39

   Source comment

   Invariance under positive rescaling of the conormal and reciprocal scaling of the transverse vector. Both are actual multilinear expressions.

   theorem parametricAreaDensity_normalize {n : ℕ}
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E) {U : Set (Space n)} (hU : IsOpen U)
       {X : Space n → E} (hX : ContDiffOn ℝ ∞ X U) (ν : E →L[ℝ] ℝ) (ξ : E)
       {c : ℝ} (hc : 0 < c) {x : Space n} (hx : x ∈ U)
       (hH : 0 ≤ (parametricSecondForm X ν x).det) :
       parametricAreaDensity b X (c • ν) (c⁻¹ • ξ) x =
         parametricAreaDensity b X ν ξ x := by
   …

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

4. lemma OAI.AffineBernstein.parametricFrame_add_tangent_det line 62

   Source comment

   A tangent vector can be added to the transverse column without changing its affine volume.

   lemma parametricFrame_add_tangent_det {n : ℕ}
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E) (X : Space n → E)
       (ξ : E) (x v : Space n) :
       b.det (parametricFrame X (ξ + fderiv ℝ X x v) x) =
         b.det (parametricFrame X ξ x) := by
   …

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

5. lemma OAI.AffineBernstein.parametricAreaDensity_add_tangent line 83