mathlib documentation

linear_algebra.affine_space.ordered

Ordered modules as affine spaces #

In this file we define the slope of a function f : k → PE taking values in an affine space over k and prove some theorems about slope and line_map in the case when PE is an ordered module over k. The slope function naturally appears in the Mean Value Theorem, and in the proof of the fact that a function with nonnegative second derivative on an interval is convex on this interval. In the third part of this file we prove inequalities that will be used in analysis.convex.basic 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

Definition of slope and basic properties #

In this section we define slope f a b and prove some properties that do not require order on the codomain.

source
def slope {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a b : k) :
E

slope f a b = (b - a)⁻¹ • (f b -ᵥ f a) is the slope of a function f on the interval [a, b]. Note that slope f a a = 0, not the derivative of f at a.

Equations
source
theorem slope_def_field {k : Type u_1} [field k] (f : k → k) (a b : k) :
slope f a b = (f b - f a) / (b - a)
source
@[simp]
theorem slope_same {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a : k) :
slope f a a = 0
source
theorem eq_of_slope_eq_zero {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] {f : k → PE} {a b : k} (h : slope f a b = 0) :
f a = f b
source
theorem slope_comm {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a b : k) :
slope f a b = slope f b a
source
theorem sub_div_sub_smul_slope_add_sub_div_sub_smul_slope {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a b c : k) :
((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

slope f a c is a linear combination of slope f a b and slope f b c. This version explicitly provides coefficients. If a ≠ c, then the sum of the coefficients is 1, so it is actually an affine combination, see line_map_slope_slope_sub_div_sub.

source
theorem line_map_slope_slope_sub_div_sub {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a b c : k) (h : a ≠ c) :
⇑(affine_map.line_map (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c

slope f a c is an affine combination of slope f a b and slope f b c. This version uses line_map to express this property.

source
theorem line_map_slope_line_map_slope_line_map {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [affine_space E PE] (f : k → PE) (a b r : k) :
⇑(affine_map.line_map (slope f (⇑(affine_map.line_map a b) r) b) (slope f a (⇑(affine_map.line_map a b) r))) r = slope f a b

slope f a b is an affine combination of slope f a (line_map a b r) and slope f (line_map a b r) b. We use line_map to express this property.

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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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:

Later these inequalities will be 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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_module 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.