English
If a function f is continuous on a convex set D and its derivative is strictly monotone on interior(D), then f is strictly convex on D.
Русский
Если функция f непрерывна на выпуклом множестве D, и её производная строго монотонна на interior(D), то f строго выпукла на D.
LaTeX
$$$$\\text{ConvexReal } D \\Rightarrow \\text{StrictConvexOn}_{\\mathbb{R}} D f.$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, and `f'` is strictly monotone on the
interior, then `f` is strictly convex on `D`.
Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict monotonicity of `f'`. -/
theorem strictConvexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : StrictMonoOn (deriv f) (interior D)) : StrictConvexOn ℝ D f :=
strictConvexOn_of_slope_strict_mono_adjacent hD fun {x y z} hx hz hxy hyz => by
-- First we prove some trivial inclusions
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 get points `a` and `b` in each interval `[x, y]` and `[y, z]` where the derivatives
-- can be compared to the slopes between `x, y` and `y, z` respectively.
obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a :=
StrictMonoOn.exists_slope_lt_deriv (hf.mono hxyD) hxy (hf'.mono hxyD')
obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b < (f z - f y) / (z - y) :=
StrictMonoOn.exists_deriv_lt_slope (hf.mono hyzD) hyz (hf'.mono hyzD')
apply ha.trans (lt_trans _ hb)
exact hf' (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb)
