feat: Basic lemmas about positivity of a • b (#7647)

All lemmas and lemma names are taken from their `mul` counterpart.

Mathlib/Algebra/Order/Module.lean

@@ -24,7 +24,7 @@ ordered module, ordered scalar, ordered smul, ordered action, ordered vector spa
 
 open Pointwise
 
-variable {k M N : Type*}
+variable {ι k M N : Type*}
 
 instance instModuleOrderDual [Semiring k] [OrderedAddCommMonoid M] [Module k M] : Module k Mᵒᵈ
     where
@@ -48,7 +48,7 @@ end Semiring
 
 section Ring
 
-variable [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a b : M} {c : k}
+variable [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a b : M} {c d : k}
 
 theorem smul_lt_smul_of_neg (h : a < b) (hc : c < 0) : c • b < c • a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
@@ -70,6 +70,12 @@ theorem lt_of_smul_lt_smul_of_nonpos (h : c • a < c • b) (hc : c ≤ 0) : b
   exact lt_of_smul_lt_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
 #align lt_of_smul_lt_smul_of_nonpos lt_of_smul_lt_smul_of_nonpos
 
+lemma smul_le_smul_of_nonneg_right (h : c ≤ d) (hb : 0 ≤ b) : c • b ≤ d • b := by
+  rw [←sub_nonneg, ←sub_smul]; exact smul_nonneg (sub_nonneg.2 h) hb
+
+lemma smul_le_smul (hcd : c ≤ d) (hab : a ≤ b) (ha : 0 ≤ a) (hd : 0 ≤ d) : c • a ≤ d • b :=
+  (smul_le_smul_of_nonneg_right hcd ha).trans $ smul_le_smul_of_nonneg_left hab hd
+
 theorem smul_lt_smul_iff_of_neg (hc : c < 0) : c • a < c • b ↔ b < a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
   exact smul_lt_smul_iff_of_pos (neg_pos_of_neg hc)
@@ -218,7 +224,8 @@ theorem BddAbove.smul_of_nonpos (hc : c ≤ 0) (hs : BddAbove s) : BddBelow (c 
 end OrderedRing
 
 section LinearOrderedRing
-variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k}
+variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M]
+  {f : ι → k} {g : ι → M} {s : Set ι} {a a₁ a₂ : k} {b b₁ b₂ : M}
 
 theorem smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • max b₁ b₂ = min (a • b₁) (a • b₂) :=
   (antitone_smul_left ha : Antitone (_ : M → M)).map_max
@@ -228,6 +235,37 @@ theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • min b₁ b₂
   (antitone_smul_left ha : Antitone (_ : M → M)).map_min
 #align smul_min_of_nonpos smul_min_of_nonpos
 
+lemma nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg (hab : 0 ≤ a • b) :
+    0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
+  simp only [Decidable.or_iff_not_and_not, not_and, not_le]
+  refine fun ab nab ↦ hab.not_lt ?_
+  obtain ha | rfl | ha := lt_trichotomy 0 a
+  exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim,
+    smul_neg_of_neg_of_pos ha (nab ha.le)]
+
+lemma smul_nonneg_iff : 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
+  ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg,
+    fun h ↦ h.elim (and_imp.2 smul_nonneg) (and_imp.2 smul_nonneg_of_nonpos_of_nonpos)⟩
+
+lemma smul_nonpos_iff : a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
+  rw [←neg_nonneg, ←smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
+
+lemma smul_nonneg_iff_pos_imp_nonneg : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) := by
+  refine smul_nonneg_iff.trans ?_
+  simp_rw [←not_le, ←or_iff_not_imp_left]
+  have := le_total a 0
+  have := le_total b 0
+  tauto
+
+lemma smul_nonneg_iff_neg_imp_nonpos : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) := by
+  rw [←neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]
+
+lemma smul_nonpos_iff_pos_imp_nonpos : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) := by
+  rw [←neg_nonneg, ←smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]
+
+lemma smul_nonpos_iff_neg_imp_nonneg : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) := by
+  rw [←neg_nonneg, ←neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]
+
 end LinearOrderedRing
 
 section LinearOrderedField

Mathlib/Algebra/Order/SMul.lean

@@ -53,7 +53,7 @@ class OrderedSMul (R M : Type*) [OrderedSemiring R] [OrderedAddCommMonoid M] [SM
   protected lt_of_smul_lt_smul_of_pos : ∀ {a b : M}, ∀ {c : R}, c • a < c • b → 0 < c → a < b
 #align ordered_smul OrderedSMul
 
-variable {ι 𝕜 R M N : Type*}
+variable {ι α β γ 𝕜 R M N : Type*}
 
 namespace OrderDual
 
@@ -63,11 +63,36 @@ instance OrderDual.instSMulWithZero [Zero R] [AddZeroClass M] [SMulWithZero R M]
     zero_smul := fun m => OrderDual.rec (zero_smul _) m
     smul_zero := fun r => OrderDual.rec (@smul_zero R M _ _) r }
 
+@[to_additive]
 instance OrderDual.instMulAction [Monoid R] [MulAction R M] : MulAction R Mᵒᵈ :=
   { OrderDual.instSMul with
     one_smul := fun m => OrderDual.rec (one_smul _) m
     mul_smul := fun r => OrderDual.rec (@mul_smul R M _ _) r }
 
+@[to_additive]
+instance OrderDual.instSMulCommClass [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
+    SMulCommClass αᵒᵈ β γ := ‹SMulCommClass α β γ›
+
+@[to_additive]
+instance OrderDual.instSMulCommClass' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
+    SMulCommClass α βᵒᵈ γ := ‹SMulCommClass α β γ›
+
+@[to_additive]
+instance OrderDual.instSMulCommClass'' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
+    SMulCommClass α β γᵒᵈ := ‹SMulCommClass α β γ›
+
+@[to_additive OrderDual.instVAddAssocClass]
+instance OrderDual.instIsScalarTower [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+   IsScalarTower αᵒᵈ β γ := ‹IsScalarTower α β γ›
+
+@[to_additive OrderDual.instVAddAssocClass']
+instance OrderDual.instIsScalarTower' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+    IsScalarTower α βᵒᵈ γ := ‹IsScalarTower α β γ›
+
+@[to_additive OrderDual.instVAddAssocClass'']
+instance OrderDual.IsScalarTower'' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+    IsScalarTower α β γᵒᵈ := ‹IsScalarTower α β γ›
+
 instance [MonoidWithZero R] [AddMonoid M] [MulActionWithZero R M] : MulActionWithZero R Mᵒᵈ :=
   { OrderDual.instMulAction, OrderDual.instSMulWithZero with }
 
@@ -99,6 +124,9 @@ variable [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [Ordere
     · exact (smul_lt_smul_of_pos hab hc).le
 #align smul_le_smul_of_nonneg smul_le_smul_of_nonneg
 
+-- TODO: Remove `smul_le_smul_of_nonneg` completely
+alias smul_le_smul_of_nonneg_left := smul_le_smul_of_nonneg
+
 theorem smul_nonneg (hc : 0 ≤ c) (ha : 0 ≤ a) : 0 ≤ c • a :=
   calc
     (0 : M) = c • (0 : M) := (smul_zero c).symm