OAI/Analysis/AffineBernstein/ParametricAffineArea.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.parametricFrame line 14

   Source comment

   The augmented tangent frame, with its transverse column last.

   def parametricFrame {n : ℕ} (X : Space n → E) (ξ : E) (x : Space n) :
       Fin n ⊕ Unit → E :=
   …

   Mentions: OAI.AffineBernstein.Space

2. def OAI.AffineBernstein.parametricSecondForm line 19

   Source comment

   The literal second form with a conormal frozen at the point in question.

   def parametricSecondForm {n : ℕ} (X : Space n → E) (ν : E →L[ℝ] ℝ)
       (x : Space n) : Matrix (Fin n) (Fin n) ℝ := hessian (fun y => ν (X y)) x

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

3. def OAI.AffineBernstein.parametricAreaDensity line 23

   Source comment

   Source (affine-area), using a fixed ambient volume basis.

   def parametricAreaDensity {n : ℕ} (b : Module.Basis (Fin n ⊕ Unit) ℝ E)
       (X : Space n → E) (ν : E →L[ℝ] ℝ) (ξ : E) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

4. lemma OAI.AffineBernstein.hessian_add_constant line 28
5. lemma OAI.AffineBernstein.parametricSecondForm_affine line 33
6. lemma OAI.AffineBernstein.parametricFrame_affine line 43
7. theorem OAI.AffineBernstein.parametricAreaDensity_affine line 55

   Source comment

   Full ambient affine covariance, not restricted to fiber-preserving maps.

   theorem parametricAreaDensity_affine {n : ℕ} (b : Module.Basis (Fin n ⊕ Unit) ℝ E)
       {X : Space n → E} {x : Space n} (hX : DifferentiableAt ℝ X x)
       (L : E ≃L[ℝ] E) (v ξ : E) (ν : E →L[ℝ] ℝ) :
       parametricAreaDensity b (fun y => L (X y) + v)
         (ν.comp L.symm.toContinuousLinearMap) (L ξ) x =
         Real.rpow |LinearMap.det L.toLinearEquiv.toLinearMap| ((n : ℝ) / ((n : ℝ) + 2)) *
           parametricAreaDensity b X ν ξ x := by
   …

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