OAI/Analysis/AffineBernstein/ParametricDensityCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.parametricAreaDensity_comp line 14

   Source comment

   Exact density change of variables; its Jacobian has exponent one.

   theorem parametricAreaDensity_comp {n : ℕ}
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E)
       {X : Space n → E} {φ : Space n → Space n} {x : Space n}
       (hX : ContDiffAt ℝ ∞ X (φ x)) (hφ : ContDiffAt ℝ ∞ φ x)
       (ν : E →L[ℝ] ℝ) (ξ : E) (hν : ν.comp (fderiv ℝ X (φ x)) = 0)
       (hH : 0 ≤ (parametricSecondForm X ν (φ x)).det)
       (hJ : (parametricJacobian φ x).det ≠ 0) :
       parametricAreaDensity b (X ∘ φ) ν ξ x =
         |(parametricJacobian φ x).det| * parametricAreaDensity b X ν ξ (φ x) := by
   …

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