English
Let D be a convex subset of R. If a function f is continuous on D, twice differentiable on the interior of D, and its second derivative f'' is nonnegative on the interior, then f is convex on D.
Русский
Пусть D ⊆ ℝ выпуктое множество. Тогда если f непрерывна на D, во внутренности D дважды дифференцируема и f''(x) ≥ 0 для всех x в interior(D), то f выпукла на 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), 0 \\le (f'')(x)\\big) \\Rightarrow \\text{ConvexOn}(\\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 nonnegative on the interior, then `f` is convex on `D`. -/
theorem convexOn_of_hasDerivWithinAt2_nonneg {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, 0 ≤ f'' x) :
ConvexOn ℝ D f := by
have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
refine convexOn_of_deriv2_nonneg 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]
