From 12b6b9934acbaa35f11df4fb8eb886b770657ff0 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 13 Jan 2022 06:20:13 +0000 Subject: [PATCH] refactor(linear_algebra/affine_space): move def of `slope` to a new file (#11361) Also add a few trivial lemmas. --- src/linear_algebra/affine_space/ordered.lean | 88 +-------------- src/linear_algebra/affine_space/slope.lean | 107 +++++++++++++++++++ 2 files changed, 112 insertions(+), 83 deletions(-) create mode 100644 src/linear_algebra/affine_space/slope.lean diff --git a/src/linear_algebra/affine_space/ordered.lean b/src/linear_algebra/affine_space/ordered.lean index 9d4bde8d5650a..ff698c31ad8da 100644 --- a/src/linear_algebra/affine_space/ordered.lean +++ b/src/linear_algebra/affine_space/ordered.lean @@ -5,17 +5,15 @@ Authors: Yury G. Kudryashov -/ import algebra.order.module import linear_algebra.affine_space.midpoint +import linear_algebra.affine_space.slope import tactic.field_simp /-! # 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.function` to link convexity of a function on an interval to monotonicity of the +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 @@ -32,81 +30,6 @@ open affine_map variables {k E PE : Type*} -/-! -### 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. -/ - -section no_order - -variables [field k] [add_comm_group E] [module k E] [add_torsor E PE] - -include 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`. -/ -def slope (f : k → PE) (a b : k) : E := (b - a)⁻¹ • (f b -ᵥ f a) - -omit E - -lemma slope_def_field (f : k → k) (a b : k) : slope f a b = (f b - f a) / (b - a) := -div_eq_inv_mul.symm - -@[simp] lemma slope_same (f : k → PE) (a : k) : (slope f a a : E) = 0 := -by rw [slope, sub_self, inv_zero, zero_smul] - -include E - -lemma eq_of_slope_eq_zero {f : k → PE} {a b : k} (h : slope f a b = (0:E)) : f a = f b := -begin - rw [slope, smul_eq_zero, inv_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq] at h, - exact h.elim (λ h, h ▸ rfl) eq.symm -end - -lemma slope_comm (f : k → PE) (a b : k) : slope f a b = slope f b a := -by rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub] - -/-- `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`. -/ -lemma sub_div_sub_smul_slope_add_sub_div_sub_smul_slope (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 := -begin - by_cases hab : a = b, - { subst hab, - rw [sub_self, zero_div, zero_smul, zero_add], - by_cases hac : a = c, - { simp [hac] }, - { rw [div_self (sub_ne_zero.2 $ ne.symm hac), one_smul] } }, - by_cases hbc : b = c, { subst hbc, simp [sub_ne_zero.2 (ne.symm hab)] }, - rw [add_comm], - simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add, - smul_inv_smul₀ (sub_ne_zero.2 $ ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 $ ne.symm hbc), - vsub_add_vsub_cancel], -end - -/-- `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. -/ -lemma line_map_slope_slope_sub_div_sub (f : k → PE) (a b c : k) (h : a ≠ c) : - line_map (slope f a b) (slope f b c) ((c - b) / (c - a)) = slope f a c := -by field_simp [sub_ne_zero.2 h.symm, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c, - line_map_apply_module] - -/-- `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. -/ -lemma line_map_slope_line_map_slope_line_map (f : k → PE) (a b r : k) : - line_map (slope f (line_map a b r) b) (slope f a (line_map a b r)) r = slope f a b := -begin - obtain (rfl|hab) : a = b ∨ a ≠ b := classical.em _, { simp }, - rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b], - convert line_map_slope_slope_sub_div_sub f b (line_map a b r) a hab.symm using 2, - rw [line_map_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub, - sub_sub_cancel] -end - -end no_order - /-! ### Monotonicity of `line_map` @@ -263,8 +186,7 @@ For each inequality between `f c` and `line_map (f a) (f b) r` we provide 3 lemm * `*_right` relates it to an inequality on `slope f a b` and `slope f c b`; * no-suffix version relates it to an inequality on `slope f a c` and `slope f c b`. -Later these inequalities will be used in to restate `convex_on` in terms of monotonicity of the -slope. +These inequalities can by used in to restate `convex_on` in terms of monotonicity of the slope. -/ variables {f : k → E} {a b r : k} diff --git a/src/linear_algebra/affine_space/slope.lean b/src/linear_algebra/affine_space/slope.lean new file mode 100644 index 0000000000000..11b0a3469a573 --- /dev/null +++ b/src/linear_algebra/affine_space/slope.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2020 Yury G. Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury G. Kudryashov +-/ +import algebra.order.module +import linear_algebra.affine_space.affine_map +import tactic.field_simp + +/-! +# 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 +-/ + +open affine_map +variables {k E PE : Type*} [field k] [add_comm_group E] [module k E] [add_torsor E PE] + +include 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`. -/ +def slope (f : k → PE) (a b : k) : E := (b - a)⁻¹ • (f b -ᵥ f a) + +omit E + +lemma slope_def_field (f : k → k) (a b : k) : slope f a b = (f b - f a) / (b - a) := +div_eq_inv_mul.symm + +@[simp] lemma slope_same (f : k → PE) (a : k) : (slope f a a : E) = 0 := +by rw [slope, sub_self, inv_zero, zero_smul] + +include E + +lemma slope_def_module (f : k → E) (a b : k) : slope f a b = (b - a)⁻¹ • (f b - f a) := rfl + +@[simp] lemma sub_smul_slope (f : k → PE) (a b : k) : (b - a) • slope f a b = f b -ᵥ f a := +begin + rcases eq_or_ne a b with rfl | hne, + { rw [sub_self, zero_smul, vsub_self] }, + { rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)] } +end + +lemma sub_smul_slope_vadd (f : k → PE) (a b : k) : (b - a) • slope f a b +ᵥ f a = f b := +by rw [sub_smul_slope, vsub_vadd] + +@[simp] lemma slope_vadd_const (f : k → E) (c : PE) : + slope (λ x, f x +ᵥ c) = slope f := +begin + ext a b, + simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub] +end + +@[simp] lemma slope_sub_smul (f : k → E) {a b : k} (h : a ≠ b): + slope (λ x, (x - a) • f x) a b = f b := +by simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)] + +lemma eq_of_slope_eq_zero {f : k → PE} {a b : k} (h : slope f a b = (0:E)) : f a = f b := +by rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd] + +lemma slope_comm (f : k → PE) (a b : k) : slope f a b = slope f b a := +by rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub] + +/-- `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`. -/ +lemma sub_div_sub_smul_slope_add_sub_div_sub_smul_slope (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 := +begin + by_cases hab : a = b, + { subst hab, + rw [sub_self, zero_div, zero_smul, zero_add], + by_cases hac : a = c, + { simp [hac] }, + { rw [div_self (sub_ne_zero.2 $ ne.symm hac), one_smul] } }, + by_cases hbc : b = c, { subst hbc, simp [sub_ne_zero.2 (ne.symm hab)] }, + rw [add_comm], + simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add, + smul_inv_smul₀ (sub_ne_zero.2 $ ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 $ ne.symm hbc), + vsub_add_vsub_cancel], +end + +/-- `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. -/ +lemma line_map_slope_slope_sub_div_sub (f : k → PE) (a b c : k) (h : a ≠ c) : + line_map (slope f a b) (slope f b c) ((c - b) / (c - a)) = slope f a c := +by field_simp [sub_ne_zero.2 h.symm, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c, + line_map_apply_module] + +/-- `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. -/ +lemma line_map_slope_line_map_slope_line_map (f : k → PE) (a b r : k) : + line_map (slope f (line_map a b r) b) (slope f a (line_map a b r)) r = slope f a b := +begin + obtain (rfl|hab) : a = b ∨ a ≠ b := classical.em _, { simp }, + rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b], + convert line_map_slope_slope_sub_div_sub f b (line_map a b r) a hab.symm using 2, + rw [line_map_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub, + sub_sub_cancel] +end