mathlib3 documentation

analysis.calculus.mean_value

The mean value inequality and equalities #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the following facts:

One-dimensional fencing inequalities #

source
theorem image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), slope f x z < r)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has right derivative B' at every point of [a, b);
  • for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by a function f';
  • we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

source
theorem image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), slope f x z < r)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has derivative B' everywhere on ℝ;
  • for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by a function f';
  • we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

source
theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), B' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), slope f x z < r)) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has right derivative B' at every point of [a, b);
  • for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by B'.

Then f x ≤ B x everywhere on [a, b].

source
theorem image_le_of_deriv_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has right derivative B' at every point of [a, b);
  • f has right derivative f' at every point of [a, b);
  • we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

source
theorem image_le_of_deriv_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has derivative B' everywhere on ℝ;
  • f has right derivative f' at every point of [a, b);
  • we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

source
theorem image_le_of_deriv_right_le_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f' x ≤ B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → f x ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • f a ≤ B a;
  • B has derivative B' everywhere on ℝ;
  • f has right derivative f' at every point of [a, b);
  • we have f' x ≤ B' x on [a, b).

Then f x ≤ B x everywhere on [a, b].

Vector-valued functions f : ℝ → E #

source
theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {a b : ℝ} {E : Type u_1} [normed_add_comm_group E] {f : ℝ → E} {f' : ℝ → ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), slope (has_norm.norm ∘ f) x z < r)) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f x‖ = B x → f' x < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → ‖f x‖ ≤ B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

  • ‖f a‖ ≤ B a;
  • B has right derivative at every point of [a, b);
  • for each x ∈ [a, b) the right-side limit inferior of (‖f z‖ - ‖f x‖) / (z - x) is bounded above by a function f';
  • we have f' x < B' x whenever ‖f x‖ = B x.

Then ‖f x‖ ≤ B x everywhere on [a, b].

source
theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f x‖ = B x → ‖f' x‖ < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → ‖f x‖ ≤ B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

  • ‖f a‖ ≤ B a;
  • f and B have right derivatives f' and B' respectively at every point of [a, b);
  • the norm of f' is strictly less than B' whenever ‖f x‖ = B x.

Then ‖f x‖ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

source
theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f x‖ = B x → ‖f' x‖ < B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → ‖f x‖ ≤ B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

  • ‖f a‖ ≤ B a;
  • f has right derivative f' at every point of [a, b);
  • B has derivative B' everywhere on ℝ;
  • the norm of f' is strictly less than B' whenever ‖f x‖ = B x.

Then ‖f x‖ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

source
theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f' x‖ ≤ B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → ‖f x‖ ≤ B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

  • ‖f a‖ ≤ B a;
  • f and B have right derivatives f' and B' respectively at every point of [a, b);
  • we have ‖f' x‖ ≤ B x everywhere on [a, b).

Then ‖f x‖ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

source
theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f' x‖ ≤ B' x) ⦃x : ℝ⦄ :
x ∈ set.Icc a b → ‖f x‖ ≤ B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

  • ‖f a‖ ≤ B a;
  • f has right derivative f' at every point of [a, b);
  • B has derivative B' everywhere on ℝ;
  • we have ‖f' x‖ ≤ B x everywhere on [a, b).

Then ‖f x‖ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

source
theorem norm_image_sub_le_of_norm_deriv_right_le_segment {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f' x‖ ≤ C) (x : ℝ) (H : x ∈ set.Icc a b) :
‖f x - f a‖ ≤ C * (x - a)

A function on [a, b] with the norm of the right derivative bounded by C satisfies ‖f x - f a‖ ≤ C * (x - a).

source
theorem norm_image_sub_le_of_norm_deriv_le_segment' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f' x‖ ≤ C) (x : ℝ) (H : x ∈ set.Icc a b) :
‖f x - f a‖ ≤ C * (x - a)

A function on [a, b] with the norm of the derivative within [a, b] bounded by C satisfies ‖f x - f a‖ ≤ C * (x - a), has_deriv_within_at version.

source
theorem norm_image_sub_le_of_norm_deriv_le_segment {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b C : ℝ} (hf : differentiable_on ℝ f (set.Icc a b)) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖deriv_within f (set.Icc a b) x‖ ≤ C) (x : ℝ) (H : x ∈ set.Icc a b) :
‖f x - f a‖ ≤ C * (x - a)

A function on [a, b] with the norm of the derivative within [a, b] bounded by C satisfies ‖f x - f a‖ ≤ C * (x - a), deriv_within version.

source
theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f f' : ℝ → E} {C : ℝ} (hf : ∀ (x : ℝ), x ∈ set.Icc 0 1 → has_deriv_within_at f (f' x) (set.Icc 0 1) x) (bound : ∀ (x : ℝ), x ∈ set.Ico 0 1 → ‖f' x‖ ≤ C) :
‖f 1 - f 0‖ ≤ C

A function on [0, 1] with the norm of the derivative within [0, 1] bounded by C satisfies ‖f 1 - f 0‖ ≤ C, has_deriv_within_at version.

source
theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {C : ℝ} (hf : differentiable_on ℝ f (set.Icc 0 1)) (bound : ∀ (x : ℝ), x ∈ set.Ico 0 1 → ‖deriv_within f (set.Icc 0 1) x‖ ≤ C) :
‖f 1 - f 0‖ ≤ C

A function on [0, 1] with the norm of the derivative within [0, 1] bounded by C satisfies ‖f 1 - f 0‖ ≤ C, deriv_within version.

source
theorem constant_of_has_deriv_right_zero {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hcont : continuous_on f (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f 0 (set.Ici x) x) (x : ℝ) (H : x ∈ set.Icc a b) :
f x = f a
source
theorem constant_of_deriv_within_zero {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hdiff : differentiable_on ℝ f (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ico a b → deriv_within f (set.Icc a b) x = 0) (x : ℝ) (H : x ∈ set.Icc a b) :
f x = f a
source
theorem eq_of_has_deriv_right_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' g : ℝ → E} (derivf : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) (derivg : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at g (f' x) (set.Ici x) x) (fcont : continuous_on f (set.Icc a b)) (gcont : continuous_on g (set.Icc a b)) (hi : f a = g a) (y : ℝ) (H : y ∈ set.Icc a b) :
f y = g y

If two continuous functions on [a, b] have the same right derivative and are equal at a, then they are equal everywhere on [a, b].

source
theorem eq_of_deriv_within_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {g : ℝ → E} (fdiff : differentiable_on ℝ f (set.Icc a b)) (gdiff : differentiable_on ℝ g (set.Icc a b)) (hderiv : set.eq_on (deriv_within f (set.Icc a b)) (deriv_within g (set.Icc a b)) (set.Ico a b)) (hi : f a = g a) (y : ℝ) (H : y ∈ set.Icc a b) :
f y = g y

If two differentiable functions on [a, b] have the same derivative within [a, b] everywhere on [a, b) and are equal at a, then they are equal everywhere on [a, b].

Vector-valued functions f : E → G #

Theorems in this section work both for real and complex differentiable functions. We use assumptions [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 G] to achieve this result. For the domain E we also assume [normed_space ℝ E] to have a notion of a convex set.

source
theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[𝕜] G)} (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with has_fderiv_within.

source
theorem convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {s : set E} {f' : E → (E →L[𝕜] G)} {C : nnreal} (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C) (hs : convex ℝ s) :
lipschitz_on_with C f s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with has_fderiv_within and lipschitz_on_with.

source
theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} {f' : E → (E →L[𝕜] G)} (hs : convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhds_within x s, has_fderiv_within_at f (f' y) s y) (hcont : continuous_within_at f' s x) (K : nnreal) (hK : ‖f' x‖₊ < K) :
∃ (t : set E) (H : t ∈ nhds_within x s), lipschitz_on_with K f t

Let s be a convex set in a real normed vector space E, let f : E → G be a function differentiable within s in a neighborhood of x : E with derivative f'. Suppose that f' is continuous within s at x. Then for any number K : ℝ≥0 larger than ‖f' x‖₊, f is K-Lipschitz on some neighborhood of x within s. See also convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at for a version that claims existence of K instead of an explicit estimate.

source
theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} {f' : E → (E →L[𝕜] G)} (hs : convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhds_within x s, has_fderiv_within_at f (f' y) s y) (hcont : continuous_within_at f' s x) :
∃ (K : nnreal) (t : set E) (H : t ∈ nhds_within x s), lipschitz_on_with K f t

Let s be a convex set in a real normed vector space E, let f : E → G be a function differentiable within s in a neighborhood of x : E with derivative f'. Suppose that f' is continuous within s at x. Then for any number K : ℝ≥0 larger than ‖f' x‖₊, f is Lipschitz on some neighborhood of x within s. See also convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt for a version with an explicit estimate on the Lipschitz constant.

source
theorem convex.norm_image_sub_le_of_norm_fderiv_within_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} (hf : differentiable_on 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderiv_within 𝕜 f s x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set: if the derivative of a function within this set is bounded by C, then the function is C-Lipschitz. Version with fderiv_within.

source
theorem convex.lipschitz_on_with_of_nnnorm_fderiv_within_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {s : set E} {C : nnreal} (hf : differentiable_on 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderiv_within 𝕜 f s x‖₊ ≤ C) (hs : convex ℝ s) :
lipschitz_on_with C f s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with fderiv_within and lipschitz_on_with.

source
theorem convex.norm_image_sub_le_of_norm_fderiv_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} (hf : ∀ (x : E), x ∈ s → differentiable_at 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with fderiv.

source
theorem convex.lipschitz_on_with_of_nnnorm_fderiv_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {s : set E} {C : nnreal} (hf : ∀ (x : E), x ∈ s → differentiable_at 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x‖₊ ≤ C) (hs : convex ℝ s) :
lipschitz_on_with C f s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with fderiv and lipschitz_on_with.

source
theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[𝕜] G)} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x - φ‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x - ⇑φ (y - x)‖ ≤ C * ‖y - x‖

Variant of the mean value inequality on a convex set, using a bound on the difference between the derivative and a fixed linear map, rather than a bound on the derivative itself. Version with has_fderiv_within.

source
theorem convex.norm_image_sub_le_of_norm_fderiv_within_le' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} {φ : E →L[𝕜] G} (hf : differentiable_on 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderiv_within 𝕜 f s x - φ‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x - ⇑φ (y - x)‖ ≤ C * ‖y - x‖

Variant of the mean value inequality on a convex set. Version with fderiv_within.

source
theorem convex.norm_image_sub_le_of_norm_fderiv_le' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x ∈ s → differentiable_at 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x - φ‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x - ⇑φ (y - x)‖ ≤ C * ‖y - x‖

Variant of the mean value inequality on a convex set. Version with fderiv.

source
theorem convex.is_const_of_fderiv_within_eq_zero {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} {s : set E} {x y : E} (hs : convex ℝ s) (hf : differentiable_on 𝕜 f s) (hf' : ∀ (x : E), x ∈ s → fderiv_within 𝕜 f s x = 0) (hx : x ∈ s) (hy : y ∈ s) :
f x = f y

If a function has zero Fréchet derivative at every point of a convex set, then it is a constant on this set.

source
theorem is_const_of_fderiv_eq_zero {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f : E → G} (hf : differentiable 𝕜 f) (hf' : ∀ (x : E), fderiv 𝕜 f x = 0) (x y : E) :
f x = f y
source
theorem convex.eq_on_of_fderiv_within_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f g : E → G} {s : set E} {x : E} (hs : convex ℝ s) (hf : differentiable_on 𝕜 f s) (hg : differentiable_on 𝕜 g s) (hs' : unique_diff_on 𝕜 s) (hf' : ∀ (x : E), x ∈ s → fderiv_within 𝕜 f s x = fderiv_within 𝕜 g s x) (hx : x ∈ s) (hfgx : f x = g x) :
set.eq_on f g s

If two functions have equal Fréchet derivatives at every point of a convex set, and are equal at one point in that set, then they are equal on that set.

source
theorem eq_of_fderiv_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group G] [normed_space 𝕜 G] {f g : E → G} (hf : differentiable 𝕜 f) (hg : differentiable 𝕜 g) (hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x) (x : E) (hfgx : f x = g x) :
f = g
source
theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f f' : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : ℝ} (hf : ∀ (x : 𝕜), x ∈ s → has_deriv_within_at f (f' x) s x) (bound : ∀ (x : 𝕜), x ∈ s → ‖f' x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with has_deriv_within.

source
theorem convex.lipschitz_on_with_of_nnnorm_has_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f f' : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hs : convex ℝ s) (hf : ∀ (x : 𝕜), x ∈ s → has_deriv_within_at f (f' x) s x) (bound : ∀ (x : 𝕜), x ∈ s → ‖f' x‖₊ ≤ C) :
lipschitz_on_with C f s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with has_deriv_within and lipschitz_on_with.

source
theorem convex.norm_image_sub_le_of_norm_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : ℝ} (hf : differentiable_on 𝕜 f s) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv_within f s x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set in dimension 1: if the derivative of a function within this set is bounded by C, then the function is C-Lipschitz. Version with deriv_within

source
theorem convex.lipschitz_on_with_of_nnnorm_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hs : convex ℝ s) (hf : differentiable_on 𝕜 f s) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv_within f s x‖₊ ≤ C) :
lipschitz_on_with C f s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with deriv_within and lipschitz_on_with.

source
theorem convex.norm_image_sub_le_of_norm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : ℝ} (hf : ∀ (x : 𝕜), x ∈ s → differentiable_at 𝕜 f x) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv f x‖ ≤ C) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x‖ ≤ C * ‖y - x‖

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with deriv.

source
theorem convex.lipschitz_on_with_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hf : ∀ (x : 𝕜), x ∈ s → differentiable_at 𝕜 f x) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv f x‖₊ ≤ C) (hs : convex ℝ s) :
lipschitz_on_with C f s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with deriv and lipschitz_on_with.

source
theorem lipschitz_with_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} {C : nnreal} (hf : differentiable 𝕜 f) (bound : ∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C) :
lipschitz_with C f

The mean value theorem set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with deriv and lipschitz_with.

source
theorem is_const_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [normed_add_comm_group G] [normed_space 𝕜 G] {f : 𝕜 → G} (hf : differentiable 𝕜 f) (hf' : ∀ (x : 𝕜), deriv f x = 0) (x y : 𝕜) :
f x = f y

If f : 𝕜 → G, 𝕜 = R or 𝕜 = ℂ, is differentiable everywhere and its derivative equal zero, then it is a constant function.

Functions [a, b] → ℝ. #

source
theorem exists_ratio_has_deriv_at_eq_ratio_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) (g g' : ℝ → ℝ) (hgc : continuous_on g (set.Icc a b)) (hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), (g b - g a) * f' c = (f b - f a) * g' c

Cauchy's Mean Value Theorem, has_deriv_at version.

source
theorem exists_ratio_has_deriv_at_eq_ratio_slope' (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g g' : ℝ → ℝ) {lfa lga lfb lgb : ℝ} (hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) (hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x) (hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds lfa)) (hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds lga)) (hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds lfb)) (hgb : filter.tendsto g (nhds_within b (set.Iio b)) (nhds lgb)) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), (lgb - lga) * f' c = (lfb - lfa) * g' c

Cauchy's Mean Value Theorem, extended has_deriv_at version.

source
theorem exists_has_deriv_at_eq_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), f' c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, has_deriv_at version

source
theorem exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfd : differentiable_on ℝ f (set.Ioo a b)) (g : ℝ → ℝ) (hgc : continuous_on g (set.Icc a b)) (hgd : differentiable_on ℝ g (set.Ioo a b)) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), (g b - g a) * deriv f c = (f b - f a) * deriv g c

Cauchy's Mean Value Theorem, deriv version.

source
theorem exists_ratio_deriv_eq_ratio_slope' (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) {lfa lga lfb lgb : ℝ} (hdf : differentiable_on ℝ f (set.Ioo a b)) (hdg : differentiable_on ℝ g (set.Ioo a b)) (hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds lfa)) (hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds lga)) (hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds lfb)) (hgb : filter.tendsto g (nhds_within b (set.Iio b)) (nhds lgb)) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c

Cauchy's Mean Value Theorem, extended deriv version.

source
theorem exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfd : differentiable_on ℝ f (set.Ioo a b)) :
∃ (c : ℝ) (H : c ∈ set.Ioo a b), deriv f c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, deriv version.

source
theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (hf'_gt : ∀ (x : ℝ), x ∈ interior D → C < deriv f x) (x : ℝ) (H : x ∈ D) (y : ℝ) (H_1 : y ∈ D) :
x < y → C * (y - x) < f y - f x

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 faster than C * x on D, i.e., C * (y - x) < f y - f x whenever x, y ∈ D, x < y.

source
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

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.

source
theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x) (x : ℝ) (H : x ∈ D) (y : ℝ) (H_1 : y ∈ D) :
x ≤ y → C * (y - x) ≤ f y - f x

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.

source
theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (hf'_ge : ∀ (x : ℝ), C ≤ deriv f x) ⦃x y : ℝ⦄ (hxy : 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.

source
theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (lt_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < C) (x : ℝ) (H : x ∈ D) (y : ℝ) (H_1 : y ∈ D) :
x < y → f y - f x < C * (y - x)

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 f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x, y ∈ D, x < y.

source
theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (lt_hf' : ∀ (x : ℝ), deriv f x < C) ⦃x y : ℝ⦄ (hxy : x < y) :
f y - f x < C * (y - x)

Let f : ℝ → ℝ be a differentiable function. If f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x < y.

source
theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C) (x : ℝ) (H : x ∈ D) (y : ℝ) (H_1 : y ∈ D) :
x ≤ y → f y - f x ≤ C * (y - x)

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 f' ≤ C, then f grows at most as fast as C * x on D, i.e., f y - f x ≤ C * (y - x) whenever x, y ∈ D, x ≤ y.

source
theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (le_hf' : ∀ (x : ℝ), deriv f x ≤ C) ⦃x y : ℝ⦄ (hxy : x ≤ y) :
f y - f x ≤ C * (y - x)

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

source
theorem convex.strict_mono_on_of_deriv_pos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x) :
strict_mono_on f D

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 f' is positive, then f is a strictly monotone function on D. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

source
theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), 0 < deriv f x) :
strict_mono f

Let f : ℝ → ℝ be a differentiable function. If f' is positive, then f is a strictly monotone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

source
theorem convex.monotone_on_of_deriv_nonneg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv f x) :
monotone_on f D

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 f' is nonnegative, then f is a monotone function on D.

source
theorem monotone_of_deriv_nonneg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ (x : ℝ), 0 ≤ deriv f x) :
monotone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonnegative, then f is a monotone function.

source
theorem convex.strict_anti_on_of_deriv_neg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < 0) :
strict_anti_on f D

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 f' is negative, then f is a strictly antitone function on D.

source
theorem strict_anti_of_deriv_neg {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), deriv f x < 0) :
strict_anti f

Let f : ℝ → ℝ be a differentiable function. If f' is negative, then f is a strictly antitone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly negative.

source
theorem convex.antitone_on_of_deriv_nonpos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_nonpos : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ 0) :
antitone_on f D

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 f' is nonpositive, then f is an antitone function on D.

source
theorem antitone_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ (x : ℝ), deriv f x ≤ 0) :
antitone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonpositive, then f is an antitone function.

source
theorem monotone_on.convex_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_mono : monotone_on (deriv f) (interior D)) :
convex_on ℝ D f

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.

source
theorem antitone_on.concave_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (h_anti : antitone_on (deriv f) (interior D)) :
concave_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is antitone on the interior, then f is concave on D.

source
theorem strict_mono_on.exists_slope_lt_deriv_aux {x y : ℝ} {f : ℝ → ℝ} (hf : continuous_on f (set.Icc x y)) (hxy : x < y) (hf'_mono : strict_mono_on (deriv f) (set.Ioo x y)) (h : ∀ (w : ℝ), w ∈ set.Ioo x y → deriv f w ≠ 0) :
∃ (a : ℝ) (H : a ∈ set.Ioo x y), (f y - f x) / (y - x) < deriv f a
source
theorem strict_mono_on.exists_slope_lt_deriv {x y : ℝ} {f : ℝ → ℝ} (hf : continuous_on f (set.Icc x y)) (hxy : x < y) (hf'_mono : strict_mono_on (deriv f) (set.Ioo x y)) :
∃ (a : ℝ) (H : a ∈ set.Ioo x y), (f y - f x) / (y - x) < deriv f a
source
theorem strict_mono_on.exists_deriv_lt_slope_aux {x y : ℝ} {f : ℝ → ℝ} (hf : continuous_on f (set.Icc x y)) (hxy : x < y) (hf'_mono : strict_mono_on (deriv f) (set.Ioo x y)) (h : ∀ (w : ℝ), w ∈ set.Ioo x y → deriv f w ≠ 0) :
∃ (a : ℝ) (H : a ∈ set.Ioo x y), deriv f a < (f y - f x) / (y - x)
source
theorem strict_mono_on.exists_deriv_lt_slope {x y : ℝ} {f : ℝ → ℝ} (hf : continuous_on f (set.Icc x y)) (hxy : x < y) (hf'_mono : strict_mono_on (deriv f) (set.Ioo x y)) :
∃ (a : ℝ) (H : a ∈ set.Ioo x y), deriv f a < (f y - f x) / (y - x)
source
theorem strict_mono_on.strict_convex_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : strict_mono_on (deriv f) (interior D)) :
strict_convex_on ℝ D f

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'.

source
theorem strict_anti_on.strict_concave_on_of_deriv {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (h_anti : strict_anti_on (deriv f) (interior D)) :
strict_concave_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f' is strictly antitone on the interior, then f is strictly concave on D. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

source
theorem monotone.convex_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf'_mono : monotone (deriv f)) :
convex_on ℝ set.univ f

If a function f is differentiable and f' is monotone on ℝ then f is convex.

source
theorem antitone.concave_on_univ_of_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf'_anti : antitone (deriv f)) :
concave_on ℝ set.univ f

If a function f is differentiable and f' is antitone on ℝ then f is concave.

source
theorem strict_mono.strict_convex_on_univ_of_deriv {f : ℝ → ℝ} (hf : continuous f) (hf'_mono : strict_mono (deriv f)) :
strict_convex_on ℝ set.univ f

If a function f is continuous and f' is strictly monotone on ℝ then f is strictly convex. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict monotonicity of f'.

source
theorem strict_anti.strict_concave_on_univ_of_deriv {f : ℝ → ℝ} (hf : continuous f) (hf'_anti : strict_anti (deriv f)) :
strict_concave_on ℝ set.univ f

If a function f is continuous and f' is strictly antitone on ℝ then f is strictly concave. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

source
theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'' : differentiable_on ℝ (deriv f) (interior D)) (hf''_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv^[2] f x) :
convex_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonnegative on the interior, then f is convex on D.

source
theorem concave_on_of_deriv2_nonpos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'' : differentiable_on ℝ (deriv f) (interior D)) (hf''_nonpos : ∀ (x : ℝ), x ∈ interior D → deriv^[2] f x ≤ 0) :
concave_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonpositive on the interior, then f is concave on D.

source
theorem strict_convex_on_of_deriv2_pos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf'' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv^[2] f x) :
strict_convex_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on the interior, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

source
theorem strict_concave_on_of_deriv2_neg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf'' : ∀ (x : ℝ), x ∈ interior D → deriv^[2] f x < 0) :
strict_concave_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on the interior, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it already implied by the second derivative being strictly negative, except at at most one point.

source
theorem convex_on_of_deriv2_nonneg' {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D) (hf''_nonneg : ∀ (x : ℝ), x ∈ D → 0 ≤ deriv^[2] f x) :
convex_on ℝ D f

If a function f is twice differentiable on a open convex set D ⊆ ℝ and f'' is nonnegative on D, then f is convex on D.

source
theorem concave_on_of_deriv2_nonpos' {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D) (hf''_nonpos : ∀ (x : ℝ), x ∈ D → deriv^[2] f x ≤ 0) :
concave_on ℝ D f

If a function f is twice differentiable on an open convex set D ⊆ ℝ and f'' is nonpositive on D, then f is concave on D.

source
theorem strict_convex_on_of_deriv2_pos' {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf'' : ∀ (x : ℝ), x ∈ D → 0 < deriv^[2] f x) :
strict_convex_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on D, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

source
theorem strict_concave_on_of_deriv2_neg' {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf'' : ∀ (x : ℝ), x ∈ D → deriv^[2] f x < 0) :
strict_concave_on ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on D, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.

source
theorem convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : differentiable ℝ f) (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ (x : ℝ), 0 ≤ deriv^[2] f x) :
convex_on ℝ set.univ f

If a function f is twice differentiable on ℝ, and f'' is nonnegative on ℝ, then f is convex on ℝ.

source
theorem concave_on_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : differentiable ℝ f) (hf'' : differentiable ℝ (deriv f)) (hf''_nonpos : ∀ (x : ℝ), deriv^[2] f x ≤ 0) :
concave_on ℝ set.univ f

If a function f is twice differentiable on ℝ, and f'' is nonpositive on ℝ, then f is concave on ℝ.

source
theorem strict_convex_on_univ_of_deriv2_pos {f : ℝ → ℝ} (hf : continuous f) (hf'' : ∀ (x : ℝ), 0 < deriv^[2] f x) :
strict_convex_on ℝ set.univ f

If a function f is continuous on ℝ, and f'' is strictly positive on ℝ, then f is strictly convex on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

source
theorem strict_concave_on_univ_of_deriv2_neg {f : ℝ → ℝ} (hf : continuous f) (hf'' : ∀ (x : ℝ), deriv^[2] f x < 0) :
strict_concave_on ℝ set.univ f

If a function f is continuous on ℝ, and f'' is strictly negative on ℝ, then f is strictly concave on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.

Functions f : E → ℝ #

source
theorem domain_mvt {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ] ℝ)} (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
∃ (z : E) (H : z ∈ segment ℝ x y), f y - f x = ⇑(f' z) (y - x)

Lagrange's Mean Value Theorem, applied to convex domains.

Vector-valued functions f : E → F. Strict differentiability. #

A C^1 function is strictly differentiable, when the field is ℝ or ℂ. This follows from the mean value inequality on balls, which is a particular case of the above results after restricting the scalars to ℝ. Note that it does not make sense to talk of a convex set over ℂ, but balls make sense and are enough. Many formulations of the mean value inequality could be generalized to balls over ℝ or ℂ. For now, we only include the ones that we need.

source
theorem has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at {𝕜 : Type u_3} [is_R_or_C 𝕜] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {H : Type u_5} [normed_add_comm_group H] [normed_space 𝕜 H] {f : G → H} {f' : G → (G →L[𝕜] H)} {x : G} (hder : ∀ᶠ (y : G) in nhds x, has_fderiv_at f (f' y) y) (hcont : continuous_at f' x) :
has_strict_fderiv_at f (f' x) x

Over the reals or the complexes, a continuously differentiable function is strictly differentiable.

source
theorem has_strict_deriv_at_of_has_deriv_at_of_continuous_at {𝕜 : Type u_3} [is_R_or_C 𝕜] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f f' : 𝕜 → G} {x : 𝕜} (hder : ∀ᶠ (y : 𝕜) in nhds x, has_deriv_at f (f' y) y) (hcont : continuous_at f' x) :
has_strict_deriv_at f (f' x) x

Over the reals or the complexes, a continuously differentiable function is strictly differentiable.