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
semimodule 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 semimodule interpreted as an affine space.
Tags #
affine space, ordered semimodule, 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.
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
.
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
.
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.
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.
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
.
Later these inequalities will be 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
.