mathlib documentation

analysis.convex.slope

Slopes of convex functions #

This file relates convexity/concavity of functions in a linearly ordered field and the monotonicity of their slopes.

The main use is to show convexity/concavity from monotonicity of the derivative.

theorem convex_on.slope_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hf : convex_on π•œ s f) {x y z : π•œ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
(f y - f x) / (y - x) ≀ (f z - f y) / (z - y)

If f : π•œ β†’ π•œ is convex, then for any three points x < y < z the slope of the secant line of f on [x, y] is less than the slope of the secant line of f on [x, z].

theorem concave_on.slope_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hf : concave_on π•œ s f) {x y z : π•œ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
(f z - f y) / (z - y) ≀ (f y - f x) / (y - x)

If f : π•œ β†’ π•œ is concave, then for any three points x < y < z the slope of the secant line of f on [x, y] is greater than the slope of the secant line of f on [x, z].

theorem strict_convex_on.slope_strict_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hf : strict_convex_on π•œ s f) {x y z : π•œ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
(f y - f x) / (y - x) < (f z - f y) / (z - y)

If f : π•œ β†’ π•œ is strictly convex, then for any three points x < y < z the slope of the secant line of f on [x, y] is strictly less than the slope of the secant line of f on [x, z].

theorem strict_concave_on.slope_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hf : strict_concave_on π•œ s f) {x y z : π•œ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
(f z - f y) / (z - y) < (f y - f x) / (y - x)

If f : π•œ β†’ π•œ is strictly concave, then for any three points x < y < z the slope of the secant line of f on [x, y] is strictly greater than the slope of the secant line of f on [x, z].

theorem convex_on_of_slope_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hs : convex π•œ s) (hf : βˆ€ {x y z : π•œ}, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f y - f x) / (y - x) ≀ (f z - f y) / (z - y)) :
convex_on π•œ s f

If for any three points x < y < z, the slope of the secant line of f : π•œ β†’ π•œ on [x, y] is less than the slope of the secant line of f on [x, z], then f is convex.

theorem concave_on_of_slope_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hs : convex π•œ s) (hf : βˆ€ {x y z : π•œ}, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f z - f y) / (z - y) ≀ (f y - f x) / (y - x)) :
concave_on π•œ s f

If for any three points x < y < z, the slope of the secant line of f : π•œ β†’ π•œ on [x, y] is greater than the slope of the secant line of f on [x, z], then f is concave.

theorem strict_convex_on_of_slope_strict_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hs : convex π•œ s) (hf : βˆ€ {x y z : π•œ}, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f y - f x) / (y - x) < (f z - f y) / (z - y)) :
strict_convex_on π•œ s f

If for any three points x < y < z, the slope of the secant line of f : π•œ β†’ π•œ on [x, y] is strictly less than the slope of the secant line of f on [x, z], then f is strictly convex.

theorem strict_concave_on_of_slope_strict_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hs : convex π•œ s) (hf : βˆ€ {x y z : π•œ}, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f z - f y) / (z - y) < (f y - f x) / (y - x)) :
strict_concave_on π•œ s f

If for any three points x < y < z, the slope of the secant line of f : π•œ β†’ π•œ on [x, y] is strictly greater than the slope of the secant line of f on [x, z], then f is strictly concave.

theorem convex_on_iff_slope_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} :
convex_on π•œ s f ↔ convex π•œ s ∧ βˆ€ ⦃x y z : π•œβ¦„, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f y - f x) / (y - x) ≀ (f z - f y) / (z - y)

A function f : π•œ β†’ π•œ is convex iff for any three points x < y < z the slope of the secant line of f on [x, y] is less than the slope of the secant line of f on [x, z].

theorem concave_on_iff_slope_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} :
concave_on π•œ s f ↔ convex π•œ s ∧ βˆ€ ⦃x y z : π•œβ¦„, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f z - f y) / (z - y) ≀ (f y - f x) / (y - x)

A function f : π•œ β†’ π•œ is concave iff for any three points x < y < z the slope of the secant line of f on [x, y] is greater than the slope of the secant line of f on [x, z].

theorem strict_convex_on_iff_slope_strict_mono_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} :
strict_convex_on π•œ s f ↔ convex π•œ s ∧ βˆ€ ⦃x y z : π•œβ¦„, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f y - f x) / (y - x) < (f z - f y) / (z - y)

A function f : π•œ β†’ π•œ is strictly convex iff for any three points x < y < z the slope of the secant line of f on [x, y] is strictly less than the slope of the secant line of f on [x, z].

theorem strict_concave_on_iff_slope_strict_anti_adjacent {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} :
strict_concave_on π•œ s f ↔ convex π•œ s ∧ βˆ€ ⦃x y z : π•œβ¦„, x ∈ s β†’ z ∈ s β†’ x < y β†’ y < z β†’ (f z - f y) / (z - y) < (f y - f x) / (y - x)

A function f : π•œ β†’ π•œ is strictly concave iff for any three points x < y < z the slope of the secant line of f on [x, y] is strictly greater than the slope of the secant line of f on [x, z].

theorem convex_on.strict_mono_of_lt {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} {f : π•œ β†’ π•œ} (hf : convex_on π•œ s f) {x y : π•œ} (hx : x ∈ s) (hxy : x < y) (hxy' : f x < f y) :

If f is convex on a set s in a linearly ordered field, and f x < f y for two points x < y in s, then f is strictly monotone on s ∩ [y, ∞).