Progress yet again

LeanAPAP.lean

@@ -23,6 +23,7 @@ import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Dirac
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
+import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity

LeanAPAP/FiniteField/Basic.lean

@@ -52,7 +52,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
     refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_)
     all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two, p]
-    rw [wdLpNorm_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
@@ -130,7 +130,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
     --   mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)]
   · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry
     sorry
-    -- simpa [wdLpNorm_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
 

LeanAPAP/Mathlib/Data/ENNReal/Operations.lean

@@ -3,7 +3,10 @@ import Mathlib.Data.ENNReal.Operations
 namespace ENNReal
 variable {α : Type*} {s : Finset α} {f : α → ℝ≥0∞}
 
-lemma sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ⊤ := by
+-- TODO: Unify `sum_lt_top` and `sum_lt_top_iff`
+attribute [simp] sum_lt_top_iff
+
+@[simp] lemma sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ⊤ := by
   simpa [lt_top_iff_ne_top] using sum_lt_top_iff
 
 end ENNReal

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -1,11 +1,25 @@
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 import Mathlib.MeasureTheory.Function.EssSup
+import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace
+import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory
+open scoped ENNReal
 
-variable {α β : Type*} [Nonempty α] {m : MeasurableSpace α} [ConditionallyCompleteLattice β]
+variable {α β : Type*} {m : MeasurableSpace α} [ConditionallyCompleteLattice β]
   {μ : Measure α} {f : α → β}
 
+section SMul
+variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
+  [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞}
+
+-- TODO: Replace in mathlib
+@[simp] lemma essSup_smul_measure' {f : α → β} {c : ℝ≥0∞} (hc : c ≠ 0) :
+    essSup f (c • μ) = essSup f μ := by simp_rw [essSup, Measure.ae_smul_measure_eq hc]
+
+end SMul
+
+variable [Nonempty α]
+
 lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) :
     essSup f μ = ⨆ a, f a := by rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
 

LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -44,4 +44,23 @@ lemma eLpNorm_nsmul [NormedSpace ℝ F] (n : ℕ) (f : α → F) :
     eLpNorm (n • f) p μ = n * eLpNorm f p μ := by
   simpa [Nat.cast_smul_eq_nsmul] using eLpNorm_const_smul (n : ℝ) f
 
+-- TODO: Replace `eLpNorm_smul_measure_of_ne_zero`
+lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0∞} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞)
+    (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p⁻¹.toReal * eLpNorm f p μ := by
+  simpa using eLpNorm_smul_measure_of_ne_zero hc
+
+lemma eLpNorm_smul_measure_of_ne_zero'' {c : ℝ≥0} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞)
+    (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p⁻¹.toReal • eLpNorm f p μ :=
+  (eLpNorm_smul_measure_of_ne_zero (ENNReal.coe_ne_zero.2 hc)).trans (by simp; norm_cast)
+
+lemma eLpNorm_smul_measure_of_ne_top' (hp : p ≠ ∞) (c : ℝ≥0∞) (f : α → F) :
+    eLpNorm f p (c • μ) = c ^ p⁻¹.toReal * eLpNorm f p μ := by
+  simpa using eLpNorm_smul_measure_of_ne_top hp _
+
+lemma eLpNorm_smul_measure_of_ne_top'' (hp : p ≠ ∞) (c : ℝ≥0) (f : α → F) :
+    eLpNorm f p (c • μ) = c ^ p⁻¹.toReal • eLpNorm f p μ := by
+  have : 0 ≤ p⁻¹.toReal := by positivity
+  refine (eLpNorm_smul_measure_of_ne_top' hp _ _).trans ?_
+  simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this]
+
 end MeasureTheory

LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1,9 +1,21 @@
 import Mathlib.MeasureTheory.Measure.MeasureSpace
 
+open scoped ENNReal
+
 namespace MeasureTheory.Measure
 variable {ι α : Type*} {mα : MeasurableSpace α} {f : ι → Measure α}
 
 @[simp] lemma sum_eq_zero : sum f = 0 ↔ ∀ i, f i = 0 := by
   simp (config := { contextual := true }) [Measure.ext_iff, forall_swap (α := ι)]
 
+variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
+  [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞}
+
+-- TODO: Replace in mathlib
+lemma ae_smul_measure_iff' {p : α → Prop} {c : R} (hc : c ≠ 0) {μ : Measure α} :
+    (∀ᵐ x ∂c • μ, p x) ↔ ∀ᵐ x ∂μ, p x := by simp [ae_iff, hc]
+
+@[simp] lemma ae_smul_measure_eq' (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ := by
+  ext; exact ae_smul_measure_iff hc
+
 end MeasureTheory.Measure

LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -0,0 +1,10 @@
+import Mathlib.MeasureTheory.Measure.Typeclasses
+import LeanAPAP.Mathlib.Data.ENNReal.Operations
+
+namespace MeasureTheory
+variable {ι α : Type*} {mα : MeasurableSpace α} {s : Finset ι} {μ : ι → Measure α}
+  [∀ i, IsFiniteMeasure (μ i)]
+
+instance : IsFiniteMeasure (∑ i ∈ s, μ i) where measure_univ_lt_top := by simp [measure_lt_top]
+
+end MeasureTheory

LeanAPAP/Physics/DRC.lean

@@ -42,7 +42,7 @@ private lemma sum_cast_c (p : ℕ) (B A : Finset G) :
 `𝟭 A ○ 𝟭 A` is positive. -/
 private lemma dLpNorm_conv_pos (hp : p ≠ 0) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :
     0 < ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
-  rw [wdLpNorm_pow_eq_sum]
+  rw [wLpNorm_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
@@ -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 [wdLpNorm_pow_eq_sum hp₀, l2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
+    simpa only [wLpNorm_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
@@ -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, wdLpNorm_smul_right, hp₀, dL1Norm_dconv, card_univ, inv_mul_eq_div]
-      _ ≤ _ := wdLpNorm_mono_right (one_le_two.trans $ by norm_cast) _ _
+        simp [mu, wLpNorm_smul_right, hp₀, 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 [univ_nonempty]) hA (by simpa)

LeanAPAP/Physics/Unbalancing.lean

@@ -63,7 +63,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       1 + ε / 2 ≤ 1 + 1 / 2 := add_le_add_left (div_le_div_of_nonneg_right hε₁ zero_le_two) _
       _ ≤ 2 := by norm_num
       _ ≤ ‖f + 1‖_[2 * p, ν] := hf₁
-      _ ≤ _ := wdLpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _
+      _ ≤ _ := wLpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _
     push_cast
     refine mul_le_mul_of_nonneg_right ?_ ?_
     calc
@@ -82,7 +82,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ ⟪((↑) ∘ ν : G → ℝ), f ^ p⟫_[ℝ] + ∑ i, ↑(ν i) * ((f ^ (p - 1)) i * |f| i) :=
         (le_add_of_nonneg_left $ pow_inner_nonneg hf hν _)
       _ = _ := ?_
-    rw [wdLpNorm_pow_eq_sum hp₁.pos.ne']
+    rw [wLpNorm_pow_eq_sum hp₁.pos.ne']
     dsimp
     refine sum_congr rfl fun i _ ↦ ?_
     rw [← abs_of_nonneg ((Nat.Odd.sub_odd hp₁ odd_one).pow_nonneg $ f _), abs_pow,
@@ -116,8 +116,8 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
         | norm_num
   replace hf₁ : ‖f‖_[2 * p, ν] ≤ 3 := by
     calc
-      _ ≤ ‖f + 1‖_[2 * p, ν] + ‖(1 : G → ℝ)‖_[2 * p, ν] := wdLpNorm_le_add_wdLpNorm_add hp' _ _ _
-      _ ≤ (2 + 1 : ℝ) := (add_le_add hf₁ (by rw [wdLpNorm_one, hν₁, one_rpow]; positivity))
+      _ ≤ ‖f + 1‖_[2 * p, ν] + ‖(1 : G → ℝ)‖_[2 * p, ν] := wLpNorm_le_add_wLpNorm_add hp' _ _ _
+      _ ≤ (2 + 1 : ℝ) := (add_le_add hf₁ (by rw [wLpNorm_one, hν₁, one_rpow]; positivity))
       _ = 3 := by norm_num
   replace hp' := zero_lt_one.trans_le hp'
   have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i in T, ν i) * 3 ^ p := by
@@ -133,11 +133,11 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) :=
         (mul_le_mul_of_nonneg_left (sqrt_le_sqrt $ sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_)
       _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_
-      _ ≤ _ := mul_le_mul_of_nonneg_left (pow_le_pow_left wdLpNorm_nonneg hf₁ _) ?_
+      _ ≤ _ := mul_le_mul_of_nonneg_left (pow_le_pow_left wLpNorm_nonneg hf₁ _) ?_
     any_goals positivity
-    rw [wdLpNorm_eq_sum hp'.ne', NNReal.coe_mul, mul_inv, rpow_mul, NNReal.coe_natCast,
+    rw [wLpNorm_eq_sum hp'.ne', NNReal.coe_mul, mul_inv, rpow_mul, NNReal.coe_natCast,
       rpow_inv_natCast_pow]
-    simp only [wdLpNorm_eq_sum hp'.ne', sqrt_eq_rpow, Nonneg.coe_one, rpow_two,
+    simp only [wLpNorm_eq_sum hp'.ne', sqrt_eq_rpow, Nonneg.coe_one, rpow_two,
       abs_nonneg, NNReal.smul_def, rpow_mul, Pi.pow_apply, abs_pow, norm_eq_abs, mul_pow,
       rpow_natCast, smul_eq_mul, pow_mul, one_div, NNReal.coe_two]
     all_goals positivity
@@ -177,7 +177,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     _ ≤ (∑ i, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ :=
         rpow_le_rpow ?_ (sum_le_sum_of_subset_of_nonneg (subset_univ _) fun i _ _ ↦ ?_) ?_
     _ = _ := by
-        rw [wdLpNorm_eq_sum (NNReal.coe_ne_zero.1 _)]
+        rw [wLpNorm_eq_sum (NNReal.coe_ne_zero.1 _)]
         simp [NNReal.smul_def, hp'.ne', p']
         dsimp
         positivity
@@ -200,9 +200,9 @@ lemma unbalancing (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁
     _ ≤ ‖f + 1‖_[(⟨_, (p'_pos this hε₀ hε₁).le⟩ : ℝ≥0), ν] :=
       unbalancing' (2 * p + 3) this ((even_two_mul _).add_odd $ by decide) hε₀ hε₁ hf hν hν₁ $
         hε.trans $
-          wdLpNorm_mono_right
+          wLpNorm_mono_right
             (Nat.cast_le.2 $ le_add_of_le_left $ le_mul_of_one_le_left' one_le_two) _ _
-    _ ≤ _ := wdLpNorm_mono_right ?_ _ _
+    _ ≤ _ := wLpNorm_mono_right ?_ _ _
   calc
     _ ≤ 24 / ε * log (3 / ε) * ↑(2 * p + 3 * p) :=
       mul_le_mul_of_nonneg_left (Nat.cast_le.2 $ add_le_add_left

LeanAPAP/Prereqs/Chang.lean

@@ -126,7 +126,7 @@ lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G}
   obtain rfl | hn := eq_or_ne n 0
   · simp
   calc
-    _ = ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) := by rw [ndLpNorm_dft_indicate_pow]
+    _ = ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) := by rw [cLpNorm_dft_indicate_pow]
     _ ≤ (4 * rexp 2⁻¹ * sqrt ↑(2 * n) * ‖dft (𝟭 s)‖ₙ_[2]) ^ (2 * n) := by
         gcongr
         refine rudin_ineq (le_mul_of_one_le_right zero_le_two $ Nat.one_le_iff_ne_zero.2 hn)

LeanAPAP/Prereqs/Energy.lean

@@ -44,7 +44,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭
 @[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = s.card := by
   simp [boringEnergy_eq, indicate_apply]
 
-lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
+lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
     ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s := by
   obtain rfl | hn := n.eq_zero_or_pos
   · simp
@@ -53,7 +53,7 @@ lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
     _ = ⟪dft (𝟭 s ∗^ n), dft (𝟭 s ∗^ n)⟫ₙ_[ℂ] := ?_
     _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := nl2Inner_dft _ _
     _ = _ := ?_
-  · rw [ndLpNorm_pow_eq_expect]
+  · rw [cLpNorm_pow_eq_expect]
     simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_expect, Complex.ofReal_pow,
       ← Complex.conj_mul', nl2Inner_eq_expect, dft_iterConv_apply]
     positivity
@@ -64,5 +64,5 @@ lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
 
 lemma ndL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by
   rw [eq_comm, sqrt_eq_iff_sq_eq]
-  simpa using ndLpNorm_dft_indicate_pow 1 s
+  simpa using cLpNorm_dft_indicate_pow 1 s
   all_goals positivity

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -53,7 +53,7 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma dL2Norm_cft (f : α → ℂ) : ‖cft f‖_[2] = ‖f‖ₙ_[2] :=
-  (sq_eq_sq nnLpNorm_nonneg ndLpNorm_nonneg).1 $ Complex.ofReal_injective $ by
+  (sq_eq_sq nnLpNorm_nonneg cLpNorm_nonneg).1 $ Complex.ofReal_injective $ by
     push_cast; simpa only [nl2Inner_self, l2Inner_self] using l2Inner_cft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
@@ -159,13 +159,13 @@ lemma cft_ndconv (f g : α → ℂ) : cft (f ○ₙ g) = cft f * conj (cft g) :=
 --   push_cast
 --   simp_rw [pow_mul, ← Complex.mul_conj', conj_iterConv_apply, mul_pow]
 
-lemma ndLpNorm_nconv_le_ndLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) :
+lemma cLpNorm_nconv_le_cLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) :
     ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
   cases isEmpty_or_nonempty α
   · rw [Subsingleton.elim (f ∗ₙ f) (f ○ₙ f)]
   refine le_of_pow_le_pow_left hn₀ (by positivity) ?_
   obtain ⟨n, rfl⟩ := hn.two_dvd
-  simp_rw [ndLpNorm_pow_eq_expect hn₀, ← cft_inversion (f ∗ₙ f), ← cft_inversion (f ○ₙ f),
+  simp_rw [cLpNorm_pow_eq_expect hn₀, ← cft_inversion (f ∗ₙ f), ← cft_inversion (f ○ₙ f),
     cft_nconv, cft_ndconv, Pi.mul_apply]
   rw [← Real.norm_of_nonneg (expect_nonneg fun i _ ↦ ?_), ← Complex.norm_real]
   rw [Complex.ofReal_expect (univ : Finset α)]
@@ -194,8 +194,8 @@ lemma ndLpNorm_nconv_le_ndLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α
   -- refine expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
   -- ring
 
---TODO: Can we unify with `ndLpNorm_nconv_le_ndLpNorm_ndconv`?
-lemma ndLpNorm_nconv_le_ndLpNorm_ndconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) :
+--TODO: Can we unify with `cLpNorm_nconv_le_cLpNorm_ndconv`?
+lemma cLpNorm_nconv_le_cLpNorm_ndconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) :
     ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
-  simpa only [← Complex.coe_comp_nconv, ← Complex.coe_comp_ndconv, Complex.ndLpNorm_coe_comp] using
-    ndLpNorm_nconv_le_ndLpNorm_ndconv hn₀ hn ((↑) ∘ f)
+  simpa only [← Complex.coe_comp_nconv, ← Complex.coe_comp_ndconv, Complex.cLpNorm_coe_comp] using
+    cLpNorm_nconv_le_cLpNorm_ndconv hn₀ hn ((↑) ∘ f)

LeanAPAP/Prereqs/FourierTransform/Discrete.lean

@@ -48,7 +48,7 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma ndL2Norm_dft (f : α → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2] :=
-  (sq_eq_sq ndLpNorm_nonneg nnLpNorm_nonneg).1 $ Complex.ofReal_injective $ by
+  (sq_eq_sq cLpNorm_nonneg nnLpNorm_nonneg).1 $ Complex.ofReal_injective $ by
     push_cast; simpa only [nl2Inner_self, l2Inner_self] using nl2Inner_dft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/