OAI/Analysis/AffineBernstein/FlatFEquation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.flatInverseTrace_hessian line 16
2. lemma OAI.AffineBernstein.flatInverseTrace_neg_hessian line 21
3. theorem OAI.AffineBernstein.flat_f_equation_of_log_euler line 32

   Source comment

   The exact local flat-chart f equation. At the center of the flat normal chart its angular terms equal the spherical covariant terms; no derivative of a determinant or scalar density has been omitted.

   theorem flat_f_equation_of_log_euler {W : Set E} (hW : IsOpen W)
       {φ t : E → ℝ} (hφ : ContDiffOn ℝ ∞ φ W) (ht : ContDiffOn ℝ ∞ t W)
       (hpos : ∀ y ∈ W, 0 < φ y) (v : ι → E) (w : κ → E)
       {x : E} (hx : x ∈ W) {c : ℝ}
       (hBd : (-flatBlockHessian φ v x).det ≠ 0)
       (hRd : (flatBlockHessian φ w x).det ≠ 0)
       (he : flatInverseTrace (-flatBlockHessian φ v x) v t x -
         c*flatInversePair (-flatBlockHessian φ v x) v t t x +
         flatInverseTrace (flatBlockHessian φ w x) w t x +
         flatInversePair (flatBlockHessian φ w x) w t t x = 0) :
       let B := -flatBlockHessian φ v x
   …

   Mentions: OAI.AffineBernstein.flatBlockHessian, OAI.AffineBernstein.flatInverseTrace, OAI.AffineBernstein.flatInversePair