diff --git a/LeanAPAP.lean b/LeanAPAP.lean index fb31482c5d..8176952b61 100644 --- a/LeanAPAP.lean +++ b/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 diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index a07bf62416..2a4ed004b4 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/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' diff --git a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean b/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean index 4bc3c8ede1..cfc129fb05 100644 --- a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index 8691deb599..2aff9ec186 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/LeanAPAP/Prereqs/Convolution/Compact.lean @@ -10,9 +10,9 @@ normalisation. ## Main declarations -* `nconv`: Discrete convolution of two functions in the compact normalisation +* `cconv`: Discrete convolution of two functions in the compact normalisation * `cdconv`: Discrete difference convolution of two functions in the compact normalisation -* `iterNConv`: Iterated convolution of a function in the compact normalisation +* `iterCconv`: Iterated convolution of a function in the compact normalisation ## Notation @@ -71,123 +71,123 @@ section Semifield variable [Semifield R] [CharZero R] {f g : G → R} /-- Convolution -/ -def nconv (f g : G → R) : G → R := fun a ↦ 𝔼 x : G × G with x.1 + x.2 = a , f x.1 * g x.2 +def cconv (f g : G → R) : G → R := fun a ↦ 𝔼 x : G × G with x.1 + x.2 = a , f x.1 * g x.2 -infixl:71 " ∗ₙ " => nconv +infixl:71 " ∗ₙ " => cconv -lemma nconv_apply (f g : G → R) (a : G) : +lemma cconv_apply (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := rfl -lemma nconv_apply_eq_smul_conv (f g : G → R) (a : G) : +lemma cconv_apply_eq_smul_conv (f g : G → R) (a : G) : (f ∗ₙ g) a = (f ∗ g) a /ℚ Fintype.card G := by - rw [nconv_apply, expect, eq_comm] + rw [cconv_apply, expect, eq_comm] congr 3 refine card_nbij' (fun b ↦ (b, a - b)) Prod.fst ?_ ?_ ?_ ?_ <;> simp [eq_sub_iff_add_eq', eq_comm] -lemma nconv_eq_smul_conv (f g : G → R) : f ∗ₙ g = (f ∗ g) /ℚ Fintype.card G := - funext $ nconv_apply_eq_smul_conv _ _ +lemma cconv_eq_smul_conv (f g : G → R) : f ∗ₙ g = (f ∗ g) /ℚ Fintype.card G := + funext $ cconv_apply_eq_smul_conv _ _ -@[simp] lemma nconv_zero (f : G → R) : f ∗ₙ 0 = 0 := by ext; simp [nconv_apply] -@[simp] lemma zero_nconv (f : G → R) : 0 ∗ₙ f = 0 := by ext; simp [nconv_apply] +@[simp] lemma cconv_zero (f : G → R) : f ∗ₙ 0 = 0 := by ext; simp [cconv_apply] +@[simp] lemma zero_cconv (f : G → R) : 0 ∗ₙ f = 0 := by ext; simp [cconv_apply] -lemma nconv_add (f g h : G → R) : f ∗ₙ (g + h) = f ∗ₙ g + f ∗ₙ h := by - ext; simp [nconv_apply, mul_add, expect_add_distrib] +lemma cconv_add (f g h : G → R) : f ∗ₙ (g + h) = f ∗ₙ g + f ∗ₙ h := by + ext; simp [cconv_apply, mul_add, expect_add_distrib] -lemma add_nconv (f g h : G → R) : (f + g) ∗ₙ h = f ∗ₙ h + g ∗ₙ h := by - ext; simp [nconv_apply, add_mul, expect_add_distrib] +lemma add_cconv (f g h : G → R) : (f + g) ∗ₙ h = f ∗ₙ h + g ∗ₙ h := by + ext; simp [cconv_apply, add_mul, expect_add_distrib] -lemma smul_nconv [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) +lemma smul_cconv [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ∗ₙ g = c • (f ∗ₙ g) := by have := SMulCommClass.symm H R R ext a - simp only [Pi.smul_apply, smul_expect, nconv_apply, smul_mul_assoc] + simp only [Pi.smul_apply, smul_expect, cconv_apply, smul_mul_assoc] -lemma nconv_smul [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) +lemma cconv_smul [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : f ∗ₙ c • g = c • (f ∗ₙ g) := by have := SMulCommClass.symm H R R ext a - simp only [Pi.smul_apply, smul_expect, nconv_apply, mul_smul_comm] + simp only [Pi.smul_apply, smul_expect, cconv_apply, mul_smul_comm] -alias smul_nconv_assoc := smul_nconv -alias smul_nconv_left_comm := nconv_smul +alias smul_cconv_assoc := smul_cconv +alias smul_cconv_left_comm := cconv_smul -@[simp] lemma translate_nconv (a : G) (f g : G → R) : τ a f ∗ₙ g = τ a (f ∗ₙ g) := +@[simp] lemma translate_cconv (a : G) (f g : G → R) : τ a f ∗ₙ g = τ a (f ∗ₙ g) := funext fun b ↦ expect_equiv ((Equiv.subRight a).prodCongr $ Equiv.refl _) (by simp [sub_add_eq_add_sub]) (by simp) -@[simp] lemma nconv_translate (a : G) (f g : G → R) : f ∗ₙ τ a g = τ a (f ∗ₙ g) := +@[simp] lemma cconv_translate (a : G) (f g : G → R) : f ∗ₙ τ a g = τ a (f ∗ₙ g) := funext fun b ↦ expect_equiv ((Equiv.refl _).prodCongr $ Equiv.subRight a) (by simp [← add_sub_assoc]) (by simp) -lemma nconv_comm (f g : G → R) : f ∗ₙ g = g ∗ₙ f := +lemma cconv_comm (f g : G → R) : f ∗ₙ g = g ∗ₙ f := funext fun a ↦ Finset.expect_equiv (Equiv.prodComm _ _) (by simp [add_comm]) (by simp [mul_comm]) -lemma mul_smul_nconv_comm [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] +lemma mul_smul_cconv_comm [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] [SMulCommClass H R R] (c d : H) (f g : G → R) : (c * d) • (f ∗ₙ g) = c • f ∗ₙ d • g := by - rw [smul_nconv, nconv_smul, mul_smul] + rw [smul_cconv, cconv_smul, mul_smul] -lemma nconv_assoc (f g h : G → R) : f ∗ₙ g ∗ₙ h = f ∗ₙ (g ∗ₙ h) := by - simp only [nconv_eq_smul_conv, smul_conv, conv_smul, conv_assoc] +lemma cconv_assoc (f g h : G → R) : f ∗ₙ g ∗ₙ h = f ∗ₙ (g ∗ₙ h) := by + simp only [cconv_eq_smul_conv, smul_conv, conv_smul, conv_assoc] -lemma nconv_right_comm (f g h : G → R) : f ∗ₙ g ∗ₙ h = f ∗ₙ h ∗ₙ g := by - rw [nconv_assoc, nconv_assoc, nconv_comm g] +lemma cconv_right_comm (f g h : G → R) : f ∗ₙ g ∗ₙ h = f ∗ₙ h ∗ₙ g := by + rw [cconv_assoc, cconv_assoc, cconv_comm g] -lemma nconv_left_comm (f g h : G → R) : f ∗ₙ (g ∗ₙ h) = g ∗ₙ (f ∗ₙ h) := by - rw [← nconv_assoc, ← nconv_assoc, nconv_comm g] +lemma cconv_left_comm (f g h : G → R) : f ∗ₙ (g ∗ₙ h) = g ∗ₙ (f ∗ₙ h) := by + rw [← cconv_assoc, ← cconv_assoc, cconv_comm g] -lemma nconv_nconv_nconv_comm (f g h i : G → R) : f ∗ₙ g ∗ₙ (h ∗ₙ i) = f ∗ₙ h ∗ₙ (g ∗ₙ i) := by - rw [nconv_assoc, nconv_assoc, nconv_left_comm g] +lemma cconv_cconv_cconv_comm (f g h i : G → R) : f ∗ₙ g ∗ₙ (h ∗ₙ i) = f ∗ₙ h ∗ₙ (g ∗ₙ i) := by + rw [cconv_assoc, cconv_assoc, cconv_left_comm g] -lemma map_nconv [Semifield S] [CharZero S] (m : R →+* S) (f g : G → R) (a : G) : m +lemma map_cconv [Semifield S] [CharZero S] (m : R →+* S) (f g : G → R) (a : G) : m ((f ∗ₙ g) a) = (m ∘ f ∗ₙ m ∘ g) a := by - simp_rw [nconv_apply, map_expect, map_mul, Function.comp_apply] + simp_rw [cconv_apply, map_expect, map_mul, Function.comp_apply] -lemma comp_nconv [Semifield S] [CharZero S] (m : R →+* S) (f g : G → R) : - m ∘ (f ∗ₙ g) = m ∘ f ∗ₙ m ∘ g := funext $ map_nconv _ _ _ +lemma comp_cconv [Semifield S] [CharZero S] (m : R →+* S) (f g : G → R) : + m ∘ (f ∗ₙ g) = m ∘ f ∗ₙ m ∘ g := funext $ map_cconv _ _ _ -lemma nconv_eq_expect_sub (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (a - t) * g t := by - rw [nconv_apply] +lemma cconv_eq_expect_sub (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (a - t) * g t := by + rw [cconv_apply] refine expect_nbij (fun x ↦ x.2) (fun x _ ↦ mem_univ _) ?_ ?_ fun b _ ↦ ⟨(a - b, b), mem_filter.2 ⟨mem_univ _, sub_add_cancel _ _⟩, rfl⟩ any_goals unfold Set.InjOn all_goals aesop -lemma nconv_eq_expect_add (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (a + t) * g (-t) := - (nconv_eq_expect_sub _ _ _).trans $ Fintype.expect_equiv (Equiv.neg _) _ _ fun t ↦ by +lemma cconv_eq_expect_add (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (a + t) * g (-t) := + (cconv_eq_expect_sub _ _ _).trans $ Fintype.expect_equiv (Equiv.neg _) _ _ fun t ↦ by simp only [sub_eq_add_neg, Equiv.neg_apply, neg_neg] -lemma nconv_eq_expect_sub' (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f t * g (a - t) := by - rw [nconv_comm, nconv_eq_expect_sub]; simp_rw [mul_comm] +lemma cconv_eq_expect_sub' (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f t * g (a - t) := by + rw [cconv_comm, cconv_eq_expect_sub]; simp_rw [mul_comm] -lemma nconv_eq_expect_add' (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (-t) * g (a + t) := by - rw [nconv_comm, nconv_eq_expect_add]; simp_rw [mul_comm] +lemma cconv_eq_expect_add' (f g : G → R) (a : G) : (f ∗ₙ g) a = 𝔼 t, f (-t) * g (a + t) := by + rw [cconv_comm, cconv_eq_expect_add]; simp_rw [mul_comm] -lemma nconv_apply_add (f g : G → R) (a b : G) : (f ∗ₙ g) (a + b) = 𝔼 t, f (a + t) * g (b - t) := - (nconv_eq_expect_sub _ _ _).trans $ Fintype.expect_equiv (Equiv.subLeft b) _ _ fun t ↦ by +lemma cconv_apply_add (f g : G → R) (a b : G) : (f ∗ₙ g) (a + b) = 𝔼 t, f (a + t) * g (b - t) := + (cconv_eq_expect_sub _ _ _).trans $ Fintype.expect_equiv (Equiv.subLeft b) _ _ fun t ↦ by simp [add_sub_assoc, ← sub_add] -lemma expect_nconv_mul (f g h : G → R) : +lemma expect_cconv_mul (f g h : G → R) : 𝔼 a, (f ∗ₙ g) a * h a = 𝔼 a, 𝔼 b, f a * g b * h (a + b) := by - simp_rw [nconv_eq_expect_sub', expect_mul] + simp_rw [cconv_eq_expect_sub', expect_mul] rw [expect_comm] exact expect_congr rfl fun x _ ↦ Fintype.expect_equiv (Equiv.subRight x) _ _ fun y ↦ by simp -lemma expect_nconv (f g : G → R) : 𝔼 a, (f ∗ₙ g) a = (𝔼 a, f a) * 𝔼 a, g a := by - simpa only [expect_mul_expect, Pi.one_apply, mul_one] using expect_nconv_mul f g 1 +lemma expect_cconv (f g : G → R) : 𝔼 a, (f ∗ₙ g) a = (𝔼 a, f a) * 𝔼 a, g a := by + simpa only [expect_mul_expect, Pi.one_apply, mul_one] using expect_cconv_mul f g 1 -@[simp] lemma nconv_const (f : G → R) (b : R) : f ∗ₙ const _ b = const _ ((𝔼 x, f x) * b) := by - ext; simp [nconv_eq_expect_sub', expect_mul] +@[simp] lemma cconv_const (f : G → R) (b : R) : f ∗ₙ const _ b = const _ ((𝔼 x, f x) * b) := by + ext; simp [cconv_eq_expect_sub', expect_mul] -@[simp] lemma const_nconv (b : R) (f : G → R) : const _ b ∗ₙ f = const _ (b * 𝔼 x, f x) := by - ext; simp [nconv_eq_expect_sub, mul_expect] +@[simp] lemma const_cconv (b : R) (f : G → R) : const _ b ∗ₙ f = const _ (b * 𝔼 x, f x) := by + ext; simp [cconv_eq_expect_sub, mul_expect] -@[simp] lemma nconv_trivNChar (f : G → R) : f ∗ₙ trivNChar = f := by - ext a; simp [nconv_eq_expect_sub, card_univ, NNRat.smul_def, mul_comm] +@[simp] lemma cconv_trivNChar (f : G → R) : f ∗ₙ trivNChar = f := by + ext a; simp [cconv_eq_expect_sub, card_univ, NNRat.smul_def, mul_comm] -@[simp] lemma trivNChar_nconv (f : G → R) : trivNChar ∗ₙ f = f := by - rw [nconv_comm, nconv_trivNChar] +@[simp] lemma trivNChar_cconv (f : G → R) : trivNChar ∗ₙ f = f := by + rw [cconv_comm, cconv_trivNChar] -lemma support_nconv_subset (f g : G → R) : support (f ∗ₙ g) ⊆ support f + support g := by +lemma support_cconv_subset (f g : G → R) : support (f ∗ₙ g) ⊆ support f + support g := by rintro a ha obtain ⟨x, hx, h⟩ := exists_ne_zero_of_expect_ne_zero ha exact ⟨_, left_ne_zero_of_mul h, _, right_ne_zero_of_mul h, (mem_filter.1 hx).2⟩ @@ -211,13 +211,13 @@ lemma cdconv_apply_eq_smul_dconv (f g : G → R) (a : G) : lemma cdconv_eq_smul_dconv (f g : G → R) : (f ○ₙ g) = (f ○ g) /ℚ Fintype.card G := funext $ cdconv_apply_eq_smul_dconv _ _ -@[simp] lemma nconv_conjneg (f g : G → R) : f ∗ₙ conjneg g = f ○ₙ g := +@[simp] lemma cconv_conjneg (f g : G → R) : f ∗ₙ conjneg g = f ○ₙ g := funext fun a ↦ expect_bij (fun x _ ↦ (x.1, -x.2)) (fun x hx ↦ by simpa using hx) (fun x _ ↦ rfl) (fun x y _ _ h ↦ by simpa [Prod.ext_iff] using h) fun x hx ↦ ⟨(x.1, -x.2), by simpa [sub_eq_add_neg] using hx, by simp⟩ @[simp] lemma cdconv_conjneg (f g : G → R) : f ○ₙ conjneg g = f ∗ₙ g := by - rw [← nconv_conjneg, conjneg_conjneg] + rw [← cconv_conjneg, conjneg_conjneg] @[simp] lemma translate_cdconv (a : G) (f g : G → R) : τ a f ○ₙ g = τ a (f ○ₙ g) := funext fun b ↦ expect_equiv ((Equiv.subRight a).prodCongr $ Equiv.refl _) @@ -227,35 +227,35 @@ lemma cdconv_eq_smul_dconv (f g : G → R) : (f ○ₙ g) = (f ○ g) /ℚ Finty funext fun b ↦ expect_equiv ((Equiv.refl _).prodCongr $ Equiv.subRight a) (by simp [sub_sub_eq_add_sub, ← sub_add_eq_add_sub]) (by simp) -@[simp] lemma conj_nconv (f g : G → R) : conj (f ∗ₙ g) = conj f ∗ₙ conj g := - funext fun a ↦ by simp only [Pi.conj_apply, nconv_apply, map_expect, map_mul] +@[simp] lemma conj_cconv (f g : G → R) : conj (f ∗ₙ g) = conj f ∗ₙ conj g := + funext fun a ↦ by simp only [Pi.conj_apply, cconv_apply, map_expect, map_mul] @[simp] lemma conj_cdconv (f g : G → R) : conj (f ○ₙ g) = conj f ○ₙ conj g := by - simp_rw [← nconv_conjneg, conj_nconv, conjneg_conj] + simp_rw [← cconv_conjneg, conj_cconv, conjneg_conj] -lemma IsSelfAdjoint.nconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ₙ g) := - (conj_nconv _ _).trans $ congr_arg₂ _ hf hg +lemma IsSelfAdjoint.cconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ₙ g) := + (conj_cconv _ _).trans $ congr_arg₂ _ hf hg lemma IsSelfAdjoint.cdconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ₙ g) := (conj_cdconv _ _).trans $ congr_arg₂ _ hf hg -@[simp]lemma conjneg_nconv (f g : G → R) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g := by +@[simp]lemma conjneg_cconv (f g : G → R) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g := by funext a - simp only [nconv_apply, conjneg_apply, map_expect, map_mul] + simp only [cconv_apply, conjneg_apply, map_expect, map_mul] exact Finset.expect_equiv (Equiv.neg (G × G)) (by simp [eq_comm, ← neg_eq_iff_eq_neg, add_comm]) (by simp) @[simp] lemma conjneg_cdconv (f g : G → R) : conjneg (f ○ₙ g) = g ○ₙ f := by - simp_rw [← nconv_conjneg, conjneg_nconv, conjneg_conjneg, nconv_comm] + simp_rw [← cconv_conjneg, conjneg_cconv, conjneg_conjneg, cconv_comm] -@[simp] lemma cdconv_zero (f : G → R) : f ○ₙ 0 = 0 := by simp [← nconv_conjneg] -@[simp] lemma zero_cdconv (f : G → R) : 0 ○ₙ f = 0 := by rw [← nconv_conjneg]; simp [-nconv_conjneg] +@[simp] lemma cdconv_zero (f : G → R) : f ○ₙ 0 = 0 := by simp [← cconv_conjneg] +@[simp] lemma zero_cdconv (f : G → R) : 0 ○ₙ f = 0 := by rw [← cconv_conjneg]; simp [-cconv_conjneg] lemma cdconv_add (f g h : G → R) : f ○ₙ (g + h) = f ○ₙ g + f ○ₙ h := by - simp_rw [← nconv_conjneg, conjneg_add, nconv_add] + simp_rw [← cconv_conjneg, conjneg_add, cconv_add] lemma add_cdconv (f g h : G → R) : (f + g) ○ₙ h = f ○ₙ h + g ○ₙ h := by - simp_rw [← nconv_conjneg, add_nconv] + simp_rw [← cconv_conjneg, add_cconv] lemma smul_cdconv [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ○ₙ g = c • (f ○ₙ g) := by @@ -272,14 +272,14 @@ lemma cdconv_smul [Star H] [DistribSMul H R] [IsScalarTower H R R] [SMulCommClas alias smul_cdconv_assoc := smul_cdconv alias smul_cdconv_left_comm := cdconv_smul -lemma nconv_cdconv_nconv_comm (f g h i : G → R) : f ∗ₙ g ○ₙ (h ∗ₙ i) = f ○ₙ h ∗ₙ (g ○ₙ i) := by - simp_rw [← nconv_conjneg, conjneg_nconv, nconv_nconv_nconv_comm] +lemma cconv_cdconv_cconv_comm (f g h i : G → R) : f ∗ₙ g ○ₙ (h ∗ₙ i) = f ○ₙ h ∗ₙ (g ○ₙ i) := by + simp_rw [← cconv_conjneg, conjneg_cconv, cconv_cconv_cconv_comm] -lemma cdconv_nconv_cdconv_comm (f g h i : G → R) : f ○ₙ g ∗ₙ (h ○ₙ i) = f ∗ₙ h ○ₙ (g ∗ₙ i) := by - simp_rw [← nconv_conjneg, conjneg_nconv, nconv_nconv_nconv_comm] +lemma cdconv_cconv_cdconv_comm (f g h i : G → R) : f ○ₙ g ∗ₙ (h ○ₙ i) = f ∗ₙ h ○ₙ (g ∗ₙ i) := by + simp_rw [← cconv_conjneg, conjneg_cconv, cconv_cconv_cconv_comm] lemma cdconv_cdconv_cdconv_comm (f g h i : G → R) : f ○ₙ g ○ₙ (h ○ₙ i) = f ○ₙ h ○ₙ (g ○ₙ i) := by - simp_rw [← nconv_conjneg, conjneg_nconv, nconv_nconv_nconv_comm] + simp_rw [← cconv_conjneg, conjneg_cconv, cconv_cconv_cconv_comm] --TODO: Can we generalise to star ring homs? -- lemma map_cdconv (f g : G → ℝ≥0) (a : G) : (↑((f ○ₙ g) a) : ℝ) = ((↑) ∘ f ○ₙ (↑) ∘ g) a := by @@ -287,17 +287,17 @@ lemma cdconv_cdconv_cdconv_comm (f g h i : G → R) : f ○ₙ g ○ₙ (h ○ -- Function.comp_apply] lemma cdconv_eq_expect_add (f g : G → R) (a : G) : (f ○ₙ g) a = 𝔼 t, f (a + t) * conj (g t) := by - simp [← nconv_conjneg, nconv_eq_expect_add] + simp [← cconv_conjneg, cconv_eq_expect_add] lemma cdconv_eq_expect_sub (f g : G → R) (a : G) : (f ○ₙ g) a = 𝔼 t, f t * conj (g (t - a)) := by - simp [← nconv_conjneg, nconv_eq_expect_sub'] + simp [← cconv_conjneg, cconv_eq_expect_sub'] lemma cdconv_apply_neg (f g : G → R) (a : G) : (f ○ₙ g) (-a) = conj ((g ○ₙ f) a) := by rw [← conjneg_cdconv f, conjneg_apply, Complex.conj_conj] lemma cdconv_apply_sub (f g : G → R) (a b : G) : (f ○ₙ g) (a - b) = 𝔼 t, f (a + t) * conj (g (b + t)) := by - simp [← nconv_conjneg, sub_eq_add_neg, nconv_apply_add, add_comm] + simp [← cconv_conjneg, sub_eq_add_neg, cconv_apply_add, add_comm] lemma expect_cdconv_mul (f g h : G → R) : 𝔼 a, (f ○ₙ g) a * h a = 𝔼 a, 𝔼 b, f a * conj (g b) * h (a - b) := by @@ -317,17 +317,17 @@ lemma const_cdconv (b : R) (f : G → R) : const _ b ○ₙ f = const _ (b * ext; simp [cdconv_eq_expect_add, mul_expect] @[simp] lemma cdconv_trivNChar (f : G → R) : f ○ₙ trivNChar = f := by - rw [← nconv_conjneg, conjneg_trivNChar, nconv_trivNChar] + rw [← cconv_conjneg, conjneg_trivNChar, cconv_trivNChar] @[simp] lemma trivNChar_cdconv (f : G → R) : trivNChar ○ₙ f = conjneg f := by - rw [← nconv_conjneg, trivNChar_nconv] + rw [← cconv_conjneg, trivNChar_cconv] lemma support_cdconv_subset (f g : G → R) : support (f ○ₙ g) ⊆ support f - support g := by - simpa [sub_eq_add_neg] using support_nconv_subset f (conjneg g) + simpa [sub_eq_add_neg] using support_cconv_subset f (conjneg g) --- lemma indicate_nconv_indicate_apply (s t : Finset G) (a : G) : +-- lemma indicate_cconv_indicate_apply (s t : Finset G) (a : G) : -- (𝟭_[R] s ∗ₙ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 + x.2 = a).card := by --- simp only [nconv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, expect_boole] +-- simp only [cconv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, expect_boole] -- simp_rw [← mem_product, filter_univ_mem] -- lemma indicate_cdconv_indicate_apply (s t : Finset G) (a : G) : @@ -341,14 +341,14 @@ end Semifield section Field variable [Field R] [CharZero R] -@[simp] lemma nconv_neg (f g : G → R) : f ∗ₙ -g = -(f ∗ₙ g) := by ext; simp [nconv_apply] -@[simp] lemma neg_nconv (f g : G → R) : -f ∗ₙ g = -(f ∗ₙ g) := by ext; simp [nconv_apply] +@[simp] lemma cconv_neg (f g : G → R) : f ∗ₙ -g = -(f ∗ₙ g) := by ext; simp [cconv_apply] +@[simp] lemma neg_cconv (f g : G → R) : -f ∗ₙ g = -(f ∗ₙ g) := by ext; simp [cconv_apply] -lemma nconv_sub (f g h : G → R) : f ∗ₙ (g - h) = f ∗ₙ g - f ∗ₙ h := by - simp only [sub_eq_add_neg, nconv_add, nconv_neg] +lemma cconv_sub (f g h : G → R) : f ∗ₙ (g - h) = f ∗ₙ g - f ∗ₙ h := by + simp only [sub_eq_add_neg, cconv_add, cconv_neg] -lemma sub_nconv (f g h : G → R) : (f - g) ∗ₙ h = f ∗ₙ h - g ∗ₙ h := by - simp only [sub_eq_add_neg, add_nconv, neg_nconv] +lemma sub_cconv (f g h : G → R) : (f - g) ∗ₙ h = f ∗ₙ h - g ∗ₙ h := by + simp only [sub_eq_add_neg, add_cconv, neg_cconv] variable [StarRing R] @@ -366,8 +366,8 @@ end Field section Semifield variable [Semifield R] [CharZero R] -@[simp] lemma indicate_univ_nconv_indicate_univ : 𝟭_[R] (univ : Finset G) ∗ₙ 𝟭 univ = 𝟭 univ := by - ext; simp [indicate_apply, nconv_eq_expect_add, card_univ, *] +@[simp] lemma indicate_univ_cconv_indicate_univ : 𝟭_[R] (univ : Finset G) ∗ₙ 𝟭 univ = 𝟭 univ := by + ext; simp [indicate_apply, cconv_eq_expect_add, card_univ, *] variable [StarRing R] @@ -379,8 +379,8 @@ end Semifield section Field variable [Field R] [CharZero R] -@[simp] lemma balance_nconv (f g : G → R) : balance (f ∗ₙ g) = balance f ∗ₙ balance g := by - simp [balance, nconv_sub, sub_nconv, expect_nconv, expect_sub_distrib] +@[simp] lemma balance_cconv (f g : G → R) : balance (f ∗ₙ g) = balance f ∗ₙ balance g := by + simp [balance, cconv_sub, sub_cconv, expect_cconv, expect_sub_distrib] variable [StarRing R] @@ -393,13 +393,13 @@ namespace RCLike variable {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G) @[simp, norm_cast] -lemma coe_nconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_nconv (algebraMap ℝ 𝕜) _ _ _ +lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_cconv (algebraMap ℝ 𝕜) _ _ _ @[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by simp [cdconv_apply, coe_expect] @[simp] -lemma coe_comp_nconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_nconv _ _ +lemma coe_comp_cconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cconv _ _ @[simp] lemma coe_comp_cdconv : ofReal ∘ (f ○ₙ g) = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cdconv _ _ @@ -410,13 +410,13 @@ namespace Complex variable (f g : G → ℝ) (a : G) @[simp, norm_cast] -lemma coe_nconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℂ) a := RCLike.coe_nconv _ _ _ +lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℂ) a := RCLike.coe_cconv _ _ _ @[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → ℂ) a := RCLike.coe_cdconv _ _ _ @[simp] -lemma coe_comp_nconv : ofReal' ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℂ) := funext $ coe_nconv _ _ +lemma coe_comp_cconv : ofReal' ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℂ) := funext $ coe_cconv _ _ @[simp] lemma coe_comp_cdconv : ofReal' ∘ (f ○ₙ g) = ((↑) ∘ f ○ₙ (↑) ∘ g : G → ℂ) := funext $ coe_cdconv _ _ @@ -427,13 +427,13 @@ namespace NNReal variable (f g : G → ℝ≥0) (a : G) @[simp, norm_cast] -lemma coe_nconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℝ) a := map_nconv NNReal.toRealHom _ _ _ +lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → ℝ) a := map_cconv NNReal.toRealHom _ _ _ @[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → ℝ) a := by simp [cdconv_apply, coe_expect] @[simp] -lemma coe_comp_nconv : ((↑) : _ → ℝ) ∘ (f ∗ₙ g) = (↑) ∘ f ∗ₙ (↑) ∘ g := funext $ coe_nconv _ _ +lemma coe_comp_cconv : ((↑) : _ → ℝ) ∘ (f ∗ₙ g) = (↑) ∘ f ∗ₙ (↑) ∘ g := funext $ coe_cconv _ _ @[simp] lemma coe_comp_cdconv : ((↑) : _ → ℝ) ∘ (f ○ₙ g) = (↑) ∘ f ○ₙ (↑) ∘ g := funext $ coe_cdconv _ _ @@ -446,84 +446,84 @@ section Semifield variable [Semifield R] [CharZero R] {f g : G → R} {n : ℕ} /-- Iterated convolution. -/ -def iterNConv (f : G → R) : ℕ → G → R +def iterCconv (f : G → R) : ℕ → G → R | 0 => trivNChar - | n + 1 => iterNConv f n ∗ₙ f + | n + 1 => iterCconv f n ∗ₙ f -infixl:78 " ∗^ₙ " => iterNConv +infixl:78 " ∗^ₙ " => iterCconv -@[simp] lemma iterNConv_zero (f : G → R) : f ∗^ₙ 0 = trivNChar := rfl -@[simp] lemma iterNConv_one (f : G → R) : f ∗^ₙ 1 = f := trivNChar_nconv _ +@[simp] lemma iterCconv_zero (f : G → R) : f ∗^ₙ 0 = trivNChar := rfl +@[simp] lemma iterCconv_one (f : G → R) : f ∗^ₙ 1 = f := trivNChar_cconv _ -lemma iterNConv_succ (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗^ₙ n ∗ₙ f := rfl -lemma iterNConv_succ' (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗ₙ f ∗^ₙ n := nconv_comm _ _ +lemma iterCconv_succ (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗^ₙ n ∗ₙ f := rfl +lemma iterCconv_succ' (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗ₙ f ∗^ₙ n := cconv_comm _ _ -lemma iterNConv_add (f : G → R) (m : ℕ) : ∀ n, f ∗^ₙ (m + n) = f ∗^ₙ m ∗ₙ f ∗^ₙ n +lemma iterCconv_add (f : G → R) (m : ℕ) : ∀ n, f ∗^ₙ (m + n) = f ∗^ₙ m ∗ₙ f ∗^ₙ n | 0 => by simp - | n + 1 => by simp [← add_assoc, iterNConv_succ', iterNConv_add, nconv_left_comm] + | n + 1 => by simp [← add_assoc, iterCconv_succ', iterCconv_add, cconv_left_comm] -lemma iterNConv_mul (f : G → R) (m : ℕ) : ∀ n, f ∗^ₙ (m * n) = f ∗^ₙ m ∗^ₙ n +lemma iterCconv_mul (f : G → R) (m : ℕ) : ∀ n, f ∗^ₙ (m * n) = f ∗^ₙ m ∗^ₙ n | 0 => rfl - | n + 1 => by simp [mul_add_one, iterNConv_succ, iterNConv_add, iterNConv_mul] + | n + 1 => by simp [mul_add_one, iterCconv_succ, iterCconv_add, iterCconv_mul] -lemma iterNConv_mul' (f : G → R) (m n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ n ∗^ₙ m := by - rw [mul_comm, iterNConv_mul] +lemma iterCconv_mul' (f : G → R) (m n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ n ∗^ₙ m := by + rw [mul_comm, iterCconv_mul] -lemma iterNConv_nconv_distrib (f g : G → R) : ∀ n, (f ∗ₙ g) ∗^ₙ n = f ∗^ₙ n ∗ₙ g ∗^ₙ n - | 0 => (nconv_trivNChar _).symm - | n + 1 => by simp_rw [iterNConv_succ, iterNConv_nconv_distrib, nconv_nconv_nconv_comm] +lemma iterCconv_cconv_distrib (f g : G → R) : ∀ n, (f ∗ₙ g) ∗^ₙ n = f ∗^ₙ n ∗ₙ g ∗^ₙ n + | 0 => (cconv_trivNChar _).symm + | n + 1 => by simp_rw [iterCconv_succ, iterCconv_cconv_distrib, cconv_cconv_cconv_comm] -@[simp] lemma zero_iterNConv : ∀ {n}, n ≠ 0 → (0 : G → R) ∗^ₙ n = 0 +@[simp] lemma zero_iterCconv : ∀ {n}, n ≠ 0 → (0 : G → R) ∗^ₙ n = 0 | 0, hn => by cases hn rfl - | n + 1, _ => nconv_zero _ + | n + 1, _ => cconv_zero _ -@[simp] lemma smul_iterNConv [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] +@[simp] lemma smul_iterCconv [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f : G → R) : ∀ n, (c • f) ∗^ₙ n = c ^ n • f ∗^ₙ n | 0 => by simp - | n + 1 => by simp_rw [iterNConv_succ, smul_iterNConv _ _ n, pow_succ, mul_smul_nconv_comm] + | n + 1 => by simp_rw [iterCconv_succ, smul_iterCconv _ _ n, pow_succ, mul_smul_cconv_comm] -lemma comp_iterNConv [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) : +lemma comp_iterCconv [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) : ∀ n, m ∘ (f ∗^ₙ n) = m ∘ f ∗^ₙ n | 0 => by ext; simp; split_ifs <;> simp - | n + 1 => by simp [iterNConv_succ, comp_nconv, comp_iterNConv] + | n + 1 => by simp [iterCconv_succ, comp_cconv, comp_iterCconv] -lemma expect_iterNConv (f : G → R) : ∀ n, 𝔼 a, (f ∗^ₙ n) a = (𝔼 a, f a) ^ n +lemma expect_iterCconv (f : G → R) : ∀ n, 𝔼 a, (f ∗^ₙ n) a = (𝔼 a, f a) ^ n | 0 => by simp [filter_eq', card_univ, NNRat.smul_def] - | n + 1 => by simp only [iterNConv_succ, expect_nconv, expect_iterNConv, pow_succ] + | n + 1 => by simp only [iterCconv_succ, expect_cconv, expect_iterCconv, pow_succ] -@[simp] lemma iterNConv_trivNChar : ∀ n, (trivNChar : G → R) ∗^ₙ n = trivNChar +@[simp] lemma iterCconv_trivNChar : ∀ n, (trivNChar : G → R) ∗^ₙ n = trivNChar | 0 => rfl - | _n + 1 => (nconv_trivNChar _).trans $ iterNConv_trivNChar _ + | _n + 1 => (cconv_trivNChar _).trans $ iterCconv_trivNChar _ -lemma support_iterNConv_subset (f : G → R) : ∀ n, support (f ∗^ₙ n) ⊆ n • support f +lemma support_iterCconv_subset (f : G → R) : ∀ n, support (f ∗^ₙ n) ⊆ n • support f | 0 => by - simp only [iterNConv_zero, zero_smul, support_subset_iff, Ne, ite_eq_right_iff, exists_prop, + simp only [iterCconv_zero, zero_smul, support_subset_iff, Ne, ite_eq_right_iff, exists_prop, not_forall, Set.mem_zero, and_imp, forall_eq, eq_self_iff_true, imp_true_iff, trivNChar_apply] | n + 1 => - (support_nconv_subset _ _).trans $ Set.add_subset_add_right $ support_iterNConv_subset _ _ + (support_cconv_subset _ _).trans $ Set.add_subset_add_right $ support_iterCconv_subset _ _ -lemma map_iterNConv [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) (a : G) - (n : ℕ) : m ((f ∗^ₙ n) a) = (m ∘ f ∗^ₙ n) a := congr_fun (comp_iterNConv m _ _) _ +lemma map_iterCconv [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) (a : G) + (n : ℕ) : m ((f ∗^ₙ n) a) = (m ∘ f ∗^ₙ n) a := congr_fun (comp_iterCconv m _ _) _ variable [StarRing R] -@[simp] lemma conj_iterNConv (f : G → R) : ∀ n, conj (f ∗^ₙ n) = conj f ∗^ₙ n +@[simp] lemma conj_iterCconv (f : G → R) : ∀ n, conj (f ∗^ₙ n) = conj f ∗^ₙ n | 0 => by simp - | n + 1 => by simp [iterNConv_succ, conj_iterNConv] + | n + 1 => by simp [iterCconv_succ, conj_iterCconv] -@[simp] lemma conjneg_iterNConv (f : G → R) : ∀ n, conjneg (f ∗^ₙ n) = conjneg f ∗^ₙ n +@[simp] lemma conjneg_iterCconv (f : G → R) : ∀ n, conjneg (f ∗^ₙ n) = conjneg f ∗^ₙ n | 0 => by simp - | n + 1 => by simp [iterNConv_succ, conjneg_iterNConv] + | n + 1 => by simp [iterCconv_succ, conjneg_iterCconv] -lemma iterNConv_cdconv_distrib (f g : G → R) : ∀ n, (f ○ₙ g) ∗^ₙ n = f ∗^ₙ n ○ₙ g ∗^ₙ n +lemma iterCconv_cdconv_distrib (f g : G → R) : ∀ n, (f ○ₙ g) ∗^ₙ n = f ∗^ₙ n ○ₙ g ∗^ₙ n | 0 => (cdconv_trivNChar _).symm - | n + 1 => by simp_rw [iterNConv_succ, iterNConv_cdconv_distrib, nconv_cdconv_nconv_comm] + | n + 1 => by simp_rw [iterCconv_succ, iterCconv_cdconv_distrib, cconv_cdconv_cconv_comm] --- lemma indicate_iterNConv_apply (s : Finset G) (n : ℕ) (a : G) : +-- lemma indicate_iterCconv_apply (s : Finset G) (n : ℕ) (a : G) : -- (𝟭_[ℝ] s ∗^ₙ n) a = ((piFinset fun _i ↦ s).filter fun x : Fin n → G ↦ ∑ i, x i = a).card := by -- induction' n with n ih generalizing a -- · simp [apply_ite card, eq_comm] --- simp_rw [iterNConv_succ, nconv_eq_expect_sub', ih, indicate_apply, boole_mul, expect_ite, filter_univ_mem, +-- simp_rw [iterCconv_succ, cconv_eq_expect_sub', ih, indicate_apply, boole_mul, expect_ite, filter_univ_mem, -- expect_const_zero, add_zero, ← Nat.cast_expect, ← Finset.card_sigma, Nat.cast_inj] -- refine Finset.card_bij (fun f _ ↦ Fin.cons f.1 f.2) _ _ _ -- · simp only [Fin.expect_cons, eq_sub_iff_add_eq', mem_sigma, mem_filter, mem_piFinset, and_imp] @@ -543,10 +543,10 @@ end Semifield section Field variable [Field R] [CharZero R] -@[simp] lemma balance_iterNConv (f : G → R) : ∀ {n}, n ≠ 0 → balance (f ∗^ₙ n) = balance f ∗^ₙ n +@[simp] lemma balance_iterCconv (f : G → R) : ∀ {n}, n ≠ 0 → balance (f ∗^ₙ n) = balance f ∗^ₙ n | 0, h => by cases h rfl | 1, _ => by simp - | n + 2, _ => by simp [iterNConv_succ _ (n + 1), balance_iterNConv _ n.succ_ne_zero] + | n + 2, _ => by simp [iterCconv_succ _ (n + 1), balance_iterCconv _ n.succ_ne_zero] end Field @@ -554,7 +554,7 @@ namespace NNReal variable {f : G → ℝ≥0} @[simp, norm_cast] -lemma coe_iterNConv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ₙ n) a) : ℝ) = ((↑) ∘ f ∗^ₙ n) a := - map_iterNConv NNReal.toRealHom _ _ _ +lemma coe_iterCconv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ₙ n) a) : ℝ) = ((↑) ∘ f ∗^ₙ n) a := + map_iterCconv NNReal.toRealHom _ _ _ end NNReal diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean index 04e9172caf..4d643e2186 100644 --- a/LeanAPAP/Prereqs/Expect/Basic.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean index 4579521501..cc08db5ed6 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/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) diff --git a/LeanAPAP/Prereqs/FourierTransform/Convolution.lean b/LeanAPAP/Prereqs/FourierTransform/Convolution.lean new file mode 100644 index 0000000000..f084d8140e --- /dev/null +++ b/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) diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean index be46d3e60d..57feb0cd3c 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean +++ b/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) diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean index 78d4a0d739..cb4c78944e 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean +++ b/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 -/ diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index b5465fe790..aaa11efccb 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -10,6 +10,8 @@ import LeanAPAP.Prereqs.NNLpNorm open Finset Function Real open scoped BigOperators ComplexConjugate ENNReal NNReal NNRat +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + variable {α 𝕜 R E : Type*} [MeasurableSpace α] namespace MeasureTheory @@ -210,6 +212,20 @@ lemma dLinftyNorm_eq_iSup_norm (f : α → E) : ‖f‖_[∞] = ⨆ i, ‖f i‖ lemma dLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖_[p] ≤ ‖g‖_[p] := nnLpNorm_mono_real .of_discrete h +lemma dLpNorm_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 [← dLpNorm_pow_eq_sum_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, sum_comm (s := univ)] + end MeasureTheory namespace Mathlib.Meta.Positivity diff --git a/blueprint/src/chapter/ff.tex b/blueprint/src/chapter/ff.tex index 88ff50b2fc..09113dfe0a 100644 --- a/blueprint/src/chapter/ff.tex +++ b/blueprint/src/chapter/ff.tex @@ -61,7 +61,7 @@ \chapter{Finite field model} \begin{lemma} \label{ast_le_circ} -\lean{Lpnorm_conv_le_Lpnorm_dconv} +\lean{cLpNorm_cconv_le_cLpNorm_cdconv} \leanok For any function $f:G\to \mathbb{C}$ and integer $k\geq 1$ \[\| f\ast f\|_{2k}\leq \| f\circ f\|_{2k}.\]