OAI/Analysis/AffineBernstein/SimultaneousMinima.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.centered_balanced_simultaneous_minima line 21

   Source documentation

   Any finite family of nonnegative entire supersolutions with infimum zero has simultaneous arbitrarily small values. This uses generated normalizations, not uniform-ellipticity assumptions.

   theorem centered_balanced_simultaneous_minima {n : ℕ} (hn : 1 ≤ n)
       {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
       (hm : AffineMaximalOn univ u) (hzero : u 0=0) (hdzero : fderiv ℝ u 0=0)
       {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ)
       {ι : Type*} [Fintype ι] (F : ι → Space n → ℝ)
       (hF : ∀ i, ContDiff ℝ ∞ (F i)) (hpos : ∀ i x, 0 ≤ F i x)
       (hLF : ∀ i x, inverseHessianTrace u (F i) x ≤ 0)
       (hsmall : ∀ i ε, 0 < ε → ∃ x, F i x < ε) {η : ℝ} (hη : 0 < η) :
       ∃ x, ∀ i, F i x < η := by
   …

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

2. theorem OAI.AffineBernstein.balanced_simultaneous_minima line 74