OAI/Analysis/AffineBernstein/LocalMaximumHessian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.deriv_affineLine_comp line 19
2. lemma OAI.AffineBernstein.localMax_second_fderiv_nonpos line 27
3. lemma OAI.AffineBernstein.hessian_neg_posSemidef_of_localMax line 55
4. lemma OAI.AffineBernstein.trace_mul_posSemidef_nonneg line 65
5. lemma OAI.AffineBernstein.inverseHessianTrace_nonpos_of_localMax line 78

   Source documentation

   A local maximum of a smooth test has nonpositive actual linearized Monge--Ampère trace at every positive Hessian point.

   lemma inverseHessianTrace_nonpos_of_localMax {n : ℕ} {u f : Space n → ℝ} {x : Space n}
       (hf : ContDiffAt ℝ ∞ f x) (hp : (hessian u x).PosDef) (hm : IsLocalMax f x) :
       inverseHessianTrace u f x ≤ 0 := by
   …

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