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 ConvexOn.slope_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 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 [y, z].

theorem ConcaveOn.slope_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConcaveOn 𝕜 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 [y, z].

theorem StrictConvexOn.slope_strict_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConvexOn 𝕜 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 [y, z].

theorem StrictConcaveOn.slope_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConcaveOn 𝕜 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 [y, z].

theorem convexOn_of_slope_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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)) : ConvexOn 𝕜 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 [y, z], then f is convex.

theorem concaveOn_of_slope_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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)) : ConcaveOn 𝕜 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 [y, z], then f is concave.

theorem strictConvexOn_of_slope_strict_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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)) : StrictConvexOn 𝕜 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 [y, z], then f is strictly convex.

theorem strictConcaveOn_of_slope_strict_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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)) : StrictConcaveOn 𝕜 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 [y, z], then f is strictly concave.

theorem convexOn_iff_slope_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} : ConvexOn 𝕜 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 [y, z].

theorem concaveOn_iff_slope_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} : ConcaveOn 𝕜 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 [y, z].

theorem strictConvexOn_iff_slope_strict_mono_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} : StrictConvexOn 𝕜 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 [y, z].

theorem strictConcaveOn_iff_slope_strict_anti_adjacent {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} : StrictConcaveOn 𝕜 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 [y, z].

theorem ConvexOn.secant_mono_aux1 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

theorem ConvexOn.secant_mono_aux2 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 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 x) / (z - x)

theorem ConvexOn.secant_mono_aux3 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

theorem ConvexOn.secant_mono {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x ≤ y) : (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

If f : 𝕜 → 𝕜 is convex, then for any point a the slope of the secant line of f through a and b ≠ a is monotone with respect to b.

theorem StrictConvexOn.secant_strict_mono_aux1 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (z - x) * f y < (z - y) * f x + (y - x) * f z

theorem StrictConvexOn.secant_strict_mono_aux2 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConvexOn 𝕜 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 x) / (z - x)

theorem StrictConvexOn.secant_strict_mono_aux3 {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f z - f x) / (z - x) < (f z - f y) / (z - y)

theorem StrictConvexOn.secant_strict_mono {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConvexOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x < y) : (f x - f a) / (x - a) < (f y - f a) / (y - a)

If f : 𝕜 → 𝕜 is strictly convex, then for any point a the slope of the secant line of f through a and b is strictly monotone with respect to b.

theorem StrictConcaveOn.secant_strict_mono {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : StrictConcaveOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x < y) : (f y - f a) / (y - a) < (f x - f a) / (x - a)

If f : 𝕜 → 𝕜 is strictly concave, then for any point a the slope of the secant line of f through a and b is strictly antitone with respect to b.

theorem ConvexOn.strict_mono_of_lt {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 s f) {x y : 𝕜} (hx : x ∈ s) (hxy : x < y) (hxy' : f x < f y) : StrictMonoOn f (s ∩ Set.Ici 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, ∞).