fix more

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 ..
 

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

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

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]

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