Make cLpNorm_cconv_le_cLpNorm_cdconv sorry-free

LeanAPAP.lean

@@ -41,6 +41,7 @@ import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.FourierTransform.Compact
+import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex

LeanAPAP/FiniteField/Basic.lean

@@ -2,11 +2,12 @@ import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Prereqs.Convolution.ThreeAP
+import LeanAPAP.Prereqs.FourierTransform.Convolution
+import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
-import LeanAPAP.Prereqs.Function.Indicator.Complex
 
 /-!
 # Finite field case
@@ -119,8 +120,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
 
 variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ}
 
-lemma ap_in_ff (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens)
-    (hαA₂ : α ≤ A₂.dens) :
+lemma ap_in_ff (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
             2 ^ 27 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 / ε ^ 2 ∧
@@ -156,8 +156,8 @@ lemma ap_in_ff (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁
   sorry
 
 lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (hq : q.Prime)
-    (hε₀ : 0 < ε) (hε₁ : ε < 1) (hA₀ : A.Nonempty)
-    (hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
+    (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
+    (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
             2 ^ 179 * 𝓛 A.dens ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 ∧
@@ -169,15 +169,18 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
   let p' : ℝ := 240 / ε * log (6 / ε) * p
   let q' : ℕ := 2 * ⌈p' + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊
   let f : G → ℝ := balance (μ A)
+  have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁
+  obtain rfl | hA₀ := A.eq_empty_or_nonempty
+  · exact ⟨⊤, Classical.decPred _, by simp; positivity⟩
   have hα₀ : 0 < α := by positivity
   have hα₁ : α ≤ 1 := by unfold_let α; exact mod_cast A.dens_le_one
-  have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁
   have : 0 < p := by positivity
   have : 0 < log (6 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
   have : 0 < p' := by positivity
   have : 0 < log (64 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
   have : 0 < q' := by positivity
   have : q' ≤ 2 ^ 30 * 𝓛 γ / ε ^ 5 := sorry
+  have := global_dichotomy hA₀ hγC hγ hAC
   have :=
     calc
       1 + ε / 4 = 1 + ε / 2 / 2 := by ring
@@ -302,8 +305,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
       rw [abs_sub_comm, le_abs, le_sub_comm]
       norm_num at hB' ⊢
       exact .inl hB'.le
-    obtain ⟨V', _, hVV', hv'⟩ := di_in_ff hq₃ hq (by positivity) two_inv_lt_one
-      (by simpa using hα₀.trans_le hαβ) (by
+    obtain ⟨V', _, hVV', hv'⟩ := di_in_ff hq₃ hq (by positivity) two_inv_lt_one (by
       rwa [Finset.dens_image (Nat.Coprime.nsmul_right_bijective _)]
       simpa [card_eq_pow_finrank (K := ZMod q) (V := V), ZMod.card] using hq'.pow) hα₀ this
     rw [dLinftyNorm_eq_iSup_norm, ← Finset.sup'_univ_eq_ciSup, Finset.le_sup'_iff] at hv'

LeanAPAP/Mathlib/Algebra/Group/AddChar.lean

@@ -1,5 +1,11 @@
 import Mathlib.Algebra.Group.AddChar
 
+/-!
+# TODO
+
+Unsimp `AddChar.sub_apply`
+-/
+
 variable {G R : Type*}
 
 namespace AddChar

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -5,7 +5,9 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Algebra.Rat
 import Mathlib.Algebra.BigOperators.GroupWithZero.Action
+import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.Module.Pi
 import Mathlib.Data.Finset.Pointwise.Basic
 import Mathlib.Data.Fintype.BigOperators
 
@@ -339,6 +341,11 @@ lemma expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) /
   simp_rw [div_eq_mul_inv, expect_mul]
 
 end Semifield
+
+@[simp] lemma expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)]
+    [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a) (a : α) :
+    (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a := by simp [expect]
+
 end Finset
 
 namespace algebraMap

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -1,5 +1,4 @@
 import LeanAPAP.Prereqs.Convolution.Compact
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 
@@ -65,6 +64,9 @@ lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a :=
     AddChar.sum_apply_eq_ite, sub_eq_zero, ite_mul, zero_mul, Fintype.expect_ite_eq]
   simp [add_neg_eq_zero, card_univ, NNRat.smul_def (α := ℂ), Fintype.card_ne_zero]
 
+/-- **Fourier inversion** for the discrete Fourier transform. -/
+lemma cft_inversion' (f : α → ℂ) : ∑ ψ, cft f ψ • ⇑ψ = f := by ext; simpa using cft_inversion _ _
+
 lemma dft_cft_doubleDualEmb (f : α → ℂ) (a : α) : dft (cft f) (doubleDualEmb a) = f (-a) := by
   simp only [← cft_inversion f (-a), mul_comm (conj _), dft_apply, dL2Inner_eq_sum, map_neg_eq_inv,
     AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
@@ -126,8 +128,8 @@ variable [DecidableEq α]
     dens, NNRat.smul_def (α := ℂ), div_eq_inv_mul]
   simp
 
-lemma cft_nconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by
-  simp_rw [cft, cL2Inner_eq_expect, nconv_eq_expect_sub', mul_expect, expect_mul, ← expect_product',
+lemma cft_cconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by
+  simp_rw [cft, cL2Inner_eq_expect, cconv_eq_expect_sub', mul_expect, expect_mul, ← expect_product',
     univ_product_univ]
   refine Fintype.expect_equiv ((Equiv.prodComm _ _).trans $
     ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _)  _ _ fun (a, b) ↦ ?_
@@ -137,69 +139,26 @@ lemma cft_nconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g
 
 lemma cft_cdconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) :
     cft (f ○ₙ g) ψ = cft f ψ * conj (cft g ψ) := by
-  rw [← nconv_conjneg, cft_nconv_apply, cft_conjneg_apply]
+  rw [← cconv_conjneg, cft_cconv_apply, cft_conjneg_apply]
 
-@[simp] lemma cft_nconv (f g : α → ℂ) : cft (f ∗ₙ g) = cft f * cft g :=
-  funext $ cft_nconv_apply _ _
+@[simp] lemma cft_cconv (f g : α → ℂ) : cft (f ∗ₙ g) = cft f * cft g :=
+  funext $ cft_cconv_apply _ _
 
 @[simp]
 lemma cft_cdconv (f g : α → ℂ) : cft (f ○ₙ g) = cft f * conj (cft g) :=
   funext $ cft_cdconv_apply _ _
 
-@[simp] lemma cft_iterNConv (f : α → ℂ) : ∀ n, cft (f ∗^ₙ n) = cft f ^ n
+@[simp] lemma cft_iterCconv (f : α → ℂ) : ∀ n, cft (f ∗^ₙ n) = cft f ^ n
   | 0 => cft_trivNChar
-  | n + 1 => by simp [iterNConv_succ, pow_succ, cft_iterNConv]
+  | n + 1 => by simp [iterCconv_succ, pow_succ, cft_iterCconv]
 
-@[simp] lemma cft_iterNConv_apply (f : α → ℂ) (n : ℕ) (ψ : AddChar α ℂ) :
-    cft (f ∗^ₙ n) ψ = cft f ψ ^ n := congr_fun (cft_iterNConv _ _) _
+@[simp] lemma cft_iterCconv_apply (f : α → ℂ) (n : ℕ) (ψ : AddChar α ℂ) :
+    cft (f ∗^ₙ n) ψ = cft f ψ ^ n := congr_fun (cft_iterCconv _ _) _
 
--- lemma dL2Norm_iterNConv (f : α → ℂ) (n : ℕ) : ‖f ∗^ₙ n‖ₙ_[2] = ‖f ^ n‖_[2] := by
---   rw [← dL2Norm_cft, cft_iterNConv, ← ENNReal.coe_two, dLpNorm_pow]
+-- lemma dL2Norm_iterCconv (f : α → ℂ) (n : ℕ) : ‖f ∗^ₙ n‖ₙ_[2] = ‖f ^ n‖_[2] := by
+--   rw [← dL2Norm_cft, cft_iterCconv, ← ENNReal.coe_two, dLpNorm_pow]
 --   norm_cast
 --   refine (sq_eq_sq (by positivity) $ by positivity).1 ?_
 --   rw [← ENNReal.coe_two, dLpNorm_pow, ← pow_mul', ← Complex.ofReal_inj]
 --   push_cast
 --   simp_rw [pow_mul, ← Complex.mul_conj', conj_iterConv_apply, mul_pow]
-
-variable [MeasurableSpace α] [DiscreteMeasurableSpace α]
-
-lemma cLpNorm_nconv_le_cLpNorm_cdconv (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 [← NNReal.coe_le_coe, NNReal.coe_pow, cLpNorm_pow_eq_expect_norm hn₀,
-    ← cft_inversion (f ∗ₙ f), ← cft_inversion (f ○ₙ f), cft_nconv, cft_cdconv, Pi.mul_apply]
-  rw [← Real.norm_of_nonneg (expect_nonneg fun i _ ↦ ?_), ← Complex.norm_real]
-  rw [Complex.ofReal_expect (univ : Finset α)]
-  any_goals positivity
-  simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_pow, ← Complex.conj_mul', map_pow, map_sum,
-    map_mul, Fintype.sum_pow, Fintype.sum_mul_sum]
-  sorry
-  -- simp only [@expect_comm _ _ α, ← mul_expect, prod_mul_prod_comm]
-  -- refine (norm_expect_le _ _).trans_eq (Complex.ofReal_injective _)
-  -- simp only [norm_mul, norm_prod, RCLike.norm_conj, ← pow_mul]
-  -- push_cast
-  -- have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by
-  --   rintro f g
-  --   suffices : ∑ a, ∏ i, conj (f i a) * g i a = if ∑ i, (g i - f i) = 0 then (card α : ℂ) else 0
-  --   · rw [this]
-  --     split_ifs <;> positivity
-  --   simp_rw [← AddChar.expect_eq_ite, AddChar.expect_apply, AddChar.sub_apply, AddChar.map_neg_eq_inv,
-  --     AddChar.inv_apply_eq_conj, mul_comm]
-  -- simp only [RCLike.ofReal_pow, pow_mul, ← Complex.conj_mul', map_expect, map_mul, Complex.conj_conj,
-  --   Pi.conj_apply, mul_pow, Fintype.expect_pow, ← sq, Fintype.expect_mul_expect]
-  -- conv_lhs =>
-  --   arg 2
-  --   ext
-  --   rw [← Complex.eq_coe_norm_of_nonneg (this _ _)]
-  -- simp only [@expect_comm _ _ α, mul_expect, map_prod, map_mul, RCLike.conj_conj, ← prod_mul_distrib]
-  -- refine expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
-  -- ring
-
---TODO: Can we unify with `cLpNorm_nconv_le_cLpNorm_cdconv`?
-lemma cLpNorm_nconv_le_cLpNorm_cdconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) :
-    ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
-  simpa only [← Complex.coe_comp_nconv, ← Complex.coe_comp_cdconv, Complex.cLpNorm_coe_comp] using
-    cLpNorm_nconv_le_cLpNorm_cdconv hn₀ hn ((↑) ∘ f)

LeanAPAP/Prereqs/FourierTransform/Convolution.lean

@@ -0,0 +1,62 @@
+import LeanAPAP.Prereqs.AddChar.MeasurableSpace
+import LeanAPAP.Prereqs.AddChar.PontryaginDuality
+import LeanAPAP.Prereqs.Convolution.Compact
+import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.Inner.Compact.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.FourierTransform.Compact
+
+open AddChar Finset Function MeasureTheory
+open Fintype (card)
+open scoped BigOperators ComplexConjugate ComplexOrder
+
+variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G] [MeasurableSpace G]
+  [DiscreteMeasurableSpace G] {ψ : AddChar G ℂ} {n : ℕ}
+
+set_option pp.piBinderTypes false
+
+lemma cLpNorm_cconv_le_cLpNorm_cdconv (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) :
+    ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
+  refine le_of_pow_le_pow_left hn₀ (by positivity) ?_
+  obtain ⟨k, rfl⟩ := hn.two_dvd
+  simp only [ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hn₀
+  refine Complex.le_of_eq_sum_of_eq_sum_norm (fun ψ : (Fin k → AddChar G ℂ) × (Fin k → AddChar G ℂ)
+    ↦ conj (∏ i, cft f (ψ.1 i) ^ 2) * (∏ i, cft f (ψ.2 i) ^ 2) * 𝔼 x, (∑ i, ψ.2 i - ∑ i, ψ.1 i) x)
+    univ (by dsimp; norm_cast; positivity) ?_ ?_
+  · simp only [NNReal.val_eq_coe]
+    push_cast
+    rw [← cft_inversion' (f ∗ₙ f), cLpNorm_two_mul_sum_pow hn₀]
+    simp_rw [cft_cconv_apply, ← sq, Fintype.sum_prod_type, mul_expect]
+    simp [mul_mul_mul_comm, mul_comm, map_neg_eq_conj, prod_mul_distrib]
+  · simp only [NNReal.val_eq_coe]
+    push_cast
+    rw [← cft_inversion' (f ○ₙ f), cLpNorm_two_mul_sum_pow hn₀]
+    simp_rw [cft_cdconv_apply, Complex.mul_conj', Fintype.sum_prod_type, mul_expect]
+    congr 1 with ψ
+    congr 1 with φ
+    simp only [Pi.smul_apply, smul_eq_mul, map_mul, map_pow, Complex.conj_ofReal, prod_mul_distrib,
+      mul_mul_mul_comm, ← mul_expect, map_prod, sub_apply, AddChar.coe_sum, Finset.prod_apply,
+      norm_mul, norm_prod, norm_pow, RCLike.norm_conj, Complex.ofReal_mul, Complex.ofReal_prod,
+      Complex.ofReal_pow]
+    congr 1
+    calc
+      𝔼 x, (∏ i, conj (ψ i x)) * ∏ i, φ i x = 𝔼 x, (∑ i, φ i - ∑ i, ψ i) x := by
+        simp [map_neg_eq_conj, mul_comm]
+      _ = ‖𝔼 x, (∑ i, φ i - ∑ i, ψ i) x‖ := by simp [expect_eq_ite, -sub_apply, apply_ite]
+      _ = ‖𝔼 x, (∏ i, φ i x) * ∏ i, (ψ i) (-x)‖ := by
+        simp [map_neg_eq_conj, mul_comm]
+
+lemma dLpNorm_conv_le_dLpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) :
+    ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := sorry
+
+-- TODO: Can we unify with `cLpNorm_cconv_le_cLpNorm_cdconv`?
+lemma cLpNorm_cconv_le_cLpNorm_cdconv' (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℝ) :
+    ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
+  simpa only [← Complex.coe_comp_cconv, ← Complex.coe_comp_cdconv, Complex.cLpNorm_coe_comp] using
+    cLpNorm_cconv_le_cLpNorm_cdconv hn₀ hn ((↑) ∘ f)
+
+-- TODO: Can we unify with `dLpNorm_conv_le_dLpNorm_dconv`?
+lemma dLpNorm_conv_le_dLpNorm_dconv' (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℝ) :
+    ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by
+  simpa only [← Complex.coe_comp_conv, ← Complex.coe_comp_dconv, Complex.dLpNorm_coe_comp] using
+    dLpNorm_conv_le_dLpNorm_dconv hn₀ hn ((↑) ∘ f)

LeanAPAP/Prereqs/FourierTransform/Discrete.lean

@@ -3,7 +3,6 @@ import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Compact.Basic
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # Discrete Fourier transform
@@ -64,10 +63,7 @@ lemma dft_inversion (f : α → ℂ) (a : α) : 𝔼 ψ, dft f ψ * ψ a = f a :
     AddChar.expect_apply_eq_ite, sub_eq_zero, boole_mul, Fintype.sum_ite_eq]
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
-lemma dft_inversion' (f : α → ℂ) (a : α) : ∑ ψ : AddChar α ℂ, dft f ψ * ψ a = card α * f a := by
-  rw [mul_comm, ← div_eq_iff, ← dft_inversion f, ← AddChar.card_eq,
-    Fintype.expect_eq_sum_div_card (M := ℂ)]
-  simp
+lemma dft_inversion' (f : α → ℂ) : 𝔼 ψ, dft f ψ • ⇑ψ = f := by ext; simpa using dft_inversion f _
 
 lemma dft_dft_doubleDualEmb (f : α → ℂ) (a : α) :
     dft (dft f) (doubleDualEmb a) = card α * f (-a) := by
@@ -147,59 +143,3 @@ lemma dft_dconv (f g : α → ℂ) : dft (f ○ g) = dft f * conj (dft g) := fun
 
 @[simp] lemma dft_iterConv_apply (f : α → ℂ) (n : ℕ) (ψ : AddChar α ℂ) :
     dft (f ∗^ n) ψ = dft f ψ ^ n := congr_fun (dft_iterConv _ _) _
-
-variable [MeasurableSpace α] [DiscreteMeasurableSpace α]
-
-lemma dLpNorm_conv_le_dLpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) :
-    ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by
-  refine le_of_pow_le_pow_left hn₀ (by positivity) ?_
-  obtain ⟨k, hnk⟩ := hn.two_dvd
-  calc ‖f ∗ f‖_[n] ^ n
-      = ∑ x, ‖(f ∗ f) x‖₊ ^ n := dLpNorm_pow_eq_sum_nnnorm hn₀ _
-    _ = ∑ x, ‖(𝔼 ψ, dft f ψ ^ 2 * ψ x)‖₊ ^ n := by
-        simp_rw [← nnnorm_pow, ← dft_inversion (f ∗ f), dft_conv_apply, sq]
-    _ ≤ ∑ x, ‖𝔼 ψ, ‖dft f ψ‖₊ ^ 2 * ψ x‖₊ ^ n := Complex.le_of_eq_sum_of_eq_sum_norm
-          (fun ψ : (Fin n → AddChar α ℂ) × (Fin n → AddChar α ℂ) ↦ conj (∏ i, dft f (ψ.1 i) ^ 2) *
-            (∏ i, dft f (ψ.2 i) ^ 2) * ∑ x, (∑ i, ψ.1 i - ∑ i, ψ.2 i) x) univ
-            (by dsimp; norm_cast; positivity) ?_ ?_
-    _ = ∑ x, ‖(f ○ f) x‖₊ ^ n := by
-        simp_rw [← nnnorm_pow, ← dft_inversion (f ○ f), dft_dconv_apply, Complex.mul_conj']; simp
-    _ = ‖f ○ f‖_[n] ^ n := (dLpNorm_pow_eq_sum_nnnorm hn₀ _).symm
-  · simp only [NNReal.val_eq_coe]
-    push_cast
-    simp_rw [hnk, pow_mul, ← Complex.conj_mul', map_expect, mul_pow, expect_pow, expect_mul_expect]
-    sorry
-  sorry
---   simp_rw [dLpNorm_pow_eq_sum_nnnorm hn₀, mul_sum, ← mul_pow, ← nsmul_eq_mul, ← norm_nsmul, nsmul_eq_mul,
---     ← dft_inversion', dft_conv, dft_dconv, Pi.mul_apply]
---   rw [← Real.norm_of_nonneg (sum_nonneg fun i _ ↦ ?_), ← Complex.norm_real]
---   rw [Complex.ofReal_sum (univ : Finset α)]
---   any_goals positivity
---   simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_pow, ← Complex.conj_mul', map_pow, map_sum,
---     map_mul, Fintype.sum_pow, Fintype.sum_mul_sum]
---   simp only [@sum_comm _ _ α, ← mul_sum, prod_mul_prod_comm]
---   refine (norm_sum_le _ _).trans_eq (Complex.ofReal_injective _)
---   simp only [norm_mul, norm_prod, RCLike.norm_conj, ← pow_mul]
---   push_cast
---   have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by
---     rintro f g
---     suffices : ∑ a, ∏ i, conj (f i a) * g i a = if ∑ i, (g i - f i) = 0 then (card α : ℂ) else 0
---     · rw [this]
---       split_ifs <;> positivity
---     simp_rw [← AddChar.sum_eq_ite, AddChar.sum_apply, AddChar.sub_apply, AddChar.map_neg_eq_inv,
---       AddChar.inv_apply_eq_conj, mul_comm]
---   simp only [RCLike.ofReal_pow, pow_mul, ← Complex.conj_mul', map_sum, map_mul, Complex.conj_conj,
---     Pi.conj_apply, mul_pow, Fintype.sum_pow, ← sq, Fintype.sum_mul_sum]
---   conv_lhs =>
---     arg 2
---     ext
---     rw [← Complex.eq_coe_norm_of_nonneg (this _ _)]
---   simp only [@sum_comm _ _ α, mul_sum, map_prod, map_mul, RCLike.conj_conj, ← prod_mul_distrib]
---   refine sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
---   ring
-
---TODO: Can we unify with `dLpNorm_conv_le_dLpNorm_dconv`?
-lemma dLpNorm_conv_le_dLpNorm_dconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) :
-    ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by
-  simpa only [← Complex.coe_comp_conv, ← Complex.coe_comp_dconv, Complex.dLpNorm_coe_comp] using
-    dLpNorm_conv_le_dLpNorm_dconv hn₀ hn ((↑) ∘ f)

LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean

@@ -13,6 +13,8 @@ open Function ProbabilityTheory Real
 open Fintype (card)
 open scoped BigOperators ComplexConjugate ENNReal NNReal
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 variable {α 𝕜 R E : Type*} [MeasurableSpace α]
 
 /-! ### Lp norm -/
@@ -218,6 +220,20 @@ lemma cLinftyNorm_eq_iSup_norm (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i
 lemma cLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] :=
   nnLpNorm_mono_real .of_discrete h
 
+lemma cLpNorm_two_mul_sum_pow {ι : Type*} {n : ℕ} (hn : n ≠ 0) (s : Finset ι) (f : ι → α → ℂ) :
+    ‖∑ i ∈ s, f i‖ₙ_[2 * n] ^ (2 * n) =
+      ∑ x ∈ s ^^ n, ∑ y ∈ s ^^ n, 𝔼 a, (∏ i, conj (f (x i) a)) * ∏ i, f (y i) a :=
+  calc
+    _ = 𝔼 a, (‖∑ i ∈ s, f i a‖ : ℂ) ^ (2 * n) := by
+      norm_cast
+      rw [← cLpNorm_pow_eq_expect_norm]
+      simp_rw [← sum_apply]
+      norm_cast
+      positivity
+    _ = 𝔼 a, (∑ i ∈ s, conj (f i a)) ^ n * (∑ j ∈ s, f j a) ^ n := by
+      simp_rw [pow_mul, ← Complex.conj_mul', mul_pow, map_sum]
+    _ = _ := by simp_rw [sum_pow', sum_mul_sum, expect_sum_comm]
+
 end NormedAddCommGroup
 
 /-! ### Hölder inequality -/