mathlib3 documentation

linear_algebra.affine_space.slope

Slope of a function #

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

In this file we define the slope of a function f : k → PE taking values in an affine space over k and prove some basic theorems about slope. 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.

Tags #

affine space, slope

def slope {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor 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
theorem slope_fun_def {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] (f : k PE) :
slope f = λ (a b : k), (b - a)⁻¹ (f b -ᵥ f a)
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)
theorem slope_fun_def_field {k : Type u_1} [field k] (f : k k) (a : k) :
slope f a = λ (b : k), (f b - f a) / (b - a)
@[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] [add_torsor E PE] (f : k PE) (a : k) :
slope f a a = 0
theorem slope_def_module {k : Type u_1} {E : Type u_2} [field k] [add_comm_group E] [module k E] (f : k E) (a b : k) :
slope f a b = (b - a)⁻¹ (f b - f a)
@[simp]
theorem sub_smul_slope {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] (f : k PE) (a b : k) :
(b - a) slope f a b = f b -ᵥ f a
theorem sub_smul_slope_vadd {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] (f : k PE) (a b : k) :
(b - a) slope f a b +ᵥ f a = f b
@[simp]
theorem slope_vadd_const {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] (f : k E) (c : PE) :
slope (λ (x : k), f x +ᵥ c) = slope f
@[simp]
theorem slope_sub_smul {k : Type u_1} {E : Type u_2} [field k] [add_comm_group E] [module k E] (f : k E) {a b : k} (h : a b) :
slope (λ (x : k), (x - a) f x) a b = f b
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] [add_torsor E PE] {f : k PE} {a b : k} (h : slope f a b = 0) :
f a = f b
theorem affine_map.slope_comp {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] {F : Type u_4} {PF : Type u_5} [add_comm_group F] [module k F] [add_torsor F PF] (f : PE →ᵃ[k] PF) (g : k PE) (a b : k) :
slope (f g) a b = (f.linear) (slope g a b)
theorem linear_map.slope_comp {k : Type u_1} {E : Type u_2} [field k] [add_comm_group E] [module k E] {F : Type u_3} [add_comm_group F] [module k F] (f : E →ₗ[k] F) (g : k E) (a b : k) :
slope (f g) a b = f (slope g a b)
theorem slope_comm {k : Type u_1} {E : Type u_2} {PE : Type u_3} [field k] [add_comm_group E] [module k E] [add_torsor E PE] (f : k PE) (a b : k) :
slope f a b = slope f b a
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] [add_torsor 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.

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] [add_torsor 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.

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] [add_torsor E PE] (f : k PE) (a b r : k) :

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.