OAI/Analysis/AffineBernstein/GlobalDetRatio.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.det_hessian_normalizedFunction line 17
2. theorem OAI.AffineBernstein.centered_balanced_global_det_ratio line 27

   Source documentation

   Genuine global determinant-ratio bounds follow from the uniform balanced section normalizations. This is a consequence of the original PDE, rather than a global determinant assumption. It does not imply individual Hessian bounds.

   theorem centered_balanced_global_det_ratio {n : ℕ} (hn : 1 ≤ n)
       {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
       (hm : AffineMaximalOn univ u) (hu0 : u 0=0) (hdu0 : fderiv ℝ u 0=0)
       {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ) :
       ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ x : Space n,
         c * (hessian u 0).det ≤ (hessian u x).det ∧
         (hessian u x).det ≤ C * (hessian u 0).det := by
   …

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