# Documentation

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

theorem lineMap_mono_left {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {a' : E} {b : E} {r : k} (ha : a a') (hr : r 1) :
↑() r ↑() r
theorem lineMap_strict_mono_left {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {a' : E} {b : E} {r : k} (ha : a < a') (hr : r < 1) :
↑() r < ↑() r
theorem lineMap_mono_right {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {b' : E} {r : k} (hb : b b') (hr : 0 r) :
↑() r ↑() r
theorem lineMap_strict_mono_right {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {b' : E} {r : k} (hb : b < b') (hr : 0 < r) :
↑() r < ↑() r
theorem lineMap_mono_endpoints {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {a' : E} {b : E} {b' : E} {r : k} (ha : a a') (hb : b b') (h₀ : 0 r) (h₁ : r 1) :
↑() r ↑() r
theorem lineMap_strict_mono_endpoints {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {a' : E} {b : E} {b' : E} {r : k} (ha : a < a') (hb : b < b') (h₀ : 0 r) (h₁ : r 1) :
↑() r < ↑() r
theorem lineMap_lt_lineMap_iff_of_lt {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {r : k} {r' : k} (h : r < r') :
↑() r < ↑() r' a < b
theorem left_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {r : k} (h : 0 < r) :
a < ↑() r a < b
theorem lineMap_lt_left_iff_lt {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {r : k} (h : 0 < r) :
↑() r < a b < a
theorem lineMap_lt_right_iff_lt {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {r : k} (h : r < 1) :
↑() r < b a < b
theorem right_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [] [Module k E] [] {a : E} {b : E} {r : k} (h : r < 1) :
b < ↑() r b < a
theorem midpoint_le_midpoint {k : Type u_1} {E : Type u_2} [Module k E] [] [] {a : E} {a' : E} {b : E} {b' : E} (ha : a a') (hb : b b') :
midpoint k a b midpoint k a' b'
theorem lineMap_le_lineMap_iff_of_lt {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} {r : k} {r' : k} (h : r < r') :
↑() r ↑() r' a b
theorem left_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} {r : k} (h : 0 < r) :
a ↑() r a b
@[simp]
theorem left_le_midpoint {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} :
a midpoint k a b a b
theorem lineMap_le_left_iff_le {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} {r : k} (h : 0 < r) :
↑() r a b a
@[simp]
theorem midpoint_le_left {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} :
midpoint k a b a b a
theorem lineMap_le_right_iff_le {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} {r : k} (h : r < 1) :
↑() r b a b
@[simp]
theorem midpoint_le_right {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} :
midpoint k a b b a b
theorem right_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {b : E} {r : k} (h : r < 1) :
b ↑() r b a
@[simp]
theorem right_le_midpoint {k : Type u_1} {E : Type u_2} [Module k E] [] {a : E} {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.

theorem map_le_lineMap_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < r * (b - a)) :
f (↑() r) ↑(AffineMap.lineMap (f a) (f b)) r slope f a (↑() 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.

theorem lineMap_le_map_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < r * (b - a)) :
↑(AffineMap.lineMap (f a) (f b)) r f (↑() r) slope f a b slope f a (↑() 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.

theorem map_lt_lineMap_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < r * (b - a)) :
f (↑() r) < ↑(AffineMap.lineMap (f a) (f b)) r slope f a (↑() 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.

theorem lineMap_lt_map_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < r * (b - a)) :
↑(AffineMap.lineMap (f a) (f b)) r < f (↑() r) slope f a b < slope f a (↑() 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.

theorem map_le_lineMap_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < (1 - r) * (b - a)) :
f (↑() r) ↑(AffineMap.lineMap (f a) (f b)) r slope f a b slope f (↑() 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.

theorem lineMap_le_map_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < (1 - r) * (b - a)) :
↑(AffineMap.lineMap (f a) (f b)) r f (↑() r) slope f (↑() 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.

theorem map_lt_lineMap_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < (1 - r) * (b - a)) :
f (↑() r) < ↑(AffineMap.lineMap (f a) (f b)) r slope f a b < slope f (↑() 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.

theorem lineMap_lt_map_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (h : 0 < (1 - r) * (b - a)) :
↑(AffineMap.lineMap (f a) (f b)) r < f (↑() r) slope f (↑() 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.

theorem map_le_lineMap_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f (↑() r) ↑(AffineMap.lineMap (f a) (f b)) r slope f a (↑() r) slope f (↑() 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.

theorem lineMap_le_map_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
↑(AffineMap.lineMap (f a) (f b)) r f (↑() r) slope f (↑() r) b slope f a (↑() 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.

theorem map_lt_lineMap_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f (↑() r) < ↑(AffineMap.lineMap (f a) (f b)) r slope f a (↑() r) < slope f (↑() 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.

theorem lineMap_lt_map_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [Module k E] [] {f : kE} {a : k} {b : k} {r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
↑(AffineMap.lineMap (f a) (f b)) r < f (↑() r) slope f (↑() r) b < slope f a (↑() 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.