OAI/Analysis/AffineBernstein/LocalMaximumSecond.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.localMax_second_deriv_nonpos line 19

   Source documentation

   The second-order necessary condition, proved from the local Taylor remainder. No elliptic estimate is hidden in the maximum principle step.

   lemma localMax_second_deriv_nonpos {f : ℝ → ℝ}
       (hf : ContDiffAt ℝ 2 f 0) (hm : IsLocalMax f 0) : deriv (deriv f) 0 ≤ 0 := by
   …