mul_sub_lt_image_sub_of_lt_deriv — Mathlib

English

If f′(x) > C for all x in interior of D, then f grows faster than C on D; i.e., C(y−x) < f(y)−f(x) for x<y in D.

Русский

Если f′(x) > C наInterior(D), тогда f растёт быстрее, чем C(y−x) на D: C(y−x) < f(y)−f(x) при x<y.

LaTeX

$$$\\forall x

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than
`C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`. -/
theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C} (hf'_gt : ∀ x, C < deriv f x) ⦃x y⦄
    (hxy : x < y) : C * (y - x) < f y - f x :=
  convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuousOn hf.differentiableOn (fun x _ => hf'_gt x) x
    trivial y trivial hxy

Похожие утверждения