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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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