# Ordered modules as affine spaces #

In this file we prove some theorems about `slope` and `lineMap` in the case when the module `E` acting on the codomain `PE` of a function is an ordered module over its domain `k`. We also prove inequalities that can be used to link convexity of a function on an interval to monotonicity of the slope, see section docstring below for details.

## Implementation notes #

We do not introduce the notion of ordered affine spaces (yet?). Instead, we prove various theorems for an ordered module interpreted as an affine space.

## Tags #

affine space, ordered module, slope

### Monotonicity of `lineMap` #

In this section we prove that `lineMap a b r` is monotone (strictly or not) in its arguments if other arguments belong to specific domains.

source
theorem lineMap_mono_left {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a a' b : E} {r : k} (ha : a ≤ a') (hr : r ≤ 1) :
(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b) r
source
theorem lineMap_strict_mono_left {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a a' b : E} {r : k} (ha : a < a') (hr : r < 1) :
(AffineMap.lineMap a b) r < (AffineMap.lineMap a' b) r
source
theorem lineMap_mono_right {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b b' : E} {r : k} (hb : b ≤ b') (hr : 0 ≤ r) :
(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b') r
source
theorem lineMap_strict_mono_right {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b b' : E} {r : k} (hb : b < b') (hr : 0 < r) :
(AffineMap.lineMap a b) r < (AffineMap.lineMap a b') r
source
theorem lineMap_mono_endpoints {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a a' b b' : E} {r : k} (ha : a ≤ a') (hb : b ≤ b') (h₀ : 0 ≤ r) (h₁ : r ≤ 1) :
(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b') r
source
theorem lineMap_strict_mono_endpoints {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a a' b b' : E} {r : k} (ha : a < a') (hb : b < b') (h₀ : 0 ≤ r) (h₁ : r ≤ 1) :
(AffineMap.lineMap a b) r < (AffineMap.lineMap a' b') r
source
theorem lineMap_lt_lineMap_iff_of_lt {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r r' : k} [PosSMulReflectLT k E] (h : r < r') :
(AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ a < b
source
theorem left_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} [PosSMulReflectLT k E] (h : 0 < r) :
a < (AffineMap.lineMap a b) r ↔ a < b
source
theorem lineMap_lt_left_iff_lt {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} [PosSMulReflectLT k E] (h : 0 < r) :
(AffineMap.lineMap a b) r < a ↔ b < a
source
theorem lineMap_lt_right_iff_lt {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} [PosSMulReflectLT k E] (h : r < 1) :
(AffineMap.lineMap a b) r < b ↔ a < b
source
theorem right_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [Ring k] [PartialOrder k] [IsOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} [PosSMulReflectLT k E] (h : r < 1) :
b < (AffineMap.lineMap a b) r ↔ b < a
source
theorem lineMap_le_lineMap_iff_of_lt' {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r r' : k} (h : a < b) :
(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ r ≤ r'
source
theorem left_le_lineMap_iff_nonneg {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
a ≤ (AffineMap.lineMap a b) r ↔ 0 ≤ r
source
theorem lineMap_le_left_iff_nonpos {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
(AffineMap.lineMap a b) r ≤ a ↔ r ≤ 0
source
theorem right_le_lineMap_iff_one_le {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
b ≤ (AffineMap.lineMap a b) r ↔ 1 ≤ r
source
theorem lineMap_le_right_iff_le_one {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
(AffineMap.lineMap a b) r ≤ b ↔ r ≤ 1
source
theorem lineMap_lt_lineMap_iff_of_lt' {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r r' : k} (h : a < b) :
(AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ r < r'
source
theorem left_lt_lineMap_iff_pos {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
a < (AffineMap.lineMap a b) r ↔ 0 < r
source
theorem lineMap_lt_left_iff_neg {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
(AffineMap.lineMap a b) r < a ↔ r < 0
source
theorem right_lt_lineMap_iff_one_lt {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
b < (AffineMap.lineMap a b) r ↔ 1 < r
source
theorem lineMap_lt_right_iff_lt_one {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k} (h : a < b) :
(AffineMap.lineMap a b) r < b ↔ r < 1
source
theorem midpoint_le_midpoint {k : Type u_1} {E : Type u_2} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] {a a' b b' : E} [Invertible 2] (ha : a ≤ a') (hb : b ≤ b') :
midpoint k a b ≤ midpoint k a' b'
source
theorem lineMap_le_lineMap_iff_of_lt {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r r' : k} (h : r < r') :
(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ a ≤ b
source
theorem left_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k} (h : 0 < r) :
a ≤ (AffineMap.lineMap a b) r ↔ a ≤ b
source
@[simp]
theorem left_le_midpoint {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} :
a ≤ midpoint k a b ↔ a ≤ b
source
theorem lineMap_le_left_iff_le {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k} (h : 0 < r) :
(AffineMap.lineMap a b) r ≤ a ↔ b ≤ a
source
@[simp]
theorem midpoint_le_left {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} :
midpoint k a b ≤ a ↔ b ≤ a
source
theorem lineMap_le_right_iff_le {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k} (h : r < 1) :
(AffineMap.lineMap a b) r ≤ b ↔ a ≤ b
source
@[simp]
theorem midpoint_le_right {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} :
midpoint k a b ≤ b ↔ a ≤ b
source
theorem right_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k} (h : r < 1) :
b ≤ (AffineMap.lineMap a b) r ↔ b ≤ a
source
@[simp]
theorem right_le_midpoint {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} :
b ≤ midpoint k a b ↔ b ≤ a

### Convexity and slope #

Given an interval `[a, b]` and a point `c ∈ (a, b)`, `c = lineMap a b r`, there are a few ways to say that the point `(c, f c)` is above/below the segment `[(a, f a), (b, f b)]`:

- compare `f c` to `lineMap (f a) (f b) r`;
- compare `slope f a c` to `slope f a b`;
- compare `slope f c b` to `slope f a b`;
- compare `slope f a c` to `slope f c b`.

In this section we prove equivalence of these four approaches. In order to make the statements more readable, we introduce local notation `c = lineMap a b r`. Then we prove lemmas like

    lemma map_le_lineMap_iff_slope_le_slope_left (h : 0 < r * (b - a)) :
        f c ≤ lineMap (f a) (f b) r ↔ slope f a c ≤ slope f a b :=

For each inequality between `f c` and `lineMap (f a) (f b) r` we provide 3 lemmas:

- `*_left` relates it to an inequality on `slope f a c` and `slope f a b`;
- `*_right` relates it to an inequality on `slope f a b` and `slope f c b`;
- no-suffix version relates it to an inequality on `slope f a c` and `slope f c b`.

These inequalities can be used to restate `convexOn` in terms of monotonicity of the slope.

source
theorem map_le_lineMap_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) ≤ slope f a b

Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is non-strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f a b`.

source
theorem lineMap_le_map_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f a b ≤ slope f a ((AffineMap.lineMap a b) r)

Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is non-strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f a c`.

source
theorem map_lt_lineMap_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) < slope f a b

Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a c < slope f a b`.

source
theorem lineMap_lt_map_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f a b < slope f a ((AffineMap.lineMap a b) r)

Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f a b < slope f a c`.

source
theorem map_le_lineMap_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f ((AffineMap.lineMap a b) r) b

Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is non-strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f c b`.

source
theorem lineMap_le_map_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b ≤ slope f a b

Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is non-strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f c b ≤ slope f a b`.

source
theorem map_lt_lineMap_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a b < slope f ((AffineMap.lineMap a b) r) b

Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a b < slope f c b`.

source
theorem lineMap_lt_map_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b < slope f a b

Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a b`.

source
theorem map_le_lineMap_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) ≤ slope f ((AffineMap.lineMap a b) r) b

Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is non-strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f c b`.

source
theorem lineMap_le_map_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b ≤ slope f a ((AffineMap.lineMap a b) r)

Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is non-strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f c b ≤ slope f a c`.

source
theorem map_lt_lineMap_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) < slope f ((AffineMap.lineMap a b) r) b

Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is strictly below the segment `[(a, f a), (b, f b)]` if and only if `slope f a c < slope f c b`.

source
theorem lineMap_lt_map_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module k E] [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b < slope f a ((AffineMap.lineMap a b) r)

Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is strictly above the segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a c`.

source
theorem slope_pos_iff {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : x₀ < b) :
0 < slope f x₀ b ↔ f x₀ < f b
source
theorem slope_pos_iff_gt {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : b < x₀) :
0 < slope f x₀ b ↔ f b < f x₀
source
theorem pos_of_slope_pos {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : x₀ < b) (hbf : 0 < slope f x₀ b) (hf : f x₀ = 0) :
0 < f b
source
theorem neg_of_slope_pos {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : b < x₀) (hbf : 0 < slope f x₀ b) (hf : f x₀ = 0) :
f b < 0