mathlib documentation

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] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a a' b : E} {r : k} (ha : a a') (hr : r 1) :
theorem line_map_strict_mono_left {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a a' b : E} {r : k} (ha : a < a') (hr : r < 1) :
theorem line_map_mono_right {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b b' : E} {r : k} (hb : b b') (hr : 0 r) :
theorem line_map_strict_mono_right {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b b' : E} {r : k} (hb : b < b') (hr : 0 < r) :
theorem line_map_mono_endpoints {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a a' b b' : E} {r : k} (ha : a a') (hb : b b') (h₀ : 0 r) (h₁ : r 1) :
theorem line_map_strict_mono_endpoints {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a a' b b' : E} {r : k} (ha : a < a') (hb : b < b') (h₀ : 0 r) (h₁ : r 1) :
theorem line_map_lt_line_map_iff_of_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r r' : k} (h : r < r') :
theorem left_lt_line_map_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : 0 < r) :
theorem line_map_lt_left_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : 0 < r) :
theorem line_map_lt_right_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : r < 1) :
theorem right_lt_line_map_iff_lt {k : Type u_1} {E : Type u_2} [ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : r < 1) :
theorem midpoint_le_midpoint {k : Type u_1} {E : Type u_2} [linear_ordered_ring k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] [invertible 2] {a a' b b' : E} (ha : a a') (hb : b b') :
midpoint k a b midpoint k a' b'
theorem line_map_le_line_map_iff_of_lt {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r r' : k} (h : r < r') :
theorem left_le_line_map_iff_le {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : 0 < r) :
@[simp]
theorem left_le_midpoint {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} :
a midpoint k a b a b
theorem line_map_le_left_iff_le {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : 0 < r) :
@[simp]
theorem midpoint_le_left {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} :
midpoint k a b a b a
theorem line_map_le_right_iff_le {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : r < 1) :
@[simp]
theorem midpoint_le_right {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} :
midpoint k a b b a b
theorem right_le_line_map_iff_le {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {a b : E} {r : k} (h : r < 1) :
@[simp]
theorem right_le_midpoint {k : Type u_1} {E : Type u_2} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul 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 = 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:

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < r * (b - a)) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < r * (b - a)) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < r * (b - a)) :
f ((affine_map.line_map a b) r) < (affine_map.line_map (f a) (f b)) r slope f a ((affine_map.line_map a b) r) < slope f 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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < r * (b - a)) :
(affine_map.line_map (f a) (f b)) r < f ((affine_map.line_map a b) r) slope f a b < slope f a ((affine_map.line_map 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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
f ((affine_map.line_map a b) r) < (affine_map.line_map (f a) (f b)) r slope f a b < slope f ((affine_map.line_map a 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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (h : 0 < (1 - r) * (b - a)) :
(affine_map.line_map (f a) (f b)) r < f ((affine_map.line_map a b) r) slope f ((affine_map.line_map a b) r) b < slope f 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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :

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} [linear_ordered_field k] [ordered_add_comm_group E] [module k E] [ordered_smul k E] {f : k E} {a b r : k} (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :

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.