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.
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)]
:
- compare
f c
toline_map (f a) (f b) r
; - compare
slope f a c
toslope
f a b`; - compare
slope f c b
toslope f a b
; - compare
slope f a c
toslope 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 = 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 onslope f a c
andslope f a b
;*_right
relates it to an inequality onslope f a b
andslope f c b
;- no-suffix version relates it to an inequality on
slope f a c
andslope f c b
.
These inequalities can by used in to restate convex_on
in terms of monotonicity of the slope.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.