Progress on rudin_exp_ineq

LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean

@@ -132,16 +132,19 @@ lemma expectWith_congr (f g : ι → α) (p : ι → Prop) [DecidablePred p]
     (h : ∀ x ∈ s, p x → f x = g x) : 𝔼 i ∈ s with p i, f i = 𝔼 i ∈ s with p i, g i :=
   expect_congr _ _ $ by simpa using h
 
+-- TODO: Backport arguments changes to `card_congr` and `prod_bij`
 lemma expect_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
-    (i_inj : ∀ a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ha, b = i a ha) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := by
-  rw [expect, expect, card_congr i hi i_inj, sum_bij i hi h i_inj i_surj]
+    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
+    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := by
+  rw [expect, expect, card_congr i hi (fun _ _ _ _ ↦ i_inj _ _ _ _),
+    sum_bij i hi h (fun _ _ _ _ ↦ i_inj _ _ _ _) (by simpa [eq_comm] using i_surj)]
   simpa [eq_comm] using i_surj
 
+-- TODO: Backport arguments changes to `prod_nbij`
 lemma expect_nbij (i : ι → β) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a))
-    (i_inj : ∀ a₁ a₂, a₁ ∈ s → a₂ ∈ s → i a₁ = i a₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ∈ s, b = i a) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x :=
-  expect_bij (fun a _ ↦ i a) hi h i_inj $ by simpa using i_surj
+    (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) :
+    𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x :=
+  expect_bij (fun a _ ↦ i a) hi h i_inj $ by simpa [Set.SurjOn, Set.subset_def] using i_surj
 
 lemma expect_bij' (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
     (j : ∀ a ∈ t, ι) (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
@@ -257,6 +260,28 @@ end Finset
 
 open Finset
 
+namespace Fintype
+variable {κ : Type*} [Fintype ι] [Fintype κ] [Semifield α]
+
+/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts
+`Function.Bijective`.
+
+See `Function.Bijective.expect_comp` for a version without `h`. -/
+lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → α) (g : κ → α)
+    (h : ∀ x, f x = g (e x)) : 𝔼 i, f i = 𝔼 i, g i :=
+  expect_nbij (fun _ ↦ e _) (fun _ _ ↦ mem_univ _) (fun x _ ↦ h x) (he.injective.injOn _) $ by
+    simpa using he.surjective.surjOn _
+
+/-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
+most arguments.
+
+See `Equiv.expect_comp` for a version without `h`. -/
+lemma expect_equiv (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ x, f x = g (e x)) :
+    𝔼 i, f i = 𝔼 i, g i :=
+  expect_bijective _ e.bijective f g h
+
+end Fintype
+
 namespace IsROrC
 variable [IsROrC α] [Fintype ι] (f : ι → ℝ) (a : ι)
 

LeanAPAP/Mathlib/Algebra/ModEq.lean

@@ -0,0 +1,19 @@
+import Mathlib.Algebra.ModEq
+
+namespace AddCommGroup
+variable {α : Type*}
+
+section AddCommGroupWithOne
+variable [AddCommGroupWithOne α] [CharZero α] {a b : ℤ} {n : ℕ}
+
+@[simp, norm_cast] lemma intCast_modEq_intCast' : a ≡ b [PMOD (n : α)] ↔ a ≡ b [PMOD (n : ℤ)] := by
+  simpa using int_cast_modEq_int_cast (α := α) (z := n)
+
+end AddCommGroupWithOne
+
+variable [DivisionRing α] {a b c p : α}
+
+@[simp] lemma div_modEq_div (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD (p * c)] := by
+  simp [ModEq, ←sub_div, div_eq_iff hc, mul_assoc]
+
+end AddCommGroup

LeanAPAP/Mathlib/Analysis/Complex/Basic.lean

@@ -4,10 +4,22 @@ import LeanAPAP.Mathlib.Data.IsROrC.Basic
 open scoped ComplexConjugate
 
 namespace Complex
+variable {x : ℂ}
 
 lemma norm_I : ‖I‖ = 1 := abs_I
 
 lemma mul_conj' (x : ℂ) : x * conj x = (‖x‖ : ℂ) ^ 2 := IsROrC.mul_conj' _
 lemma conj_mul' (x : ℂ) : conj x * x = (‖x‖ : ℂ) ^ 2 := IsROrC.conj_mul' _
 
+lemma inv_eq_conj (hx : ‖x‖ = 1) : x⁻¹ = conj x := IsROrC.inv_eq_conj hx
+
+--TODO: Do we rather want the map as an explicit definition?
+lemma exists_norm_eq_mul_self (x : ℂ) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x :=
+  IsROrC.exists_norm_eq_mul_self _
+
+lemma exists_norm_mul_eq_self (x : ℂ) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x :=
+  IsROrC.exists_norm_mul_eq_self _
+
+@[simp] lemma conj_div (x y : ℂ) : conj (x / y) = conj x / conj y := IsROrC.conj_div _ _
+
 end Complex

LeanAPAP/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -0,0 +1,14 @@
+import Mathlib.Analysis.Convex.SpecificFunctions.Basic
+
+namespace Real
+
+lemma exp_le_cosh_add_mul_sinh {t : ℝ} (ht : |t| ≤ 1) (x : ℝ) :
+    exp (t * x) ≤ cosh x + t * sinh x := by
+  rw [abs_le] at ht
+  calc
+    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
+    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
+        convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) $ by ring
+    _ = _ := by rw [cosh_eq, sinh_eq]; ring
+
+end Real

LeanAPAP/Mathlib/Data/IsROrC/Basic.lean

@@ -14,6 +14,11 @@ lemma exists_norm_eq_mul_self (x : K) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c *
   · exact ⟨1, by simp⟩
   · exact ⟨‖x‖ / x, by simp [norm_ne_zero_iff.2, hx]⟩
 
+lemma exists_norm_mul_eq_self (x : K) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x := by
+  obtain rfl | hx := eq_or_ne x 0
+  · exact ⟨1, by simp⟩
+  · exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩
+
 lemma mul_conj' (x : K) : x * conj x = (‖x‖ : K) ^ 2 := by rw [mul_conj, normSq_eq_def']; norm_cast
 lemma conj_mul' (x : K) : conj x * x = (‖x‖ : K) ^ 2 := by rw [conj_mul, normSq_eq_def']; norm_cast
 

LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean

@@ -19,7 +19,7 @@ Rename
 open Finset hiding card
 open Fintype (card)
 open Function
-open scoped BigOperators ComplexConjugate DirectSum
+open scoped BigOps ComplexConjugate DirectSum
 
 variable {G H R : Type*}
 
@@ -181,6 +181,7 @@ protected lemma l2inner_self [Fintype G] (ψ : AddChar G R) :
 
 end IsROrC
 
+section CommSemiring
 variable [Fintype G] [CommSemiring R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
 
 lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) else 0 := by
@@ -198,6 +199,25 @@ lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
 lemma sum_ne_zero_iff_eq_zero : ∑ x, ψ x ≠ 0 ↔ ψ = 0 :=
   sum_eq_zero_iff_ne_zero.not_left
 
+end CommSemiring
+
+section Semifield
+variable [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
+
+lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 := by
+  split_ifs with h
+  · simp [h, card_univ, univ_nonempty]
+  obtain ⟨x, hx⟩ := ne_one_iff.1 h
+  refine' eq_zero_of_mul_eq_self_left hx _
+  rw [Finset.mul_expect]
+  exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_mul _ _ _).symm
+
+lemma expect_eq_zero_iff_ne_zero : 𝔼 x, ψ x = 0 ↔ ψ ≠ 0 := by
+  rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]
+
+lemma expect_ne_zero_iff_eq_zero : 𝔼 x, ψ x ≠ 0 ↔ ψ = 0 := expect_eq_zero_iff_ne_zero.not_left
+
+end Semifield
 end AddGroup
 
 section AddCommGroup

LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Duality.lean

@@ -1,4 +1,5 @@
 import LeanAPAP.Mathlib.Algebra.Group.TypeTags
+import LeanAPAP.Mathlib.Algebra.ModEq
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Data.ZMod.Basic
 import LeanAPAP.Mathlib.GroupTheory.FiniteAbelian
@@ -14,29 +15,11 @@ We first prove it for `ZMod n` and then extend to all finite abelian groups usin
 Structure Theorem.
 -/
 
-namespace AddCommGroup
-variable {α : Type*}
-
-section AddCommGroupWithOne
-variable [AddCommGroupWithOne α] [CharZero α] {a b : ℤ} {n : ℕ}
-
-@[simp, norm_cast] lemma intCast_modEq_intCast' : a ≡ b [PMOD (n : α)] ↔ a ≡ b [PMOD (n : ℤ)] := by
-  simpa using int_cast_modEq_int_cast (α := α) (z := n)
-
-end AddCommGroupWithOne
-
-variable [DivisionRing α] {a b c p : α}
-
-@[simp] lemma div_modEq_div (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD (p * c)] := by
-  simp [ModEq, ←sub_div, div_eq_iff hc, mul_assoc]
-
-end AddCommGroup
-
 noncomputable section
 
 open circle Circle Finset Function Multiplicative
 open Fintype (card)
-open scoped BigOperators DirectSum
+open scoped BigOps DirectSum
 
 variable {α : Type*} [AddCommGroup α] {n : ℕ} {a b : α}
 
@@ -231,6 +214,10 @@ lemma sum_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
     ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then (Fintype.card α : ℂ) else 0 := by
   simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)
 
+lemma expect_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
+    𝔼 ψ : AddChar α ℂ, ψ a = if a = 0 then 1 else 0 := by
+  simpa using expect_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)
+
 lemma sum_apply_eq_zero_iff_ne_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
   classical
   cases nonempty_fintype α
@@ -240,4 +227,12 @@ lemma sum_apply_eq_zero_iff_ne_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a
 lemma sum_apply_ne_zero_iff_eq_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
   sum_apply_eq_zero_iff_ne_zero.not_left
 
+lemma expect_apply_eq_zero_iff_ne_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
+  classical
+  cases nonempty_fintype α
+  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]
+
+lemma expect_apply_ne_zero_iff_eq_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
+  expect_apply_eq_zero_iff_ne_zero.not_left
+
 end AddChar

LeanAPAP/Prereqs/DFT.lean

@@ -14,7 +14,7 @@ attribute [-ext] Complex.ext
 
 open AddChar Finset Function
 open Fintype (card)
-open scoped BigOperators ComplexConjugate ComplexOrder
+open scoped BigOps ComplexConjugate ComplexOrder
 
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
 
@@ -56,25 +56,26 @@ lemma l2norm_dft_sq (f : α → ℂ) : ‖dft f‖_[2] ^ 2 = card α * ‖f‖_[
   simpa using congr_arg Real.sqrt (l2norm_dft_sq f)
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
-lemma dft_inversion (f : α → ℂ) (a : α) : ∑ ψ : AddChar α ℂ, dft f ψ * ψ a = card α * f a := by
-  classical simp_rw [dft, l2inner_eq_sum, sum_mul, @sum_comm _ α, mul_right_comm _ (f _), ←sum_mul,
-    ←AddChar.inv_apply_eq_conj, inv_mul_eq_div, ←map_sub_eq_div, AddChar.sum_apply_eq_ite,
-    sub_eq_zero, ite_mul, MulZeroClass.zero_mul, Fintype.sum_ite_eq]
+lemma dft_inversion (f : α → ℂ) (a : α) : 𝔼 ψ, dft f ψ * ψ a = f a := by
+  classical simp_rw [dft, l2inner_eq_sum, sum_mul, expect_sum_comm, mul_right_comm _ (f _),
+    ← expect_mul, ←AddChar.inv_apply_eq_conj, inv_mul_eq_div, ←map_sub_eq_div, 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, expect, card_univ, AddChar.card_eq]; simp
 
 lemma dft_dft_doubleDualEmb (f : α → ℂ) (a : α) :
     dft (dft f) (doubleDualEmb a) = card α * f (-a) := by
-  simp only [←dft_inversion, mul_comm (conj _), dft_apply, l2inner_eq_sum, map_neg_eq_inv,
-    AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
+  simp only [←dft_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]
 
 lemma dft_dft (f : α → ℂ) : dft (dft f) = card α * f ∘ doubleDualEquiv.symm ∘ Neg.neg :=
   funext fun a ↦ by
     simp_rw [Pi.mul_apply, Function.comp_apply, map_neg, Pi.nat_apply, ←dft_dft_doubleDualEmb,
       doubleDualEmb_doubleDualEquiv_symm_apply]
 
 lemma dft_injective : Injective (dft : (α → ℂ) → AddChar α ℂ → ℂ) := fun f g h ↦
-  funext fun a ↦
-    mul_right_injective₀ (Nat.cast_ne_zero.2 Fintype.card_ne_zero) $
-      (dft_inversion _ _).symm.trans $ by rw [h, dft_inversion]
+  funext fun a ↦ (dft_inversion _ _).symm.trans $ by rw [h, dft_inversion]
 
 lemma dft_inv (ψ : AddChar α ℂ) (hf : IsSelfAdjoint f) : dft f ψ⁻¹ = conj (dft f ψ) := by
   simp_rw [dft_apply, l2inner_eq_sum, map_sum, AddChar.inv_apply', map_mul,
@@ -147,8 +148,8 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → 
   swap
   sorry -- positivity
   obtain ⟨n, rfl⟩ := hn.two_dvd
-  simp_rw [lpNorm_pow_eq_sum hn₀, mul_sum, ←mul_pow, ←nsmul_eq_mul, ←norm_nsmul, nsmul_eq_mul, ←
-    dft_inversion, dft_conv, dft_dconv, Pi.mul_apply]
+  simp_rw [lpNorm_pow_eq_sum 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

LeanAPAP/Prereqs/Rudin.lean

@@ -1,5 +1,6 @@
 import LeanAPAP.Mathlib.Algebra.Support
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
+import LeanAPAP.Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Exponential
 import LeanAPAP.Prereqs.Dissociation
@@ -9,17 +10,57 @@ import LeanAPAP.Prereqs.DFT
 # Rudin's inequality
 -/
 
-open Finset Function Real
+attribute [-simp] Complex.norm_eq_abs
+
+namespace Complex
+
+
+end Complex
+
+open Finset hiding card
+open Fintype (card)
+open Function Real
 open Complex (I re im)
 open scoped BigOps Nat NNReal ENNReal
 
 variable {α : Type*} [Fintype α] [AddCommGroup α] {p : ℕ}
 
 /-- **Rudin's inequality**, exponential form. -/
 lemma rudin_exp_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support $ dft f) :
-    𝔼 a, exp |(f a).re| ≤ exp (‖f‖_[2] ^ 2 / 2) :=
+    𝔼 a, exp (card α * f a).re ≤ exp (‖f‖_[2] ^ 2 / 2) := by
+  have (z : ℂ) : exp (re z) ≤ cosh ‖z‖ + re (z / ‖z‖) * sinh ‖z‖ :=
+    calc
+      _ = _ := by obtain rfl | hz := eq_or_ne z 0 <;> simp [norm_pos_iff.2, *]
+      _ ≤ _ := exp_le_cosh_add_mul_sinh (by simpa [abs_div] using z.abs_re_div_abs_le_one) _
+  choose c hc hcf using fun ψ ↦ Complex.exists_norm_mul_eq_self (dft f ψ)
+  have hc₀ (ψ) : c ψ ≠ 0 := fun h ↦ by simpa [h] using hc ψ
+  have (a) :
+    exp (card α * f a).re ≤ ∏ ψ, (cosh ‖dft f ψ‖ + (c ψ * ψ a).re * sinh ‖dft f ψ‖) :=
+    calc
+      _ = ∏ ψ, exp (dft f ψ * ψ a).re := by
+          rw [← exp_sum, ← dft_inversion', Complex.re_sum]
+      _ ≤ _ := prod_le_prod (fun _ _ ↦ by positivity) fun _ _ ↦ this _
+      _ = ∏ ψ, (cosh ‖dft f ψ‖ +
+            (c ψ * (dft f ψ * ψ a) / (c ψ * ↑‖dft f ψ‖)).re * sinh ‖dft f ψ‖) := by
+          simp_rw [norm_mul, AddChar.norm_apply, mul_one, mul_div_mul_left _ _ (hc₀ _)]
+      _ = _ := by
+          congr with ψ
+          obtain hψ | hψ := eq_or_ne (dft f ψ) 0
+          · simp [hψ]
+          · simp only [hcf, mul_left_comm (c _), mul_div_cancel_left _ hψ]
+  calc
+    _ ≤ 𝔼 a, ∏ ψ, (cosh ‖dft f ψ‖ + (c ψ * ψ a).re * sinh ‖dft f ψ‖) :=
+         expect_le_expect fun _ _ ↦ this _
+    _ = _ := ?_
   sorry
 
+
+  -- calc
+  --   _ = exp (𝔼 a, 𝔼 ψ, dft f ψ * ψ a).re
+  -- rw [← dft_inversion']
+  -- calc
+  --   _ = exp (∑ )
+
 private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support $ dft f) :
     ‖re ∘ f‖_[p] ≤ exp 2⁻¹ * sqrt p * ‖f‖_[2] := by
   wlog hfp : ‖f‖_[2] = sqrt p with H