diss_energy

LeanAPAP/Prereqs/Chang.lean

@@ -15,7 +15,7 @@ import LeanAPAP.Prereqs.Misc
 # Chang's lemma
 -/
 
-open Finset Fintype Real
+open Finset Fintype Function Real
 open scoped BigOperators ComplexConjugate ComplexOrder NNReal
 
 variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ}
@@ -108,31 +108,43 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0)
     div_le_iff hG, energy_nsmul, -nsmul_eq_mul, ←nsmul_eq_mul'] using
     general_hoelder hη 1 (fun (_ : G) _ ↦ le_rfl) hΔ hm
 
-noncomputable def changConst : ℝ := 8 * Real.exp 1
+noncomputable def changConst : ℝ := 32 * exp 1
 
 lemma one_lt_changConst : 1 < changConst := one_lt_mul (by norm_num) $ one_lt_exp_iff.2 one_pos
 
+lemma changConst_pos : 0 < changConst := zero_lt_one.trans one_lt_changConst
+
+namespace Mathlib.Meta.Positivity
+open Lean.Meta Qq
+
+/-- Extension for the `positivity` tactic: `changConst` is positive. -/
+@[positivity changConst] def evalChangConst : PositivityExt where eval _ _ _ := do
+  return .positive (q(changConst_pos) : Lean.Expr)
+
+example : 0 < changConst := by positivity
+
+end Mathlib.Meta.Positivity
+
 lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G}
     (hs : AddDissociated (s : Set G)) (n : ℕ) :
     boringEnergy n s ≤ changConst ^ n * n ^ n * s.card ^ n := by
-  obtain rfl | hn := n.eq_zero_or_pos
+  obtain rfl | hn := eq_or_ne n 0
   · simp
-  have := rudin_ineq (le_mul_of_one_le_right zero_le_two $ Nat.one_le_iff_ne_zero.2 hn.ne')
-    (cft (𝟭_[ℂ] s)) ?_
-  sorry
-  sorry
-  -- · replace this := pow_le_pow_left ?_ this (2 * n)
-  --   rw [lpNorm_cft_indicate_pow] at this
-  --   convert this using 0
-  --   simp_rw [mul_pow, pow_mul]
-  --   rw [← exp_nsmul, sq_sqrt, sq_sqrt]
-  --   simp_rw [←mul_pow]
-  --   simp [changConst]
-  --   ring_nf
-  --   all_goals sorry -- positivity
-  -- rwa [dft_dft, ←nsmul_eq_mul, support_smul', support_comp_eq_preimage, support_indicate,
-  --   Set.preimage_comp, Set.neg_preimage, addDissociated_neg, AddEquiv.addDissociated_preimage]
-  -- sorry -- positivity
+  calc
+    _ = ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) := by rw [nlpNorm_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)
+          (dft (𝟭_[ℂ] s)) ?_
+        rwa [cft_dft, support_comp_eq_preimage, support_indicate, Set.preimage_comp,
+          Set.neg_preimage, addDissociated_neg, AddEquiv.addDissociated_preimage]
+    _ = _ := by
+        simp_rw [mul_pow, pow_mul, nl2Norm_dft_indicate]
+        rw [← exp_nsmul, sq_sqrt, sq_sqrt]
+        simp_rw [←mul_pow]
+        simp [changConst]
+        ring_nf
+        all_goals positivity
 
 /-- **Chang's lemma**. -/
 lemma chang (hf : f ≠ 0) (hη : 0 < η) :
@@ -157,7 +169,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
     _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α f * exp β) := by
         rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
-  refine' le_mul_of_one_le_right (by sorry) _ -- positivity
+  refine' le_mul_of_one_le_right (by positivity) _
   rw [←inv_pos_le_iff_one_le_mul']
   exact inv_le_exp_curlog.trans $ exp_monotone $ Nat.le_ceil _
-  all_goals sorry -- positivity
+  all_goals positivity

LeanAPAP/Prereqs/Discrete/Convolution/Basic.lean

@@ -86,6 +86,19 @@ lemma conv_comm (f g : α → β) : f ∗ g = g ∗ f :=
 @[simp] lemma conj_conv (f g : α → β) : conj (f ∗ g) = conj f ∗ conj g :=
   funext fun a ↦ by simp only [Pi.conj_apply, conv_apply, map_sum, map_mul]
 
+@[simp] lemma conj_dconv (f g : α → β) : conj (f ○ g) = conj f ○ conj g := by
+  simp_rw [← conv_conjneg, conj_conv, conjneg_conj]
+
+@[simp] lemma conj_trivChar : conj (trivChar : α → β) = trivChar := by ext; simp
+
+lemma IsSelfAdjoint.conv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ g) :=
+  (conj_conv _ _).trans $ congr_arg₂ _ hf hg
+
+lemma IsSelfAdjoint.dconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ g) :=
+  (conj_dconv _ _).trans $ congr_arg₂ _ hf hg
+
+@[simp] lemma isSelfAdjoint_trivChar : IsSelfAdjoint (trivChar : α → β) := conj_trivChar
+
 @[simp]lemma conjneg_conv (f g : α → β) : conjneg (f ∗ g) = conjneg f ∗ conjneg g := by
   funext a
   simp only [conv_apply, conjneg_apply, map_sum, map_mul]
@@ -348,7 +361,7 @@ lemma coe_dconv : (↑((f ○ g) a) : 𝕜) = ((↑) ∘ f ○ (↑) ∘ g) a :=
 end IsROrC
 
 namespace Complex
-variable (f g : α → ℝ) (a : α)
+variable (f g : α → ℝ) (n : ℕ) (a : α)
 
 @[simp, norm_cast]
 lemma coe_conv : (↑((f ∗ g) a) : ℂ) = ((↑) ∘ f ∗ (↑) ∘ g) a := IsROrC.coe_conv _ _ _
@@ -408,6 +421,9 @@ lemma iterConv_mul' (f : α → β) (m n : ℕ) : f ∗^ (m * n) = f ∗^ n ∗^
   | 0 => by ext; simp
   | n + 1 => by simp [iterConv_succ, conj_iterConv]
 
+lemma IsSelfAdjoint.iterConv (hf : IsSelfAdjoint f) (n : ℕ) : IsSelfAdjoint (f ∗^ n) :=
+  (conj_iterConv _ _).trans $ congr_arg (· ∗^ n) hf
+
 @[simp]
 lemma conjneg_iterConv (f : α → β) : ∀ n, conjneg (f ∗^ n) = conjneg f ∗^ n
   | 0 => by ext; simp
@@ -485,10 +501,17 @@ variable [Field β] [StarRing β] [CharZero β]
 end Field
 
 namespace NNReal
-variable {f : α → ℝ≥0}
 
 @[simp, norm_cast]
 lemma coe_iterConv (f : α → ℝ≥0) (n : ℕ) (a : α) : (↑((f ∗^ n) a) : ℝ) = ((↑) ∘ f ∗^ n) a :=
   map_iterConv NNReal.toRealHom _ _ _
 
 end NNReal
+
+namespace Complex
+
+@[simp, norm_cast]
+lemma coe_iterConv (f : α → ℝ) (n : ℕ) (a : α) : (↑((f ∗^ n) a) : ℂ) = ((↑) ∘ f ∗^ n) a :=
+  map_iterConv ofReal _ _ _
+
+end Complex

LeanAPAP/Prereqs/Discrete/Convolution/Compact.lean

@@ -80,9 +80,20 @@ lemma nconv_comm (f g : α → β) : f ∗ₙ g = g ∗ₙ f :=
 @[simp] lemma conj_nconv (f g : α → β) : 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_ndconv (f g : α → β) : conj (f ○ₙ g) = conj f ○ₙ conj g := by
+  simp_rw [← nconv_conjneg, conj_nconv, conjneg_conj]
+
 @[simp] lemma conj_trivNChar : conj (trivNChar : α → β) = trivNChar := by
   ext; simp; split_ifs <;> simp
 
+lemma IsSelfAdjoint.nconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ₙ g) :=
+  (conj_nconv _ _).trans $ congr_arg₂ _ hf hg
+
+lemma IsSelfAdjoint.ndconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ₙ g) :=
+  (conj_ndconv _ _).trans $ congr_arg₂ _ hf hg
+
+@[simp] lemma isSelfAdjoint_trivNChar : IsSelfAdjoint (trivChar : α → β) := conj_trivChar
+
 @[simp]lemma conjneg_nconv (f g : α → β) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g := by
   funext a
   simp only [nconv_apply, conjneg_apply, map_expect, map_mul]

LeanAPAP/Prereqs/Discrete/DFT/Compact.lean

@@ -62,12 +62,20 @@ lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a :=
 
 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, l2Inner_eq_sum, map_neg_eq_inv,
-    AddChar.inv_apply_eq_conj, doubleDualEmb_apply, ← Fintype.card_mul_expect, AddChar.card_eq]
+    AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
+
+lemma cft_dft_doubleDualEmb (f : α → ℂ) (a : α) : cft (dft f) (doubleDualEmb a) = f (-a) := by
+  simp only [← dft_inversion f (-a), mul_comm (conj _), cft_apply, nl2Inner_eq_expect,
+    map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
 
 lemma dft_cft (f : α → ℂ) : dft (cft f) = f ∘ doubleDualEquiv.symm ∘ Neg.neg :=
   funext fun a ↦ by simp_rw [Function.comp_apply, map_neg, ←dft_cft_doubleDualEmb,
       doubleDualEmb_doubleDualEquiv_symm_apply]
 
+lemma cft_dft (f : α → ℂ) : cft (dft f) = f ∘ doubleDualEquiv.symm ∘ Neg.neg :=
+  funext fun a ↦ by simp_rw [Function.comp_apply, map_neg, ←cft_dft_doubleDualEmb,
+      doubleDualEmb_doubleDualEquiv_symm_apply]
+
 lemma cft_injective : Injective (cft : (α → ℂ) → AddChar α ℂ → ℂ) := fun f g h ↦
   funext fun a ↦ (cft_inversion _ _).symm.trans $ by rw [h, cft_inversion]
 

LeanAPAP/Prereqs/Energy.lean

@@ -7,27 +7,27 @@ noncomputable section
 open Finset Fintype Function Real
 open scoped BigOperators Nat
 
-variable {G : Type*} [AddCommGroup G] [Fintype G] {A : Finset G}
+variable {G : Type*} [AddCommGroup G] [Fintype G] {s : Finset G}
 
-def energy (n : ℕ) (A : Finset G) (ν : G → ℂ) : ℝ :=
-  ∑ γ in piFinset fun _ : Fin n ↦ A, ∑ δ in piFinset fun _ : Fin n ↦ A, ‖ν (∑ i, γ i - ∑ i, δ i)‖
+def energy (n : ℕ) (s : Finset G) (ν : G → ℂ) : ℝ :=
+  ∑ γ in piFinset fun _ : Fin n ↦ s, ∑ δ in piFinset fun _ : Fin n ↦ s, ‖ν (∑ i, γ i - ∑ i, δ i)‖
 
 @[simp]
-lemma energy_nonneg (n : ℕ) (A : Finset G) (ν : G → ℂ) : 0 ≤ energy n A ν := by
+lemma energy_nonneg (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s ν := by
   unfold energy; positivity
 
-lemma energy_nsmul (m n : ℕ) (A : Finset G) (ν : G → ℂ) :
-    energy n A (m • ν) = m • energy n A ν := by
+lemma energy_nsmul (m n : ℕ) (s : Finset G) (ν : G → ℂ) :
+    energy n s (m • ν) = m • energy n s ν := by
   simp only [energy, nsmul_eq_mul, mul_sum, @Pi.coe_nat G (fun _ ↦ ℂ) _ m, Pi.mul_apply, norm_mul,
     Complex.norm_nat]
 
-@[simp] lemma energy_zero (A : Finset G) (ν : G → ℂ) : energy 0 A ν = ‖ν 0‖ := by simp [energy]
+@[simp] lemma energy_zero (s : Finset G) (ν : G → ℂ) : energy 0 s ν = ‖ν 0‖ := by simp [energy]
 
 variable [DecidableEq G]
 
-def boringEnergy (n : ℕ) (A : Finset G) : ℝ := energy n A trivChar
+def boringEnergy (n : ℕ) (s : Finset G) : ℝ := energy n s trivChar
 
-lemma boringEnergy_eq (n : ℕ) (A : Finset G) : boringEnergy n A = ∑ x, (𝟭 A ∗^ n) x ^ 2 := by
+lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭 s ∗^ n) x ^ 2 := by
   classical
   simp only [boringEnergy, energy, apply_ite norm, trivChar_apply, norm_one, norm_zero, sum_boole,
     sub_eq_zero]
@@ -37,36 +37,29 @@ lemma boringEnergy_eq (n : ℕ) (A : Finset G) : boringEnergy n A = ∑ x, (𝟭
   refine' sum_congr rfl fun f hf ↦ _
   simp_rw [(mem_filter.1 hf).2, eq_comm]
 
-@[simp] lemma boringEnergy_zero (A : Finset G) : boringEnergy 0 A = 1 := by simp [boringEnergy]
-@[simp] lemma boringEnergy_one (A : Finset G) : boringEnergy 1 A = A.card := by
+@[simp] lemma boringEnergy_zero (s : Finset G) : boringEnergy 0 s = 1 := by simp [boringEnergy]
+@[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = s.card := by
   simp [boringEnergy_eq, indicate_apply]
 
-lemma lpNorm_cft_indicate_pow (n : ℕ) (A : Finset G) :
-    ‖cft (𝟭 A)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n A := sorry
+lemma nlpNorm_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
+  refine Complex.ofReal_injective ?_
+  calc
+    _ = ⟪dft (𝟭 s ∗^ n), dft (𝟭 s ∗^ n)⟫ₙ_[ℂ] := ?_
+    _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := nl2Inner_dft _ _
+    _ = _ := ?_
+  · rw [nlpNorm_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
+  · simp only [l2Inner_eq_sum, boringEnergy_eq, Complex.ofReal_mul, Complex.ofReal_nat_cast,
+      Complex.ofReal_sum, Complex.ofReal_pow, mul_eq_mul_left_iff, Nat.cast_eq_zero, card_ne_zero,
+      or_false, sq, (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.coe_iterConv,
+      Complex.ofReal_comp_indicate]
 
-
-lemma lpNorm_dft_indicate_pow (n : ℕ) (A : Finset G) :
-    ‖dft (𝟭 A)‖_[↑(2 * n)] ^ (2 * n) = card G * boringEnergy n A := by
-  sorry
-  -- obtain rfl | hn := n.eq_zero_or_pos
-  -- · simp
-  -- refine Complex.ofReal_injective ?_
-  -- calc
-  --   ↑(‖dft (𝟭 A)‖_[↑(2 * n)] ^ (2 * n))
-  --     = ⟪dft (𝟭 A ∗^ n), dft (𝟭 A ∗^ n)⟫_[ℂ] := ?_
-  --   _ = card G * ⟪𝟭 A ∗^ n, 𝟭 A ∗^ n⟫_[ℂ] := nl2Inner_dft _ _
-  --   _ = ↑(card G * boringEnergy n A) := ?_
-  -- · rw [lpNorm_pow_eq_sum]
-  --   simp_rw [pow_mul', ←norm_pow _ n, Complex.ofReal_sum, Complex.ofReal_pow, ←Complex.conj_mul',
-  --     l2Inner_eq_sum, dft_iterConv_apply]
-  --   positivity
-  -- · simp only [l2Inner_eq_sum, boringEnergy_eq, Complex.ofReal_mul, Complex.ofReal_nat_cast,
-  --     Complex.ofReal_sum, Complex.ofReal_pow, mul_eq_mul_left_iff, Nat.cast_eq_zero, card_ne_zero,
-  --     or_false, sq]
-  --   congr with a
-  --   simp
-  --   sorry
-  --   sorry
-
-lemma l2Norm_dft_indicate (A : Finset G) : ‖dft (𝟭 A)‖_[2] = sqrt A.card := by
-  sorry -- simpa using lpNorm_dft_indicate_pow 1 A
+lemma nl2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by
+  rw [eq_comm, sqrt_eq_iff_sq_eq]
+  simpa using nlpNorm_dft_indicate_pow 1 s
+  all_goals positivity

LeanAPAP/Prereqs/Indicator.lean

@@ -1,3 +1,4 @@
+import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Finset.Pointwise
 import Mathlib.Data.Real.NNReal
 import LeanAPAP.Prereqs.Expect.Basic
@@ -96,14 +97,24 @@ end Semifield
 namespace NNReal
 open scoped NNReal
 
-@[simp, norm_cast] lemma coe_indicate' (s : Finset α) (x : α) : ↑(𝟭_[ℝ≥0] s x) = 𝟭_[ℝ] s x :=
+@[simp, norm_cast] lemma coe_indicate (s : Finset α) (x : α) : ↑(𝟭_[ℝ≥0] s x) = 𝟭_[ℝ] s x :=
   map_indicate NNReal.toRealHom _ _
 
 @[simp] lemma coe_comp_indicate (s : Finset α) : (↑) ∘ 𝟭_[ℝ≥0] s = 𝟭_[ℝ] s := by
-  ext; exact coe_indicate' _ _
+  ext; exact coe_indicate _ _
 
 end NNReal
 
+namespace Complex
+
+@[simp, norm_cast] lemma ofReal_indicate (s : Finset α) (x : α) : ↑(𝟭_[ℝ] s x) = 𝟭_[ℂ] s x :=
+  map_indicate ofReal _ _
+
+@[simp] lemma ofReal_comp_indicate (s : Finset α) : (↑) ∘ 𝟭_[ℝ] s = 𝟭_[ℂ] s := by
+  ext; exact ofReal_indicate _ _
+
+end Complex
+
 section OrderedSemiring
 variable [OrderedSemiring β] {s : Finset α}
 

LeanAPAP/Prereqs/Translate.lean

@@ -77,6 +77,8 @@ lemma conjneg_injective : Injective (conjneg : (α → β) → α → β) :=
 @[simp] lemma conjneg_inj : conjneg f = conjneg g ↔ f = g := conjneg_injective.eq_iff
 lemma conjneg_ne_conjneg : conjneg f ≠ conjneg g ↔ f ≠ g := conjneg_injective.ne_iff
 
+@[simp] lemma conjneg_conj (f : α → β) : conjneg (conj f) = conj (conjneg f) := rfl
+
 @[simp] lemma conjneg_zero : conjneg (0 : α → β) = 0 := by ext; simp
 @[simp] lemma conjneg_one : conjneg (1 : α → β) = 1 := by ext; simp
 @[simp] lemma conjneg_add (f g : α → β) : conjneg (f + g) = conjneg f + conjneg g := by ext; simp

blueprint/src/chang.tex

@@ -170,17 +170,20 @@ \chapter{Chang's lemma}
 \uses{dissociated, energy}
 \lean{AddDissociated.boringEnergy_le}
 \leanok
-If $A\subseteq G$ is dissociated then $E_{2m}(A) \leq (8e m \abs{A})^m$.
+If $A\subseteq G$ is dissociated then $E_{2m}(A) \leq (32e m \abs{A})^m$.
 \end{lemma}
 \begin{proof}
 \uses{energy_alt, rudin}
-By Lemma~\ref{energy_alt}
-
-\[E_{2m}(A) = \sum_x 1_A^{(m)}(x)^2.\]
-By the definition of dissociativity, $1_A^{(m)}(x)\leq m!$ for all $x\in G$. We are done since
-\[ \sum_x 1_A^{(m)}(x) = \abs{A}^m.\]
-
-TODO(Thomas): This proof is wrong.
+\leanok
+By Lemma~\ref{energy_alt} and Lemma~\ref{rudin}
+\begin{align*}
+  E_{2m}(A)
+  & = \bbE_\gamma \abs{\hat 1_A(\gamma)}^{2m} \\
+  & = \norm{\hat 1_A}_{2m}^{2m} \\
+  & \le (4\sqrt{2em})^{2m} \norm{\hat 1_A}_2^{2m} \\
+  & = (32em)^m \norm{1_A^{(m)}}_2^{2m} \\
+  & = (32em)^m \abs{A}^m
+\end{align*}
 \end{proof}