OAI/Analysis/AffineBernstein/HessianDominance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.balanced_dominating_hessian line 21

   Source documentation

   The simultaneous near-minimum principle produces one limiting Hessian which dominates every actual Hessian in quadratic-form order.

   theorem balanced_dominating_hessian {n : ℕ} (hn : 1 ≤ n)
       {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
       (hm : AffineMaximalOn univ u) {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
       (hbal : SectionBalance univ u ρ)
       (hD : ∀ x y, (hessian u x).det=(hessian u y).det) :
       ∃ A ∈ closure (range (hessian u)), ∀ x, (A-hessian u x).PosSemidef := by
   …

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

2. theorem OAI.AffineBernstein.balanced_constant_hessian line 95