From 569b8a44cc06afda34b7d8e11e5b03db527aed34 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 30 Oct 2023 15:05:20 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20Basic=20lemmas=20about=20positivity=20o?= =?UTF-8?q?f=20`a=20=E2=80=A2=20b`=20(#7647)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All lemmas and lemma names are taken from their `mul` counterpart. --- Mathlib/Algebra/Order/Module.lean | 44 ++++++++++++++++++++++++++++--- Mathlib/Algebra/Order/SMul.lean | 30 ++++++++++++++++++++- 2 files changed, 70 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean index 38413e037c287..029187d36b8a7 100644 --- a/Mathlib/Algebra/Order/Module.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/SMul.lean b/Mathlib/Algebra/Order/SMul.lean index 933dfff133ca6..0fb038c5d4f71 100644 --- a/Mathlib/Algebra/Order/SMul.lean +++ b/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