From 1deb0dc0ac952ae64886ac64f3b55dd77cd80a05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 28 Aug 2024 11:50:02 +0000 Subject: [PATCH] fix more --- LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean | 19 ++++++++++++++----- .../Mathlib/Algebra/Group/Action/Defs.lean | 6 ++++++ .../Mathlib/Algebra/Order/Module/Defs.lean | 4 ++++ LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean | 12 ++++++------ LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean | 6 +++++- 5 files changed, 35 insertions(+), 12 deletions(-) create mode 100644 LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean create mode 100644 LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean diff --git a/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean b/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean index 73291f6f08..ddc8d7ad6f 100644 --- a/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean +++ b/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean @@ -1,17 +1,26 @@ import Mathlib.Algebra.Algebra.Rat +import Mathlib.Algebra.Module.Basic -variable {α : Type*} +variable {α β : Type*} -instance [Semiring α] [Module ℚ≥0 α] : SMulCommClass ℚ≥0 α α where - smul_comm q a b := sorry +instance [Monoid α] [AddCommMonoid β] [Module ℚ≥0 β] [DistribMulAction α β] : + SMulCommClass ℚ≥0 α β where + smul_comm q a b := by + rw [← q.num_div_den, div_eq_mul_inv] + simp_rw [mul_smul, inv_natCast_smul_comm, Nat.cast_smul_eq_nsmul] + rw [smul_comm a q.num] instance [Semiring α] [Module ℚ≥0 α] : SMulCommClass α ℚ≥0 α := .symm .. instance [Semiring α] [Module ℚ≥0 α] : IsScalarTower ℚ≥0 α α where smul_assoc q a b := sorry -instance [Ring α] [Module ℚ α] : SMulCommClass ℚ α α where - smul_comm q a b := sorry +instance [Monoid α] [AddCommGroup β] [Module ℚ β] [DistribMulAction α β] : + SMulCommClass ℚ α β where + smul_comm q a b := by + rw [← q.num_div_den, div_eq_mul_inv] + simp_rw [mul_smul, inv_natCast_smul_comm, Int.cast_smul_eq_zsmul] + rw [smul_comm a q.num] instance [Ring α] [Module ℚ α] : SMulCommClass α ℚ α := .symm .. diff --git a/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean b/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean new file mode 100644 index 0000000000..b99bb308a8 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean @@ -0,0 +1,6 @@ +import Mathlib.Algebra.Group.Action.Defs + +@[to_additive] +lemma smul_mul_smul_comm {α β : Type*} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] + [IsScalarTower α α β] [SMulCommClass β α β] (a : α) (b : β) (c : α) (d : β) : + (a • b) * c • d = (a * c) • (b * d) := smul_smul_smul_comm a b c d diff --git a/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean new file mode 100644 index 0000000000..8534515b29 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean @@ -0,0 +1,4 @@ +import Mathlib.Algebra.Order.Module.Defs + +attribute [gcongr] smul_le_smul_of_nonneg_left smul_le_smul_of_nonneg_right + smul_lt_smul_of_pos_left smul_lt_smul_of_pos_right diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean index 4c410c237e..6cb79e5ce5 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean @@ -129,16 +129,16 @@ end NormedField variable [DiscreteMeasurableSpace α] lemma cLpNorm_eq_expect' (hp₀ : p ≠ 0) (hp : p ≠ ∞) (f : α → E) : - ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by + ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖₊ ^ p.toReal) ^ p.toReal⁻¹ := by simp [cLpNorm, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete, one_div, ← mul_sum, integral_fintype, tsum_eq_sum' (s := univ) (by simp), ENNReal.coe_rpow_of_nonneg, cond_apply, expect_eq_sum_div_card, div_eq_inv_mul] lemma cLpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : α → E) : - ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by + ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖₊ ^ p) ^ p⁻¹ := by rw [cLpNorm_eq_expect'] <;> simp [hp.le, hp] lemma cLpNorm_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : - ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := + ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖₊ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := cLpNorm_eq_expect' (by simpa using hp) (by simp) _ lemma cLpNorm_rpow_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : @@ -152,12 +152,12 @@ lemma cLpNorm_pow_eq_expect {p : ℕ} (hp : p ≠ 0) (f : α → E) : lemma cL2Norm_sq_eq_expect (f : α → E) : ‖f‖ₙ_[2] ^ 2 = 𝔼 i, ‖f i‖ ^ 2 := by simpa using cLpNorm_pow_eq_expect two_ne_zero _ -lemma cL2Norm_eq_expect (f : α → E) : ‖f‖ₙ_[2] = sqrt (𝔼 i, ‖f i‖ ^ 2) := by +lemma cL2Norm_eq_expect (f : α → E) : ‖f‖ₙ_[2] = (𝔼 i, ‖f i‖₊ ^ 2) ^ (2⁻¹ : ℝ) := by simpa [sqrt_eq_rpow] using cLpNorm_eq_expect two_ne_zero _ -lemma cL1Norm_eq_expect (f : α → E) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [cLpNorm_eq_expect'] +lemma cL1Norm_eq_expect (f : α → E) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖₊ := by simp [cLpNorm_eq_expect'] -lemma nLinftyNorm_eq_iSup (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by +lemma nLinftyNorm_eq_iSup (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖₊ := by cases isEmpty_or_nonempty α · simp · simp [cLpNorm, nnLinftyNorm_eq_essSup] diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean index 460eabadf2..aaf44eb892 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean @@ -1,5 +1,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import LeanAPAP.Mathlib.Algebra.Algebra.Rat +import LeanAPAP.Mathlib.Algebra.Group.Action.Defs +import LeanAPAP.Mathlib.Algebra.Order.Module.Defs import LeanAPAP.Mathlib.Algebra.Star.Rat import LeanAPAP.Prereqs.LpNorm.Compact.Defs @@ -135,8 +137,10 @@ variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] /-- **Cauchy-Schwarz inequality** -/ lemma cL2Inner_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by simp only [cL2Norm_eq_expect, div_mul_div_comm, ← sq, ENNReal.toReal_ofNat] - rw [← sqrt_mul, le_sqrt, cL2Inner_eq_smul_dL2Inner, expect, card_univ] + rw [← mul_rpow, le_rpow_inv_iff_of_pos, cL2Inner_eq_smul_dL2Inner, expect, expect, card_univ, + rpow_two, smul_pow, smul_mul_smul_comm, ← sq, ← dL2Norm_sq_eq_sum, ← dL2Inner_eq_sum] gcongr + refine dL2Inner_le_dL2Norm_mul_dL2Norm _ _ refine div_le_div_of_nonneg_right (dL2Inner_le_dL2Norm_mul_dL2Norm _ _) ?_ all_goals positivity