feat: n • v and v are on the same ray (#9104)

From LeanAPAP

Mathlib.lean

@@ -387,6 +387,7 @@ import Mathlib.Algebra.Order.Hom.Ring
 import Mathlib.Algebra.Order.Interval
 import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
+import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Algebra.Order.Module.Pointwise

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -167,6 +167,10 @@ theorem pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : M → M) := st
 #align pow_strict_mono_right' pow_left_strictMono
 #align nsmul_strict_mono_left nsmul_right_strictMono
 
+@[to_additive (attr := mono, gcongr) nsmul_lt_nsmul_right]
+lemma pow_lt_pow_left' (hn : n ≠ 0) {a b : M} (hab : a < b) : a ^ n < b ^ n :=
+  pow_left_strictMono hn hab
+
 end CovariantLTSwap
 
 section CovariantLESwap

Mathlib/Algebra/Order/Module/Algebra.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Order.Module.Defs
+
+/-!
+# Ordered algebras
+
+This file proves properties of algebras where both rings are ordered compatibly.
+
+### TODO
+
+`positivity` extension for `algebraMap`
+-/
+
+variable {α β : Type*} [OrderedCommSemiring α]
+
+section OrderedSemiring
+variable (β)
+variable [OrderedSemiring β] [Algebra α β] [SMulPosMono α β] {a : α}
+
+@[mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
+  fun a₁ a₂ ha ↦ by
+    simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one
+
+/-- A version of `algebraMap_mono` for use by `gcongr` since it currently does not preprocess
+`Monotone` conclusions. -/
+@[gcongr] protected lemma GCongr.algebraMap_le_algebraMap {a₁ a₂ : α} (ha : a₁ ≤ a₂) :
+    algebraMap α β a₁ ≤ algebraMap α β a₂ := algebraMap_mono _ ha
+
+lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by simpa using algebraMap_mono β ha
+
+end OrderedSemiring
+
+section StrictOrderedSemiring
+variable [StrictOrderedSemiring β] [Algebra α β]
+
+section SMulPosMono
+variable [SMulPosMono α β] [SMulPosReflectLE α β] {a₁ a₂ : α}
+
+@[simp] lemma algebraMap_le_algebraMap : algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂ := by
+  simp [Algebra.algebraMap_eq_smul_one]
+
+end SMulPosMono
+
+section SMulPosStrictMono
+variable [SMulPosStrictMono α β] {a a₁ a₂ : α}
+variable (β)
+
+@[mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
+  fun a₁ a₂ ha ↦ by
+    simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one
+
+/-- A version of `algebraMap_strictMono` for use by `gcongr` since it currently does not preprocess
+`Monotone` conclusions. -/
+@[gcongr] protected lemma GCongr.algebraMap_lt_algebraMap {a₁ a₂ : α} (ha : a₁ < a₂) :
+    algebraMap α β a₁ < algebraMap α β a₂ := algebraMap_strictMono _ ha
+
+lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a := by
+  simpa using algebraMap_strictMono β ha
+
+variable {β}
+variable [SMulPosReflectLT α β]
+
+@[simp] lemma algebraMap_lt_algebraMap : algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂ := by
+  simp [Algebra.algebraMap_eq_smul_one]
+
+end SMulPosStrictMono
+end StrictOrderedSemiring

Mathlib/Algebra/Order/Module/Defs.lean

@@ -1123,6 +1123,26 @@ lemma SMulPosReflectLT.lift [SMulPosReflectLT α γ] : SMulPosReflectLT α β wh
 
 end Lift
 
+section Nat
+
+instance OrderedSemiring.toPosSMulMonoNat [OrderedSemiring α] : PosSMulMono ℕ α where
+  elim _n _ _a _b hab := nsmul_le_nsmul_right hab _
+
+instance OrderedSemiring.toSMulPosMonoNat [OrderedSemiring α] : SMulPosMono ℕ α where
+  elim _a ha _m _n hmn := nsmul_le_nsmul_left ha hmn
+
+instance StrictOrderedSemiring.toPosSMulStrictMonoNat [StrictOrderedSemiring α] :
+    PosSMulStrictMono ℕ α where
+  elim _n hn _a _b hab := nsmul_right_strictMono hn.ne' hab
+
+instance StrictOrderedSemiring.toSMulPosStrictMonoNat [StrictOrderedSemiring α] :
+    SMulPosStrictMono ℕ α where
+  elim _a ha _m _n hmn := nsmul_lt_nsmul_left ha hmn
+
+end Nat
+
+-- TODO: Instances for `Int` and `Rat`
+
 namespace Mathlib.Meta.Positivity
 section OrderedSMul
 variable [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α}

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

@@ -458,7 +458,7 @@ theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) :
     have hx' : 0 < ‖x‖ := by simpa using hx
     have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity)
     have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb
-    simpa [hb'] using SameRay.sameRay_nonneg_smul_right x ha'
+    exact (SameRay.sameRay_nonneg_smul_right x ha').add_right $ by simp [hb']
   · intro h
     obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
     simp only [inner_smul_right, real_inner_self_eq_norm_sq, LinearMap.map_smulₛₗ,

Mathlib/Data/IsROrC/Basic.lean

@@ -733,6 +733,10 @@ theorem norm_natCast (n : ℕ) : ‖(n : K)‖ = n := by
 theorem norm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖(no_index (OfNat.ofNat n) : K)‖ = OfNat.ofNat n :=
   norm_natCast n
 
+variable (K) in
+lemma norm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖ = n • ‖x‖ := by
+  rw [nsmul_eq_smul_cast K, norm_smul, IsROrC.norm_natCast, nsmul_eq_mul]
+
 theorem mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z := by rw [normSq_eq_def', sq]
 #align is_R_or_C.mul_self_norm IsROrC.mul_self_norm
 

Mathlib/LinearAlgebra/Ray.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
+import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.GroupTheory.Subgroup.Actions
 import Mathlib.LinearAlgebra.LinearIndependent
 
@@ -114,47 +115,50 @@ theorem trans (hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y = 0 → x = 0
   rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
 #align same_ray.trans SameRay.trans
 
+variable {S : Type*} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R]
+  [IsScalarTower S R M] {a : S}
+
 /-- A vector is in the same ray as a nonnegative multiple of itself. -/
-theorem sameRay_nonneg_smul_right (v : M) {r : R} (h : 0 ≤ r) : SameRay R v (r • v) :=
-  Or.inr <|
-    h.eq_or_lt.imp (fun (h : 0 = r) => h ▸ zero_smul R v) fun h =>
-      ⟨r, 1, h, by
-        nontriviality R
-        exact zero_lt_one, (one_smul _ _).symm⟩
+lemma sameRay_nonneg_smul_right (v : M) (h : 0 ≤ a) : SameRay R v (a • v) := by
+  obtain h | h := (algebraMap_nonneg R h).eq_or_gt
+  · rw [← algebraMap_smul R a v, h, zero_smul]
+    exact zero_right _
+  · refine Or.inr $ Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩
+    rw [algebraMap_smul, one_smul]
 #align same_ray_nonneg_smul_right SameRay.sameRay_nonneg_smul_right
 
-/-- A vector is in the same ray as a positive multiple of itself. -/
-theorem sameRay_pos_smul_right (v : M) {r : R} (h : 0 < r) : SameRay R v (r • v) :=
-  sameRay_nonneg_smul_right v h.le
-#align same_ray_pos_smul_right SameRay.sameRay_pos_smul_right
-
-/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
-theorem nonneg_smul_right {r : R} (h : SameRay R x y) (hr : 0 ≤ r) : SameRay R x (r • y) :=
-  h.trans (sameRay_nonneg_smul_right y hr) fun hy => Or.inr <| by rw [hy, smul_zero]
-#align same_ray.nonneg_smul_right SameRay.nonneg_smul_right
-
-/-- A vector is in the same ray as a positive multiple of one it is in the same ray as. -/
-theorem pos_smul_right {r : R} (h : SameRay R x y) (hr : 0 < r) : SameRay R x (r • y) :=
-  h.nonneg_smul_right hr.le
-#align same_ray.pos_smul_right SameRay.pos_smul_right
-
 /-- A nonnegative multiple of a vector is in the same ray as that vector. -/
-theorem sameRay_nonneg_smul_left (v : M) {r : R} (h : 0 ≤ r) : SameRay R (r • v) v :=
-  (sameRay_nonneg_smul_right v h).symm
+lemma sameRay_nonneg_smul_left (v : M) (ha : 0 ≤ a) : SameRay R (a • v) v :=
+  (sameRay_nonneg_smul_right v ha).symm
 #align same_ray_nonneg_smul_left SameRay.sameRay_nonneg_smul_left
 
+/-- A vector is in the same ray as a positive multiple of itself. -/
+lemma sameRay_pos_smul_right (v : M) (ha : 0 < a) : SameRay R v (a • v) :=
+  sameRay_nonneg_smul_right v ha.le
+#align same_ray_pos_smul_right SameRay.sameRay_pos_smul_right
+
 /-- A positive multiple of a vector is in the same ray as that vector. -/
-theorem sameRay_pos_smul_left (v : M) {r : R} (h : 0 < r) : SameRay R (r • v) v :=
-  sameRay_nonneg_smul_left v h.le
+lemma sameRay_pos_smul_left (v : M) (ha : 0 < a) : SameRay R (a • v) v :=
+  sameRay_nonneg_smul_left v ha.le
 #align same_ray_pos_smul_left SameRay.sameRay_pos_smul_left
 
+/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
+lemma nonneg_smul_right (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y) :=
+  h.trans (sameRay_nonneg_smul_right y ha) fun hy => Or.inr <| by rw [hy, smul_zero]
+#align same_ray.nonneg_smul_right SameRay.nonneg_smul_right
+
 /-- A nonnegative multiple of a vector is in the same ray as one it is in the same ray as. -/
-theorem nonneg_smul_left {r : R} (h : SameRay R x y) (hr : 0 ≤ r) : SameRay R (r • x) y :=
-  (h.symm.nonneg_smul_right hr).symm
+lemma nonneg_smul_left (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y :=
+  (h.symm.nonneg_smul_right ha).symm
 #align same_ray.nonneg_smul_left SameRay.nonneg_smul_left
 
+/-- A vector is in the same ray as a positive multiple of one it is in the same ray as. -/
+theorem pos_smul_right (h : SameRay R x y) (ha : 0 < a) : SameRay R x (a • y) :=
+  h.nonneg_smul_right ha.le
+#align same_ray.pos_smul_right SameRay.pos_smul_right
+
 /-- A positive multiple of a vector is in the same ray as one it is in the same ray as. -/
-theorem pos_smul_left {r : R} (h : SameRay R x y) (hr : 0 < r) : SameRay R (r • x) y :=
+theorem pos_smul_left (h : SameRay R x y) (hr : 0 < a) : SameRay R (a • x) y :=
   h.nonneg_smul_left hr.le
 #align same_ray.pos_smul_left SameRay.pos_smul_left