English
If a function f is continuous on a convex set D ⊆ ℝ, differentiable on interior(D), and its derivative is monotone on interior(D), then f is convex on D.
Русский
Пусть f непрерывна на выпуклом множестве D ⊆ ℝ, дифференцируема внутри D, и производная f монотонна внутри interior(D); тогда f выпукла на D.
LaTeX
$$$$\\operatorname{ConvexOn}_{\\mathbb{R}} D f \\gets\\!\\!\\!\\!\\!\\rightarrow \\; \\operatorname{MonotoneOn}(\\operatorname{deriv} f)(\\operatorname{interior} D) \\Rightarrow \\operatorname{ConvexOn}_{\\mathbb{R}} D f.$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
and `f'` is monotone on the interior, then `f` is convex on `D`. -/
theorem convexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) (hf'_mono : MonotoneOn (deriv f) (interior D)) : ConvexOn ℝ D f :=
convexOn_of_slope_mono_adjacent hD
(by
intro x y z hx hz hxy hyz
have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
have hxyD' : Ioo x y ⊆ interior D := subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
have hyzD' : Ioo y z ⊆ interior D :=
subset_sUnion_of_mem
⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩
-- Then we apply MVT to both `[x, y]` and `[y, z]`
obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')
obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y) :=
exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD')
rw [← ha, ← hb]
exact hf'_mono (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb).le)
