Bump mathlib to v4.25.0

Author: YaelDillies

LeanAPAP/Extras/BSG.lean

@@ -112,12 +112,12 @@ lemma claim_two :
   have hf : ∀ s, f s ^ 2 = (𝟭_[ℝ] A ○ 𝟭 B) s := by
     intro s
     rw [Real.sq_sqrt]
-    exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation??
+    exact dconv_apply_nonneg indicate_nonneg indicate_nonneg s
   have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * #(A ∩ (s +ᵥ B)))
   refine div_le_of_le_mul₀ (by positivity) ?_ ?_
   · refine sum_nonneg fun i _ ↦ ?_
     -- indicate nonneg should be a positivity lemma
-    exact mul_nonneg (dconv_nonneg indicate_nonneg indicate_nonneg _) (by positivity)
+    exact mul_nonneg (dconv_apply_nonneg indicate_nonneg indicate_nonneg _) (by positivity)
   simp only [← sq, ← mul_assoc, hf, thing_two, mul_pow, claim_one] at this
   refine this.trans ?_
   rw [mul_comm]
@@ -148,8 +148,9 @@ lemma claim_four (ab : G × G) :
   have : ∑ s : G, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) ≤
       #B * ∑ s : G, (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) := by
     rw [mul_sum]
-    refine sum_le_sum fun i _ ↦ ?_
-    exact mul_le_mul_of_nonneg_right (this _) (mul_nonneg (indicate_nonneg _) (indicate_nonneg _))
+    gcongr with s hs
+    · exact mul_nonneg indicate_apply_nonneg indicate_apply_nonneg
+    · exact this _
   refine this.trans_eq ?_
   congr 1
   simp only [dconv_eq_sum_add]

LeanAPAP/FiniteField.lean

@@ -55,7 +55,10 @@ private lemma curlog_mul_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (h
     𝓛 (x * y) ≤ x⁻¹ * 𝓛 y := by
   suffices h : log x⁻¹ - (x⁻¹ - 1) ≤ (x⁻¹ - 1) * log y⁻¹ by
     rw [← sub_nonneg] at h ⊢
-    exact h.trans_eq (by rw [mul_inv, log_mul]; ring; all_goals positivity)
+    convert h using 1
+    rw [mul_inv, log_mul]
+    any_goals positivity
+    ring
   calc
     log x⁻¹ - (x⁻¹ - 1) ≤ 0 := sub_nonpos.2 <| log_le_sub_one_of_pos <| by positivity
     _ ≤ (x⁻¹ - 1) * log y⁻¹ := mul_nonneg (sub_nonneg.2 <| (one_le_inv₀ hx₀).2 hx₁) <| by bound
@@ -68,7 +71,10 @@ private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y)
     𝓛 (x ^ y) ≤ y⁻¹ * 𝓛 x := by
   suffices h : 1 - y⁻¹ ≤ (y⁻¹ - y) * log x⁻¹ by
     rw [← sub_nonneg] at h ⊢
-    exact h.trans_eq (by rw [← inv_rpow, log_rpow]; ring; all_goals positivity)
+    convert h using 1
+    rw [← inv_rpow, log_rpow]
+    any_goals positivity
+    ring
   calc
     1 - y⁻¹ ≤ 0 := sub_nonpos.2 <| (one_le_inv₀ hy₀).2 hy₁
     _ ≤ (y⁻¹ - y) * log x⁻¹ := mul_nonneg (sub_nonneg.2 <| hy₁.trans <| by bound) <| by bound
@@ -298,28 +304,33 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
       _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring
   obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),
       1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧
-        (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₁.dens ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₂.dens :=
-    sifting_cor (ε := ε / 16) (δ := ε / 32) (by positivity) (by linarith) (by positivity) (p := q')
-    (even_two_mul _) (le_mul_of_one_le_right zero_le_two (by simp; positivity)) (by
-      calc
-        (ε / 16)⁻¹ * log (2 / (ε / 32)) = 2 ^ 4 * ε⁻¹ ^ 1 * log (64 / ε) := by ring_nf
-        _ ≤ 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε) := by
-          gcongr
-          · norm_num
-          · norm_num
-          · exact (one_le_inv₀ hε₀).2 hε₁.le
-          · norm_num
-        _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _
-        _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add]
-        _ ≤ q' := by
-          unfold q'
-          gcongr
-          · norm_num
-          · positivity) hA₀
+        (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₁.dens ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₂.dens := by
+    refine sifting_cor (ε := ε / 16) (δ := ε / 32) (by positivity) (by linarith)
+      (by positivity) (p := q') (even_two_mul _)
+      (le_mul_of_one_le_right zero_le_two <| by simp; positivity) ?_ hA₀
+    calc
+      (ε / 16)⁻¹ * log (2 / (ε / 32)) = 2 ^ 4 * ε⁻¹ ^ 1 * log (64 / ε) := by ring_nf
+      _ ≤ 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε) := by
+        gcongr
+        · norm_num
+        · norm_num
+        · exact (one_le_inv₀ hε₀).2 hε₁.le
+        · norm_num
+      _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _
+      _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add]
+      _ ≤ q' := by
+        unfold q'
+        gcongr
+        · norm_num
+        · positivity
   have :=
     calc
       p' = 1 * ⌈(p' + 0 : ℝ)⌉₊ := by simp
-      _ ≤ q' := by unfold q'; gcongr; norm_num; positivity
+      _ ≤ q' := by
+        unfold q'
+        gcongr
+        · norm_num
+        · positivity
   have : card G • (f ○ f) + 1 = card G • (μ A ○ μ A) := by
     unfold f
     rw [← balance_dconv, balance, smul_sub, smul_const, Fintype.card_smul_expect]

LeanAPAP/Physics/DRC.lean

@@ -120,10 +120,9 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         mul_nonneg (sum_nonneg fun x _ ↦ mul_nonneg (this _) <| by positivity) <| by positivity
     have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p)
       ≤ #(A₁ s) / #B₁ * (#(A₂ s) / #B₂) := by
-      rw [div_mul_div_comm, le_div_iff₀]
+      rw [div_mul_div_comm, le_div_iff₀ (by positivity)]
       simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
         mul_div_right_comm] using h
-      positivity
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) <| hg s).le, this.trans <|
       mul_le_of_le_one_right ?_ <| div_le_one_of_le₀ ?_ ?_, this.trans <|
       mul_le_of_le_one_left ?_ <| div_le_one_of_le₀ ?_ ?_⟩
@@ -209,13 +208,13 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         ∑ x ∈ (s p ε B₁ B₂ A)ᶜ,
           (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by
       gcongr with x hx
-      · exact Pi.le_def.1 (dconv_nonneg (R := ℝ) mu_nonneg mu_nonneg) x
-      · exact dconv_nonneg indicate_nonneg indicate_nonneg _
+      · exact dconv_apply_nonneg mu_nonneg mu_nonneg x
+      · exact dconv_apply_nonneg indicate_nonneg indicate_nonneg _
       · simpa using hx
     _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by
       gcongr
       · intros
-        exact mul_nonneg (dconv_nonneg (mu_nonneg (K := ℝ)) mu_nonneg _) <| hp.pow_nonneg _
+        exact mul_nonneg (dconv_apply_nonneg mu_nonneg mu_nonneg _) <| hp.pow_nonneg _
       · exact subset_univ _
     _ = ‖μ_[ℝ] B₁‖_[1] * ‖μ_[ℝ] B₂‖_[1] * ((1 - ε) ^ p * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p)
         := ?_
@@ -248,12 +247,11 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
         4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / #A ^ (2 * p) := by
       rw [mul_div_assoc, ← div_pow]
       gcongr
-      rw [nnratCast_dens, le_div_iff₀, ← mul_div_right_comm]
+      rw [nnratCast_dens, le_div_iff₀ (by positivity), ← mul_div_right_comm]
       calc
         _ = (‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] : ℝ) := by
           simp [mu, wLpNorm_smul_right, dL1Norm_dconv, card_univ, inv_mul_eq_div]
         _ ≤ _ := wLpNorm_mono_right (one_le_two.trans <| by norm_cast) _ _
-      · exact Nat.cast_pos.2 hA.card_pos
     obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ :=
       sifting univ univ hε hε₁ hδ hp hp₂ hpε (by simp) hA (by simpa)
     exact ⟨A₁, A₂, h, this.trans <| by simpa [nnratCast_dens] using hcard₁,

LeanAPAP/Physics/Unbalancing.lean

@@ -101,7 +101,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ = _ := by simp [mul_sum, mul_left_comm (2 : ℝ)]
   set P : Finset _ := {i | 0 ≤ f i}
   set T : Finset _ := {i | 3 / 4 * ε ≤ f i}
-  have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans <| by positivity
+  have hTP : T ⊆ P := by unfold P T; gcongr; positivity
   have : 2⁻¹ * ε ^ p ≤ ∑ i ∈ P, ↑(ν i) * (f ^ p) i := by
     rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter]
     convert this using 3
@@ -159,17 +159,18 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
   set p' := 24 / ε * log (3 / ε) * p
   have hp' : 0 < p' := p'_pos hp hε₀ hε₁
   have : 1 - 8⁻¹ * ε ≤ (∑ i ∈ T, ↑(ν i)) ^ p'⁻¹ := by
-    rw [← div_le_iff₀, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this
+    rw [← div_le_iff₀ (by positivity), mul_div_assoc, ← div_pow,
+      le_sqrt (by positivity) (by positivity), mul_pow, ← pow_mul'] at this
     calc
       _ ≤ exp (-(8⁻¹ * ε)) := one_sub_le_exp_neg _
       _ = ((ε / 3) ^ p * (ε / 3) ^ (2 * p)) ^ p'⁻¹ := ?_
       _ ≤ _ := rpow_le_rpow ?_ ((mul_le_mul_of_nonneg_right ?_ ?_).trans this) ?_
     · rw [← pow_add, ← one_add_mul _ p, ← rpow_natCast, Nat.cast_mul, ← rpow_mul, ← div_eq_mul_inv,
         mul_div_mul_right, ← exp_log (_ : 0 < ε / 3), ← exp_mul, ← inv_div, log_inv, neg_mul,
         mul_div_left_comm, div_mul_cancel_right₀ (log_ε_pos hε₀ hε₁).ne']
+      any_goals positivity
       field_simp
       ring_nf
-      all_goals positivity
     any_goals positivity
     calc
       _ ≤ (1 / 3 : ℝ) ^ p := by gcongr

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -75,9 +75,6 @@ lemma ext_width {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies)
 
 /-! ### Coercion, membership -/
 
--- instance instMem : Membership G (BohrSet G) :=
---   ⟨fun x B ↦ ∀ ψ, ‖1 - ψ x‖₊ ≤ B.ewidth ψ⟩
-
 /-- The set corresponding to a Bohr set `B` is `{x | ∀ ψ ∈ B.frequencies, ‖1 - ψ x‖ ≤ B.width ψ}`.
 This is the *chord-length* convention. The arc-length convention would instead be
 `{x | ∀ ψ ∈ B.frequencies, |arg (ψ x)| ≤ B.width ψ}`.
@@ -120,7 +117,7 @@ lemma mem_chordSet_iff_norm_width :
 -- TODO: This lemma needs `Finite G` because we are using `AddChar G ℂ` rather than `AddChar G ℂˣ`
 -- as the dual group.
 @[simp] lemma neg_mem [Finite G] : -x ∈ B.chordSet ↔ x ∈ B.chordSet :=
-  forall₂_congr fun ψ hψ ↦ by rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
+  forall_congr' fun ψ ↦ by rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
 
 /-! ### Lattice structure -/
 
@@ -131,40 +128,34 @@ noncomputable instance : Max (BohrSet G) where
       mem_frequencies := fun ψ => by simp [mem_frequencies] }
 
 noncomputable instance : Min (BohrSet G) where
-  min B₁ B₂ :=
-    { frequencies := B₁.frequencies ∪ B₂.frequencies,
-      ewidth := fun ψ => B₁.ewidth ψ ⊓ B₂.ewidth ψ,
-      mem_frequencies := fun ψ => by simp [mem_frequencies] }
+  min B₁ B₂ := {
+    frequencies := B₁.frequencies ∪ B₂.frequencies,
+    ewidth ψ := B₁.ewidth ψ ⊓ B₂.ewidth ψ,
+    mem_frequencies ψ := by simp [mem_frequencies]
+  }
 
 noncomputable instance [Finite G] : Bot (BohrSet G) where
-  bot :=
-    { frequencies := ⊤,
-      ewidth := 0,
-      mem_frequencies := by simp }
+  bot.frequencies := ⊤
+  bot.ewidth := 0
+  bot.mem_frequencies := by simp
 
 noncomputable instance : Top (BohrSet G) where
-  top :=
-    { frequencies := ⊥,
-      ewidth := ⊤,
-      mem_frequencies := by simp }
+  top.frequencies := ⊥
+  top.ewidth := ⊤
+  top.mem_frequencies := by simp
 
 noncomputable instance : DistribLattice (BohrSet G) :=
-  Function.Injective.distribLattice BohrSet.ewidth
-    ewidth_injective
-    (fun _ _ => rfl)
-    (fun _ _ => rfl)
+  ewidth_injective.distribLattice BohrSet.ewidth (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
 
 lemma le_iff_ewidth {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ ∀ ⦃ψ⦄, B₁.ewidth ψ ≤ B₂.ewidth ψ := Iff.rfl
 
 @[gcongr]
-lemma frequencies_anti {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) :
-    B₂.frequencies ⊆ B₁.frequencies := by
+lemma frequencies_anti {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : B₂.frequencies ⊆ B₁.frequencies := by
   intro ψ hψ
   simp only [mem_frequencies] at hψ ⊢
   exact (h ψ).trans_lt hψ
 
-lemma frequencies_antitone : Antitone (frequencies : BohrSet G → _) :=
-  fun _ _ => frequencies_anti
+lemma frequencies_antitone : Antitone (frequencies : BohrSet G → _) := fun _ _ ↦ frequencies_anti
 
 lemma le_iff_width {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔
     B₂.frequencies ⊆ B₁.frequencies ∧ ∀ ⦃ψ⦄, ψ ∈ B₂.frequencies → B₁.width ψ ≤ B₂.width ψ := by

LeanAPAP/Prereqs/Convolution/Order.lean

@@ -13,11 +13,15 @@ variable [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f g : G → R}
 lemma conv_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ f ∗ g :=
   fun _a ↦ sum_nonneg fun _x _ ↦ mul_nonneg (hf _) (hg _)
 
+lemma conv_apply_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) : 0 ≤ (f ∗ g) a := conv_nonneg hf hg _
+
 variable [StarRing R] [StarOrderedRing R]
 
 lemma dconv_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ f ○ g :=
   fun _a ↦ sum_nonneg fun _x _ ↦ mul_nonneg (hf _) <| star_nonneg_iff.2 <| hg _
 
+lemma dconv_apply_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) : 0 ≤ (f ○ g) a := dconv_nonneg hf hg _
+
 end OrderedCommSemiring
 
 section StrictOrderedCommSemiring

LeanAPAP/Prereqs/Function/Indicator/Defs.lean

@@ -1,7 +1,6 @@
-import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Algebra.BigOperators.Pi
+import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Group.Action.Pointwise.Finset
-import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Star.Pi
 import Mathlib.Data.Fintype.Lattice
 import Mathlib.Data.Nat.Cast.Order.Ring
@@ -121,10 +120,12 @@ variable [StarRing R]
 end CommSemiring
 
 section OrderedSemiring
-variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α}
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α} {a : α}
 
 @[simp] lemma indicate_nonneg : 0 ≤ 𝟭_[R] s := fun a ↦ by rw [indicate_apply]; split_ifs <;> simp
 
+@[simp] lemma indicate_apply_nonneg : 0 ≤ 𝟭_[R] s a := indicate_nonneg _
+
 @[simp] lemma indicate_pos [Nontrivial R] : 0 < 𝟭_[R] s ↔ s.Nonempty := by
   simp [indicate_apply, funext_iff, lt_iff_le_and_ne, @eq_comm R 0,
     Finset.Nonempty]

LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean

@@ -1,6 +1,6 @@
 /-
 Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved.
-Released under Apache 2.0 license as described ∈ the file LICENSE.
+Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Data.Nat.Choose.Multinomial
@@ -28,7 +28,7 @@ can be obtained from this specific one by nesting of Lp norms.
 -/
 
 open Finset Fintype Function Nat MeasureTheory ProbabilityTheory Real
-open scoped NNReal
+open scoped NNReal ENNReal
 
 variable {ι Ω E : Type*} {A : Finset ι} {m n : ℕ} [MeasurableSpace Ω] {μ : Measure Ω}
   [IsFiniteMeasure μ] [mE : MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
@@ -42,16 +42,16 @@ noncomputable def marcinkiewiczZygmundSymmConst (p : ℝ≥0) : ℝ := (p / 2) ^
 
 /-- The **Marcinkiewicz-Zygmund inequality** for symmetric random variables, with a slightly better
 constant than `marcinkiewicz_zygmund`. -/
-theorem marcinkiewicz_zygmund_symmetric
-    (iIndepFun_X : iIndepFun X μ)
+theorem marcinkiewicz_zygmund_symmetric (iIndepFun_X : iIndepFun X μ)
     (identDistrib_neg_X : ∀ i, IdentDistrib (X i) (-X i) μ μ)
-    (MemLp_X : ∀ i ∈ A, MemLp (X i) (2 * m) μ) :
+    (memLp_X : ∀ i ∈ A, MemLp (X i) (2 * m) μ) :
     ∫ ω, ‖∑ i ∈ A, X i ω‖ ^ (2 * m) ∂μ ≤
       marcinkiewiczZygmundSymmConst (2 * m) * ∫ ω, (∑ i ∈ A, ‖X i ω‖ ^ 2) ^ m ∂μ := by
   have : DecidableEq ι := Classical.decEq _
   -- Turn the `L^p` assumption on the `X i` into various integrability conditions.
   have integrable_prod_norm_X I (hI : I ∈ A ×ˢ A ^^ m) :
-    Integrable (fun ω ↦ ∏ k, ‖X (I k).1 ω‖ * ‖X (I k).2 ω‖) μ := sorry
+    Integrable (fun ω ↦ ∏ k, ‖X (I k).1 ω‖ * ‖X (I k).2 ω‖) μ := by
+    sorry
   have integrable_prod_inner_X I (hI : I ∈ A ×ˢ A ^^ m) :
     Integrable (fun ω ↦ ∏ k, inner ℝ (X (I k).1 ω) (X (I k).2 ω)) μ := sorry
   -- Call a family of indices `i₁, ..., iₙ, j₁, ..., jₙ` *even* if each `i ∈ A` appears an even
@@ -85,7 +85,7 @@ theorem marcinkiewicz_zygmund_symmetric
         · simpa [Y, hji] using .refl (identDistrib_neg_X _).aemeasurable_fst
       -- To show that `𝔼 ∏ k, ⟨X iₖ, X jₖ⟩ = 0`, we will show
       -- `𝔼 ∏ k, ⟨X iₖ, X jₖ⟩ = 𝔼 ∏ k, ⟨Y iₖ, Y jₖ⟩ = -𝔼 ∏ k, ⟨X iₖ, X jₖ⟩`.
-      rw [← neg_eq_self ℝ, ← integral_neg, eq_comm]
+      rw [← neg_eq_self, ← integral_neg, eq_comm]
       calc
         -- `𝔼 ∏ k, ⟨X iₖ, X jₖ⟩ = 𝔼 ∏ k, ⟨Y iₖ, Y jₖ⟩` because `𝔼 ∏ k, ⟨X iₖ, X jₖ⟩` and
         -- `∏ k, ⟨Y iₖ, Y jₖ⟩` are identically distributed.
@@ -168,10 +168,9 @@ noncomputable def marcinkiewiczZygmundConst (p : ℝ≥0) : ℝ :=
 /-- The **Marcinkiewicz-Zygmund inequality** for random variables with zero mean.
 
 For symmetric random variables, `marcinkiewicz_zygmund` provides a slightly better constant. -/
-theorem marcinkiewicz_zygmund
-    (iIndepFun_X : iIndepFun X μ)
+theorem marcinkiewicz_zygmund (iIndepFun_X : iIndepFun X μ)
     (integral_X : ∀ i, ∫ ω, X i ω ∂μ = 0)
-    (MemLp_X : ∀ i ∈ A, MemLp (X i) (2 * m) μ) :
+    (memLp_X : ∀ i ∈ A, MemLp (X i) (2 * m) μ) :
     ∫ ω, ‖∑ i ∈ A, X i ω‖ ^ (2 * m) ∂μ ≤
       marcinkiewiczZygmundConst (2 * m) * ∫ ω, (∑ i ∈ A, ‖X i ω‖ ^ 2) ^ m ∂μ := by
   let X₁ i : Ω × Ω → E := X i ∘ Prod.fst