mathlibdocumentation

linear_algebra.affine_space.ordered

Ordered modules as affine spaces #

In this file we prove some theorems about slope and line_map 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 line_map#

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

theorem line_map_mono_left {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a a' b : E} {r : k} (ha : a a') (hr : r 1) :
b) r b) r
theorem line_map_strict_mono_left {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a a' b : E} {r : k} (ha : a < a') (hr : r < 1) :
b) r < b) r
theorem line_map_mono_right {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b b' : E} {r : k} (hb : b b') (hr : 0 r) :
b) r b') r
theorem line_map_strict_mono_right {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b b' : E} {r : k} (hb : b < b') (hr : 0 < r) :
b) r < b') r
theorem line_map_mono_endpoints {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a a' b b' : E} {r : k} (ha : a a') (hb : b b') (h₀ : 0 r) (h₁ : r 1) :
b) r b') r
theorem line_map_strict_mono_endpoints {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a a' b b' : E} {r : k} (ha : a < a') (hb : b < b') (h₀ : 0 r) (h₁ : r 1) :
b) r < b') r
theorem line_map_lt_line_map_iff_of_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b : E} {r r' : k} (h : r < r') :
b) r < b) r' a < b
theorem left_lt_line_map_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b : E} {r : k} (h : 0 < r) :
a < b) r a < b
theorem line_map_lt_left_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b : E} {r : k} (h : 0 < r) :
b) r < a b < a
theorem line_map_lt_right_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b : E} {r : k} (h : r < 1) :
b) r < b a < b
theorem right_lt_line_map_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ E] [ E] {a b : E} {r : k} (h : r < 1) :
b < b) r b < a
theorem midpoint_le_midpoint {k : Type u_1} {E : Type u_2} [ E] [ E] [invertible 2] {a a' b b' : E} (ha : a a') (hb : b b') :
a b a' b'
theorem line_map_le_line_map_iff_of_lt {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} {r r' : k} (h : r < r') :
b) r b) r' a b
theorem left_le_line_map_iff_le {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} {r : k} (h : 0 < r) :
a b) r a b
@[simp]
theorem left_le_midpoint {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} :
a a b a b
theorem line_map_le_left_iff_le {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} {r : k} (h : 0 < r) :
b) r a b a
@[simp]
theorem midpoint_le_left {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} :
a b a b a
theorem line_map_le_right_iff_le {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} {r : k} (h : r < 1) :
b) r b a b
@[simp]
theorem midpoint_le_right {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} :
a b b a b
theorem right_le_line_map_iff_le {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} {r : k} (h : r < 1) :
b b) r b a
@[simp]
theorem right_le_midpoint {k : Type u_1} {E : Type u_2} [ E] [ E] {a b : E} :
b a b b a

Convexity and slope #

Given an interval [a, b] and a point c ∈ (a, b), c = line_map 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)]:

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

lemma map_le_line_map_iff_slope_le_slope_left (h : 0 < r * (b - a)) :
f c  line_map (f a) (f b) r  slope f a c  slope f a b :=

For each inequality between f c and line_map (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 by used in to restate convex_on in terms of monotonicity of the slope.

theorem map_le_line_map_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
f ( b) r) (affine_map.line_map (f a) (f b)) r a ( b) r) a b

Given c = line_map 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 line_map_le_map_iff_slope_le_slope_left {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
(affine_map.line_map (f a) (f b)) r f ( b) r) a b a ( b) r)

Given c = line_map 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_line_map_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
f ( b) r) < (affine_map.line_map (f a) (f b)) r a ( b) r) < a b

Given c = line_map 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 line_map_lt_map_iff_slope_lt_slope_left {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < r * (b - a)) :
(affine_map.line_map (f a) (f b)) r < f ( b) r) a b < a ( b) r)

Given c = line_map 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_line_map_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
f ( b) r) (affine_map.line_map (f a) (f b)) r a b ( b) r) b

Given c = line_map 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 line_map_le_map_iff_slope_le_slope_right {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
(affine_map.line_map (f a) (f b)) r f ( b) r) ( b) r) b a b

Given c = line_map 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_line_map_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
f ( b) r) < (affine_map.line_map (f a) (f b)) r a b < ( b) r) b

Given c = line_map 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 line_map_lt_map_iff_slope_lt_slope_right {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
(affine_map.line_map (f a) (f b)) r < f ( b) r) ( b) r) b < a b

Given c = line_map 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_line_map_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f ( b) r) (affine_map.line_map (f a) (f b)) r a ( b) r) ( b) r) b

Given c = line_map 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 line_map_le_map_iff_slope_le_slope {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
(affine_map.line_map (f a) (f b)) r f ( b) r) ( b) r) b a ( b) r)

Given c = line_map 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_line_map_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f ( b) r) < (affine_map.line_map (f a) (f b)) r a ( b) r) < ( b) r) b

Given c = line_map 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 line_map_lt_map_iff_slope_lt_slope {k : Type u_1} {E : Type u_2} [ E] [ E] {f : k → E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
(affine_map.line_map (f a) (f b)) r < f ( b) r) ( b) r) b < a ( b) r)

Given c = line_map 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.