English
If f′ ≥ C on interior(D), then f(y)−f(x) ≥ C(y−x) for x≤y in D.
Русский
Если f′(x) ≥ C на interior(D), то f(y)−f(x) ≥ C(y−x) для x≤y в D.
LaTeX
$$$\\forall x\\le y\\in D:\\; f(y)-f(x) \\ge C(y-x)$$$
Lean4
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
`f` grows at least as fast as `C * x` on `D`, i.e., `C * (y - x) ≤ f y - f x` whenever `x, y ∈ D`,
`x ≤ y`. -/
theorem mul_sub_le_image_sub_of_le_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) {C} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) :
∀ᵉ (x ∈ D) (y ∈ D), x ≤ y → C * (y - x) ≤ f y - f x :=
by
intro x hx y hy hxy
rcases eq_or_lt_of_le hxy with hxy' | hxy'
· rw [hxy', sub_self, sub_self, mul_zero]
have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
have hxyD' : Ioo x y ⊆ interior D := subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
obtain ⟨a, a_mem, 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')
have : C ≤ (f y - f x) / (y - x) := ha ▸ hf'_ge _ (hxyD' a_mem)
exact (le_div_iff₀ (sub_pos.2 hxy')).1 this
