Slope of a function

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] [AddCommGroup E] [Module k E] [AddTorsor 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.

theorem slope_fun_def {k : Type u_1} {E : Type u_2} {PE : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddTorsor E PE] (f : k → PE) : slope f = fun (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 = fun (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] [AddCommGroup E] [Module k E] [AddTorsor 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] [AddCommGroup 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] [AddCommGroup E] [Module k E] [AddTorsor 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] [AddCommGroup E] [Module k E] [AddTorsor 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] [AddCommGroup E] [Module k E] [AddTorsor E PE] (f : k → E) (c : PE) : (slope fun (x : k) => f x +ᵥ c) = slope f

@[simp]

theorem slope_sub_smul {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] (f : k → E) {a b : k} (h : a ≠ b) : slope (fun (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] [AddCommGroup E] [Module k E] [AddTorsor E PE] {f : k → PE} {a b : k} (h : slope f a b = 0) : f a = f b

theorem AffineMap.slope_comp {k : Type u_1} {E : Type u_2} {PE : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddTorsor E PE] {F : Type u_4} {PF : Type u_5} [AddCommGroup F] [Module k F] [AddTorsor F PF] (f : PE →ᵃ[k] PF) (g : k → PE) (a b : k) : slope (⇑f ∘ g) a b = f.linear (slope g a b)

theorem LinearMap.slope_comp {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] {F : Type u_4} [AddCommGroup 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] [AddCommGroup E] [Module k E] [AddTorsor E PE] (f : k → PE) (a b : k) : slope f a b = slope f b a

@[simp]

theorem slope_neg {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] (f : k → E) (x y : k) : slope (fun (t : k) => -f t) x y = -slope f x y

@[simp]

theorem slope_neg_fun {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] (f : k → E) : slope (-f) = -slope f

theorem slope_eq_zero_iff {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] {f : k → E} {a b : k} : slope f a b = 0 ↔ f a = f b

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] [AddCommGroup E] [Module k E] [AddTorsor 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 lineMap_slope_slope_sub_div_sub.

theorem lineMap_slope_slope_sub_div_sub {k : Type u_1} {E : Type u_2} {PE : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddTorsor E PE] (f : k → PE) (a b c : k) (h : a ≠ c) : (AffineMap.lineMap (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 lineMap to express this property.

theorem lineMap_slope_lineMap_slope_lineMap {k : Type u_1} {E : Type u_2} {PE : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddTorsor E PE] (f : k → PE) (a b r : k) : (AffineMap.lineMap (slope f ((AffineMap.lineMap a b) r) b) (slope f a ((AffineMap.lineMap a b) r))) r = slope f a b

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

theorem slope_nonneg_iff_of_le {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} (hxy : x ≤ y) : 0 ≤ slope f x y ↔ f x ≤ f y

theorem MonotoneOn.slope_nonneg {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} {s : Set k} (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : 0 ≤ slope f x y

theorem slope_nonpos_iff_of_le {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} (hxy : x ≤ y) : slope f x y ≤ 0 ↔ f y ≤ f x

theorem AntitoneOn.slope_nonpos {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} {s : Set k} (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : slope f x y ≤ 0

theorem slope_pos_iff_of_le {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} (hxy : x ≤ y) : 0 < slope f x y ↔ f x < f y

theorem StrictMonoOn.slope_pos {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} {s : Set k} (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : 0 < slope f x y

theorem slope_neg_iff_of_le {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} (hxy : x ≤ y) : slope f x y < 0 ↔ f y < f x

theorem StrictAntiOn.slope_neg {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} {s : Set k} (hf : StrictAntiOn f s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : slope f x y < 0