English
Let D be a convex subset of R. If f is continuous on D, twice differentiable on the interior, and its second derivative f'' is nonpositive on the interior, then f is concave on D.
Русский
Пусть D ⊆ ℝ выпукло. Если f непрерывна на D, внутри D дважды дифференцируема и f''(x) ≤ 0 для x в interior(D), то f concave на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{ContinuousOn}(f,D) \\Rightarrow\\big(\\forall x\\in \\mathrm{intr}(D),\\; \\text{HasDerivWithinAt}(f, f'(x), \\mathrm{intr}(D), x)\\big) \\Rightarrow \\big(\\forall x\\in \\mathrm{intr}(D),\\; \\text{HasDerivWithinAt}(f', (f'')(x), \\mathrm{intr}(D), x)\\big) \\Rightarrow \\big(\\forall x\\in \\mathrm{intr}(D), (f'')(x) \\le 0\\big) \\Rightarrow \\text{ConcaveOn}(\\mathbb{R}, D, f).$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`. -/
theorem concaveOn_of_hasDerivWithinAt2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f f' f'' : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
(hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x) (hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0) :
ConcaveOn ℝ D f := by
have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
· rw [differentiableOn_congr this]
exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt
· rintro x hx
convert hf''₀ _ hx using 1
dsimp
rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
exact (hf'' _ hy).congr this <| by rw [this hy]
