Theorems · Theorem · real analysis

mul_sub_le_image_sub_of_le_deriv

∀ {f : ℝ → ℝ}, Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), C ≤ deriv f x) → ∀ ⦃x y : ℝ⦄, x ≤ y → C * (y - x) ≤ f y - f x

Let f : ℝ → ℝ be a differentiable function. If C ≤ f', then f grows at least as fast as C * x, i.e., C * (y - x) ≤ f y - f x whenever x ≤ y.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

0 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound