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} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a a' b : E} {r : k} (ha : a ≤ a') (hr : r ≤ 1) : (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b) r

theorem lineMap_strict_mono_left {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a a' b : E} {r : k} (ha : a < a') (hr : r < 1) : (AffineMap.lineMap a b) r < (AffineMap.lineMap a' b) r

theorem lineMap_mono_right {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b b' : E} {r : k} (hb : b ≤ b') (hr : 0 ≤ r) : (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b') r

theorem lineMap_strict_mono_right {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b b' : E} {r : k} (hb : b < b') (hr : 0 < r) : (AffineMap.lineMap a b) r < (AffineMap.lineMap a b') r

theorem lineMap_mono_endpoints {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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

theorem lineMap_strict_mono_endpoints {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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

theorem lineMap_lt_lineMap_iff_of_lt {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r r' : k} (h : r < r') : (AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ a < b

theorem left_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : 0 < r) : a < (AffineMap.lineMap a b) r ↔ a < b

theorem lineMap_lt_left_iff_lt {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : 0 < r) : (AffineMap.lineMap a b) r < a ↔ b < a

theorem lineMap_lt_right_iff_lt {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : r < 1) : (AffineMap.lineMap a b) r < b ↔ a < b

theorem right_lt_lineMap_iff_lt {k : Type u_1} {E : Type u_2} [OrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : r < 1) : b < (AffineMap.lineMap a b) r ↔ b < a

theorem midpoint_le_midpoint {k : Type u_1} {E : Type u_2} [LinearOrderedRing k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] [Invertible 2] {a a' b 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} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r r' : k} (h : r < r') : (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ a ≤ b

theorem left_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : 0 < r) : a ≤ (AffineMap.lineMap a b) r ↔ a ≤ b

@[simp]

theorem left_le_midpoint {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} : a ≤ midpoint k a b ↔ a ≤ b

theorem lineMap_le_left_iff_le {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : 0 < r) : (AffineMap.lineMap a b) r ≤ a ↔ b ≤ a

@[simp]

theorem midpoint_le_left {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} : midpoint k a b ≤ a ↔ b ≤ a

theorem lineMap_le_right_iff_le {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : r < 1) : (AffineMap.lineMap a b) r ≤ b ↔ a ≤ b

@[simp]

theorem midpoint_le_right {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} : midpoint k a b ≤ b ↔ a ≤ b

theorem right_le_lineMap_iff_le {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul k E] {a b : E} {r : k} (h : r < 1) : b ≤ (AffineMap.lineMap a b) r ↔ b ≤ a

@[simp]

theorem right_le_midpoint {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_le_lineMap_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_le_map_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_lt_lineMap_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_lt_map_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_le_lineMap_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_le_map_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_lt_lineMap_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_lt_map_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_le_lineMap_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_le_map_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem map_lt_lineMap_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.

theorem lineMap_lt_map_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup E] [Module k E] [OrderedSMul 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.