antitoneOn_slope_gt — Mathlib

English

If f is differentiable on a convex domain D and its second derivative is strictly negative on D, then f is strictly concave on D.

Русский

Если f дифференцируема на выпуклом D и f'' строго отрицательна на D, то f строго вогнута на D.

LaTeX

$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{DifferentiableOn}(f, D) \\Rightarrow (\\forall x\\in D, (\\mathrm{deriv}^{[2]} f)(x) < 0) \\Rightarrow \\text{StrictConcaveOn}(\\mathbb{R}, D, f).$$

Lean4

theorem antitoneOn_slope_gt (hfc : ConcaveOn 𝕜 s f) (hxs : x ∈ s) : AntitoneOn (slope f x) ({y ∈ s | x < y}) :=
  (hfc.slope_anti hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne'⟩

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