fderivWithin_nonneg — Mathlib

English

If a has a local minimum on s and y is in the positive tangent cone, then fderivWithin y ≥ 0.

Русский

Если у f будет локальный минимум на s в a, и y лежит в pos tangent cone, то fderivWithin по y неотрицательно.

LaTeX

$$$ fderivWithin \\(\\mathbb{R}\\; f\\; s\\; a\\; y \\ge 0 $$$

Lean4

/-- If `f` has a local min on `s` at `a` and `y` belongs to the positive tangent cone
of `s` at `a`, then `0 ≤ f' y`. -/
theorem fderivWithin_nonneg (h : IsLocalMinOn f s a) (hy : y ∈ posTangentConeAt s a) :
    (0 : ℝ) ≤ (fderivWithin ℝ f s a : E → ℝ) y := by
  classical
    exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonneg hf.hasFDerivWithinAt hy
    else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Похожие утверждения