[Merged by Bors] - refactor(linear_algebra/affine_space): move def of slope to a new file

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}

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