mathlib documentation

linear_algebra.affine_space.ordered

Ordered modules as affine spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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) :
⇑(affine_map.line_map a b) r ≤ ⇑(affine_map.line_map a' b) r
source
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) :
⇑(affine_map.line_map a b) r < ⇑(affine_map.line_map a' b) r
source
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) :
⇑(affine_map.line_map a b) r ≤ ⇑(affine_map.line_map a b') r
source
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) :
⇑(affine_map.line_map a b) r < ⇑(affine_map.line_map a b') r
source
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) :
⇑(affine_map.line_map a b) r ≤ ⇑(affine_map.line_map a' b') r
source
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) :
⇑(affine_map.line_map a b) r < ⇑(affine_map.line_map a' b') r
source
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') :
⇑(affine_map.line_map a b) r < ⇑(affine_map.line_map a b) r' ↔ a < b
source
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) :
a < ⇑(affine_map.line_map a b) r ↔ a < b
source
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) :
⇑(affine_map.line_map a b) r < a ↔ b < a
source
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) :
⇑(affine_map.line_map a b) r < b ↔ a < b
source
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) :
b < ⇑(affine_map.line_map a b) r ↔ b < a
source
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'
source
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') :
⇑(affine_map.line_map a b) r ≤ ⇑(affine_map.line_map a b) r' ↔ a ≤ b
source
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) :
a ≤ ⇑(affine_map.line_map a b) r ↔ a ≤ b
source
@[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
source
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) :
⇑(affine_map.line_map a b) r ≤ a ↔ b ≤ a
source
@[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
source
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) :
⇑(affine_map.line_map a b) r ≤ b ↔ a ≤ b
source
@[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
source
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) :
b ≤ ⇑(affine_map.line_map a b) r ↔ b ≤ a
source
@[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.

source
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)) :
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 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 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)) :
⇑(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 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_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.

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

source
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)) :
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 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 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)) :
⇑(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 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_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.

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

source
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) :
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 (⇑(affine_map.line_map a 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.

source
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) :
⇑(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 (⇑(affine_map.line_map 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.

source
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) :
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 (⇑(affine_map.line_map a 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.

source
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) :
⇑(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 (⇑(affine_map.line_map 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.