nnLpNorm

LeanAPAP.lean

@@ -54,6 +54,8 @@ import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
+import LeanAPAP.Prereqs.NNLpNorm
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/FiniteField/Basic.lean

@@ -37,22 +37,22 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
     _ ≤ _ := div_le_div_of_nonneg_right hAC (card G).cast_nonneg
     _ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_
     _ ≤ ‖balance (μ_[ℝ] A) ∗ balance (μ A)‖_[p] * ‖μ_[ℝ] C‖_[NNReal.conjExponent p] :=
-        abs_l2Inner_le_lpNorm_mul_lpNorm hp'' _ _
+        abs_l2Inner_le_dLpNorm_mul_dLpNorm hp'' _ _
     _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) :=
-        mul_le_mul (lpNorm_conv_le_lpNorm_dconv' (by positivity) (even_two_mul _) _) ?_
+        mul_le_mul (dLpNorm_conv_le_dLpNorm_dconv' (by positivity) (even_two_mul _) _) ?_
           (by positivity) (by positivity)
     _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] *
           γ ^ (-(p : ℝ)⁻¹) := ?_
     _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity
   · rw [← balance_conv, balance, l2Inner_sub_left, l2Inner_const_left, expect_conv, sum_mu ℝ hA,
       expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ← mul_inv_cancel₀, ← mul_sub,
       abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity
-  · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow]
+  · rw [dLpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow]
     rw [nnratCast_dens, le_div_iff, mul_comm] at hγC
     refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_)
     all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two, p]
-    rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
+    rw [wdLpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
     push_cast
     any_goals norm_cast; rw [Nat.succ_le_iff]
     rfl
@@ -109,7 +109,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
     refine ⟨⊤, univ, _⟩
     rw [AffineSubspace.direction_top]
     simp only [AffineSubspace.top_coe, coe_univ, eq_self_iff_true, finrank_top, tsub_self,
-      Nat.cast_zero, indicate_empty, zero_mul, lpNorm_zero, true_and_iff,
+      Nat.cast_zero, indicate_empty, zero_mul, nnLpNorm_zero, true_and_iff,
       Finset.card_empty, zero_div] at hαA ⊢
     exact ⟨by positivity, mul_nonpos_of_nonneg_of_nonpos (by positivity) hαA⟩
   have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
@@ -124,13 +124,13 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
     simp [smul_dconv, dconv_smul, smul_smul]
   · simp [card_univ, show (card G : ℂ) ≠ 0 by sorry]
   · simp only [comp_const, Nonneg.coe_inv, NNReal.coe_natCast]
-    rw [← ENNReal.coe_one, lpNorm_const one_ne_zero]
+    rw [← ENNReal.coe_one, dLpNorm_const one_ne_zero]
     sorry
     -- simp only [Nonneg.coe_one, inv_one, rpow_one, norm_inv, norm_coe_nat,
     --   mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)]
   · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry
     sorry
-    -- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity),
+    -- simpa [wdLpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity),
     --   ← div_div, *] using global_dichotomy hA hγC hγ hAC
   sorry
 

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -95,7 +95,7 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) :
     refine mul_ne_zero two_pos.ne' ?_
     rw [← pos_iff_ne_zero, ← Nat.succ_le_iff]
     exact hm
-  rw [mul_pow (2 : ℝ), ← hmeq, ← lpNorm_pow_eq_sum hm' f, ← mul_assoc, ← mul_assoc,
+  rw [mul_pow (2 : ℝ), ← hmeq, ← dLpNorm_pow_eq_sum hm' f, ← mul_assoc, ← mul_assoc,
     mul_right_comm _ (A.card ^ k : ℝ), mul_right_comm _ (A.card ^ k : ℝ),
     mul_right_comm _ (A.card ^ k : ℝ)]
   gcongr ?_ * _ * _
@@ -166,16 +166,16 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
   have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1
   have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by rw [← hmeq, Nat.one_le_cast]; exact hm'.le
   gcongr
-  refine (lpNorm_sub_le hm'' _ _).trans ?_
-  rw [lpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left]
+  refine (dLpNorm_sub_le hm'' _ _).trans ?_
+  rw [dLpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left]
   have hmeq' : ((2 * m : ℝ≥0) : ℝ≥0∞) = 2 * m := by
     rw [ENNReal.coe_mul, ENNReal.coe_two, ENNReal.coe_natCast]
   have : (1 : ℝ≥0) < 2 * m := by
     rw [← Nat.cast_two, ← Nat.cast_mul, Nat.one_lt_cast]
     exact hm'
   rw [← hmeq', conv_comm]
-  refine (lpNorm_conv_le this.le _ _).trans ?_
-  rw [l1Norm_mu hA, mul_one]
+  refine (dLpNorm_conv_le this.le _ _).trans ?_
+  rw [dL1Norm_mu hA, mul_one]
 
 lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :
     (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by
@@ -191,7 +191,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
   have hm' : 2 * m ≠ 0 := by linarith
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
   rw [← hmeq, mul_pow]
-  simp only [lpNorm_pow_eq_sum hm']
+  simp only [dLpNorm_pow_eq_sum hm']
   rw [sum_comm]
   have : ∀ x : G, ∑ a in A ^^ k,
       ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
@@ -203,7 +203,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
   simp only [@sum_comm _ _ G]
   have (a : Fin k → G) (i : Fin k) :
       ∑ x, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) = ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) := by
-    rw [← hmeq, lpNorm_pow_eq_sum hm']
+    rw [← hmeq, dLpNorm_pow_eq_sum hm']
     simp only [Pi.sub_apply, translate_apply]
   simp only [this]
   have :
@@ -234,18 +234,18 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m 
     refine Finset.sum_congr rfl fun j _ ↦ ?_
     rw [sub_right_comm]
   have h₄₁ : ‖τ t f₁ - k • (mu A ∗ f)‖_[2 * m] = ‖τ (-t) (τ t f₁ - k • (mu A ∗ f))‖_[2 * m] := by
-    rw [lpNorm_translate]
+    rw [dLpNorm_translate]
   have h₄ : ‖τ t f₁ - k • (mu A ∗ f)‖_[2 * m] = ‖f₁ - τ (-t) (k • (mu A ∗ f))‖_[2 * m] := by
     rw [h₄₁, translate_sub_right, translate_translate]
     simp
   have h₅₁ : ‖τ (-t) (k • (mu A ∗ f)) - f₁‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by
-    rwa [lpNorm_sub_comm, ← h₄, ← h₃]
+    rwa [dLpNorm_sub_comm, ← h₄, ← h₃]
   have : (0 : ℝ) < k := by positivity
   refine le_of_mul_le_mul_left ?_ this
-  rw [← nsmul_eq_mul, ← lpNorm_nsmul hp _ (_ - mu A ∗ f), nsmul_sub, ←
+  rw [← nsmul_eq_mul, ← dLpNorm_nsmul hp _ (_ - mu A ∗ f), nsmul_sub, ←
     translate_smul_right (-t) (mu A ∗ f) k, mul_assoc, mul_left_comm, two_mul ((k : ℝ) * _), ←
     mul_assoc]
-  exact (lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub hp _ _).trans (add_le_add h₅₁ h₁)
+  exact (dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub hp _ _).trans (add_le_add h₅₁ h₁)
 
 lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     (∑ x in L + S.piDiag (Fin k), ∑ l in L, ∑ s in S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2
@@ -381,7 +381,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
       refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_
       rw [one_mul, Nat.cast_le]
       exact card_le_univ _
-    simp only [mu_empty, zero_conv, translate_zero_right, sub_self, lpNorm_zero]
+    simp only [mu_empty, zero_conv, translate_zero_right, sub_self, nnLpNorm_zero]
     positivity
   let k := ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊
   have hk : k ≠ 0 := by positivity
@@ -438,19 +438,19 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
         = (F ∗ μ C) x := by simp [sub_conv, F]
       _ = ∑ y, F y * μ C (x - y) := conv_eq_sum_sub' ..
       _ = ∑ y, F y * μ (x +ᵥ -C) y := by simp [neg_add_eq_sub]
-  rw [linftyNorm_eq_ciSup]
+  rw [dLinftyNorm_eq_iSup]
   refine ciSup_le fun x ↦ ?_
   calc
     ‖(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x‖
       = ‖∑ y, F y * μ (x +ᵥ -C) y‖ := by rw [this]
     _ ≤ ∑ y, ‖F y * μ (x +ᵥ -C) y‖ := norm_sum_le _ _
-    _ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [l1Norm_eq_sum]; rfl
-    _ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := l1Norm_mul_le hM _ _
+    _ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [dL1Norm_eq_sum]; rfl
+    _ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := dL1Norm_mul_le hM _ _
     _ ≤ ε / exp 1 * B.card ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by
         gcongr
-        simpa only [← ENNReal.coe_natCast, lpNorm_indicate hM₀] using hT _ ht
+        simpa only [← ENNReal.coe_natCast, dLpNorm_indicate hM₀] using hT _ ht
     _ = ε * ((C.card / B.card) ^ (-(M : ℝ)⁻¹) / exp 1) := by
-        rw [← mul_comm_div, lpNorm_mu hM.symm.one_le hC.neg.vadd_finset, card_vadd_finset,
+        rw [← mul_comm_div, dLpNorm_mu hM.symm.one_le hC.neg.vadd_finset, card_vadd_finset,
           card_neg, hM.symm.coe.inv_sub_one, div_rpow, mul_assoc, NNReal.coe_natCast,
           rpow_neg, rpow_neg, ← div_eq_mul_inv, inv_div_inv] <;> positivity
     _ ≤ ε := mul_le_of_le_one_right (by positivity) $ (div_le_one $ by positivity).2 ?_
@@ -482,12 +482,12 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
     ‖μ T ∗^ k ∗ F - F‖_[∞]
       = ‖𝔼 a ∈ T ^^ k, (τ (∑ i, a i) F - F)‖_[∞] := by
         rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinset_const]
-    _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := lpNorm_expect_le le_top _ _
+    _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := dLpNorm_expect_le le_top _ _
     _ ≤ 𝔼 _a ∈ T ^^ k, ε := expect_le_expect fun x hx ↦ ?_
     _ = ε := by rw [expect_const hT'.piFinset_const]
   calc
     ‖τ (∑ i, x i) F - F‖_[⊤]
-    _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := lpNorm_translate_sum_sub_le le_top _ _ _
+    _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := dLpNorm_translate_sum_sub_le le_top _ _ _
     _ ≤ ∑ _i, ε / k := sum_le_sum fun i _ ↦ hT _ $ Fintype.mem_piFinset.1 hx _
     _ = ε := by simp only [sum_const, card_fin, nsmul_eq_mul]; rw [mul_div_cancel₀]; positivity
 

LeanAPAP/Physics/DRC.lean

@@ -40,9 +40,9 @@ private lemma sum_cast_c (p : ℕ) (B A : Finset G) :
 
 /-- If `A` is nonempty, and `B₁` and `B₂` intersect, then the `μ B₁ ○ μ B₂`-weighted Lp norm of
 `𝟭 A ○ 𝟭 A` is positive. -/
-private lemma lpNorm_conv_pos (hp : p ≠ 0) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :
+private lemma dLpNorm_conv_pos (hp : p ≠ 0) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :
     0 < ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
-  rw [wlpNorm_pow_eq_sum]
+  rw [wdLpNorm_pow_eq_sum]
   refine sum_pos' (fun x _ ↦ by positivity) ⟨0, mem_univ _, smul_pos ?_ $ pow_pos ?_ _⟩
   · rwa [pos_iff_ne_zero, ← Function.mem_support, support_dconv, support_mu, support_mu, ← coe_sub,
       mem_coe, zero_mem_sub_iff, not_disjoint_iff_nonempty_inter] <;> exact mu_nonneg
@@ -63,7 +63,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   have := hB.mono inter_subset_left
   have := hB.mono inter_subset_right
   have hp₀ : p ≠ 0 := by positivity
-  have := lpNorm_conv_pos hp₀ hB hA
+  have := dLpNorm_conv_pos hp₀ hB hA
   set M : ℝ :=
     2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
       with hM_def
@@ -82,7 +82,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity
   have hgB : ∑ s, g s = B₁.card * B₂.card * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
     have hAdconv : 0 ≤ 𝟭_[ℝ] A ○ 𝟭 A := dconv_nonneg indicate_nonneg indicate_nonneg
-    simpa only [wlpNorm_pow_eq_sum hp₀, l2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
+    simpa only [wdLpNorm_pow_eq_sum hp₀, l2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
       RCLike.inner_apply, RCLike.conj_to_real, norm_of_nonneg (hAdconv _), mul_one, nsmul_eq_mul,
       Nat.cast_mul, ← hg_def, NNReal.smul_def, NNReal.coe_dconv, NNReal.coe_comp_mu]
         using lemma_0 p B₁ B₂ A 1
@@ -177,7 +177,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     simp_rw [nonempty_iff_ne_empty]
     rintro c r h rfl
     simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff (zero_lt_four' ℝ), mul_assoc,
-      div_nonpos_iff, mul_nonpos_iff, (pow_pos (lpNorm_conv_pos hp₀.ne' hB hA) 2).not_le] at h
+      div_nonpos_iff, mul_nonpos_iff, (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_le] at h
     norm_cast at h
     simp [hp₀, hA.ne_empty] at h
   have hA₁ : A₁.Nonempty := aux _ _ hcard₁
@@ -188,11 +188,11 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
     _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by
       simp [l2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
-    _ ≤ _ := (le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h
+    _ ≤ _ := (le_div_iff $ dLpNorm_conv_pos hp₀.ne' hB hA).2 h
     _ ≤ _ := ?_
   · simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu]
     rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul]
-  rw [div_le_iff (lpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff' (zero_lt_two' ℝ)]
+  rw [div_le_iff (dLpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff' (zero_lt_two' ℝ)]
   simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole,
     sum_ite_mem, univ_inter, mul_div_right_comm]
   calc
@@ -210,10 +210,10 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         := ?_
     _ ≤ _ :=
       (mul_le_of_le_one_left (mul_nonneg (hp.pow_nonneg _) $ hp.pow_nonneg _) $
-        mul_le_one l1Norm_mu_le_one lpNorm_nonneg l1Norm_mu_le_one)
+        mul_le_one dL1Norm_mu_le_one nnLpNorm_nonneg dL1Norm_mu_le_one)
     _ ≤ _ := mul_le_mul_of_nonneg_right ?_ $ hp.pow_nonneg _
   · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ := dconv_nonneg mu_nonneg mu_nonneg
-    simp_rw [← l1Norm_dconv mu_nonneg mu_nonneg, l1Norm_eq_sum, norm_of_nonneg (this _), sum_mul,
+    simp_rw [← dL1Norm_dconv mu_nonneg mu_nonneg, dL1Norm_eq_sum, norm_of_nonneg (this _), sum_mul,
       mul_pow]
   calc
     (1 - ε) ^ p ≤ exp (-ε) ^ p := pow_le_pow_left (sub_nonneg.2 hε₁) (one_sub_le_exp_neg _) _
@@ -239,8 +239,8 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
     rw [nnratCast_dens, le_div_iff, ← mul_div_right_comm]
     calc
       _ = ‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] := by
-        simp [mu, wlpNorm_smul_right, hp₀, l1Norm_dconv, card_univ, inv_mul_eq_div]
-      _ ≤ _ := wlpNorm_mono_right (one_le_two.trans $ by norm_cast) _ _
+        simp [mu, wdLpNorm_smul_right, hp₀, dL1Norm_dconv, card_univ, inv_mul_eq_div]
+      _ ≤ _ := wdLpNorm_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 [univ_nonempty]) hA (by simpa)