nnLpNorm

LeanAPAP.lean

@@ -1,17 +1,24 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
+import LeanAPAP.Mathlib.Algebra.Algebra.Rat
+import LeanAPAP.Mathlib.Algebra.Group.Action.Defs
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
+import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
+import LeanAPAP.Mathlib.Algebra.Star.Basic
+import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Data.Fintype.Order
+import LeanAPAP.Mathlib.Data.NNReal.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
+import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
@@ -38,9 +45,12 @@ import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.LargeSpec
-import LeanAPAP.Prereqs.LpNorm.Compact
+import LeanAPAP.Prereqs.LpNorm.Compact.Defs
+import LeanAPAP.Prereqs.LpNorm.Compact.Inner
 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

@@ -31,22 +31,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_dL2Inner_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,
+  · rw [← balance_conv, balance, dL2Inner_sub_left, dL2Inner_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 [nnratCast_dens, le_div_iff₀, mul_comm] at hγC
+  · 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 [wLpNorm_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
@@ -86,7 +86,7 @@ lemma ap_in_ff (hS : S.Nonempty) (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : 
     calc
       _ = ⟪μ V', μ A₁ ∗ μ A₂ ○ 𝟭 S⟫_[ℝ] := by
         sorry
-        -- rw [conv_assoc, conv_l2Inner, ← conj_l2Inner]
+        -- rw [conv_assoc, conv_dL2Inner, ← conj_dL2Inner]
         -- simp
 
       _ = _ := sorry
@@ -103,7 +103,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)
@@ -118,13 +118,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 [wLpNorm_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
 
@@ -207,7 +207,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
             _ ≤ 2 := by norm_num
         · positivity
     all_goals positivity
-  rw [hB.l2Inner_mu_conv_mu_mu_two_smul_mu] at hBV
+  rw [hB.dL2Inner_mu_conv_mu_mu_two_smul_mu] at hBV
   suffices h : (q ^ (n - 65 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) by
     rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc] at h
     norm_num at h

LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean

@@ -0,0 +1,30 @@
+import Mathlib.Algebra.Algebra.Rat
+import Mathlib.Algebra.Module.Basic
+
+variable {α β : Type*}
+
+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 [Monoid α] [AddCommMonoid β] [Module ℚ≥0 β] [DistribMulAction α β] :
+    SMulCommClass α ℚ≥0 β := .symm ..
+
+instance [Semiring α] [Module ℚ≥0 α] : IsScalarTower ℚ≥0 α α where
+  smul_assoc 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 [Monoid α] [AddCommGroup β] [Module ℚ β] [DistribMulAction α β] : SMulCommClass α ℚ β :=
+  .symm ..
+
+instance [Ring α] [Module ℚ α] : IsScalarTower ℚ α α where
+  smul_assoc q a b := sorry

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/Mathlib/Algebra/Star/Basic.lean

@@ -0,0 +1,12 @@
+import Mathlib.Algebra.Star.Basic
+
+/-!
+# TODO
+
+Swap arguments to `star_nsmul`/`star_zsmul`
+-/
+
+variable {α : Type*}
+
+instance StarAddMonoid.toStarModuleInt [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where
+  star_smul _ _ := star_zsmul _ _

LeanAPAP/Mathlib/Algebra/Star/Rat.lean

@@ -0,0 +1,16 @@
+import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Star.Rat
+
+variable {α : Type*}
+
+@[simp] lemma star_nnqsmul [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] (q : ℚ≥0) (a : α) :
+    star (q • a) = q • star a := sorry
+
+@[simp] lemma star_qsmul [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] (q : ℚ) (a : α) :
+    star (q • a) = q • star a := sorry
+
+instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] :
+    StarModule ℚ≥0 α where star_smul := star_nnqsmul
+
+instance StarAddMonoid.toStarModuleRat [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] :
+    StarModule ℚ α where star_smul := star_qsmul

LeanAPAP/Mathlib/Data/NNReal/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib.Data.NNReal.Basic
+
+namespace NNReal
+
+@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ) := rfl
+
+end NNReal

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.EssSup
-import Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory

LeanAPAP/Mathlib/Probability/ConditionalProbability.lean

@@ -0,0 +1,13 @@
+import Mathlib.Probability.ConditionalProbability
+
+open ENNReal MeasureTheory MeasureTheory.Measure MeasurableSpace Set
+
+variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} (μ : Measure Ω)
+  {s t : Set Ω}
+
+namespace ProbabilityTheory
+
+@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[|s] s = 1 := by
+  simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs
+
+end ProbabilityTheory

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -10,6 +10,7 @@ import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 # Almost-periodicity
 -/
 
+open MeasureTheory
 open scoped Pointwise Combinatorics.Additive
 
 namespace Finset
@@ -85,7 +86,8 @@ end
 open Finset Real
 open scoped BigOperators Pointwise NNReal ENNReal
 
-variable {G : Type*} [Fintype G] {A S : Finset G} {f : G → ℂ} {ε K : ℝ} {k m : ℕ}
+variable {G : Type*} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {A S : Finset G}
+  {f : G → ℂ} {ε K : ℝ} {k m : ℕ}
 
 lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) :
     (8 * m) ^ m * k ^ (m - 1) * A.card ^ k * k * (2 * ‖f‖_[2 * m]) ^ (2 * m) ≤
@@ -95,7 +97,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_norm 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 ?_ * _ * _
@@ -119,6 +121,22 @@ variable [DecidableEq G] [AddCommGroup G]
 
 local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 
+lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
+    ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
+      (8 * m) ^ m * k ^ (m - 1) *
+        ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
+  let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x
+  refine (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_
+  · intro i
+    rw [Fintype.sum_piFinset_apply, sum_sub_distrib]
+    simp only [sub_eq_zero, sum_const, indicate_apply]
+    rw [← Pi.smul_apply (card A), ← smul_conv, card_smul_mu, conv_eq_sum_sub']
+    simp only [boole_mul, indicate_apply]
+    rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
+  congr with a : 1
+  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
+variable [DecidableEq G] [AddCommGroup G]
+
 namespace AlmostPeriodicity
 
 def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G) : Prop :=
@@ -143,21 +161,6 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
   congr with a : 3
   refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity
 
-lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
-    ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
-      (8 * m) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
-  let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x
-  refine (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_
-  · intro i
-    rw [Fintype.sum_piFinset_apply, sum_sub_distrib]
-    simp only [sub_eq_zero, sum_const, indicate_apply]
-    rw [← Pi.smul_apply (card A), ← smul_conv, card_smul_mu, conv_eq_sum_sub']
-    simp only [boole_mul, indicate_apply]
-    rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
-  congr with a : 1
-  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
-
 lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
     (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
       (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
@@ -166,16 +169,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 +194,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_nnnorm 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 +206,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_nnnorm hm']
     simp only [Pi.sub_apply, translate_apply]
   simp only [this]
   have :
@@ -234,18 +237,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 +384,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 +441,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_nnnorm]; 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 +485,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