Theorems · Theorem · real analysis

IsLocalMaxOn.hasFDerivWithinAt_nonpos

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {a y : E}, IsLocalMaxOn f s a → HasFDerivWithinAt f f' s a → y ∈ posTangentConeAt s a → f' y ≤ 0

If f has a local max on s at a, f' is the derivative of f at a within s, and y belongs to the positive tangent cone of s at a, then f' y ≤ 0.

Defined in

Mathlib.Analysis.Calculus.LocalExtr.Basic

Cited by

3 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace