BilinearFourier.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.residueFourier line 10
Source documentation
The positive-sign discrete Fourier transform, convenient for residue products.
```
def residueFourier {q : ℕ} [NeZero q] (β : ZMod q → ℂ) (x : ZMod q) : ℂ :=
…
```
lemma OAI.Problem337.residue_character_orthogonality line 13

theorem OAI.Problem337.residueFourier_parseval line 23

Source documentation

Parseval's identity for the positive-sign transform on all residue classes.

theorem residueFourier_parseval {q : ℕ} [NeZero q] (β : ZMod q → ℂ) :
    (∑ x : ZMod q, ‖residueFourier β x‖ ^ 2) =
      (q : ℝ) * ∑ y : ZMod q, ‖β y‖ ^ 2 := by
…

Mentions: OAI.Problem337.residueFourier

theorem OAI.Problem337.residueFourier_parseval_unit line 51

Source documentation

A unit frequency preserves the Parseval identity, also for composite moduli.

theorem residueFourier_parseval_unit {q : ℕ} [NeZero q]
    (β : ZMod q → ℂ) (c : (ZMod q)ˣ) :
    (∑ x : ZMod q, ‖residueFourier β ((c : ZMod q) * x)‖ ^ 2) =
      (q : ℝ) * ∑ y : ZMod q, ‖β y‖ ^ 2 := by
…

Mentions: OAI.Problem337.residueFourier

theorem OAI.Problem337.residue_bilinear_bound line 62

Source documentation

The bilinear additive-character bound used for random prime products. No primality hypothesis on the modulus is needed; the frequency is a unit.

theorem residue_bilinear_bound {q : ℕ} [NeZero q]
    (α β : ZMod q → ℂ) (c : (ZMod q)ˣ) :
    ‖∑ x : ZMod q, ∑ y : ZMod q,
      α x * β y * ZMod.stdAddChar ((c : ZMod q) * x * y)‖ ≤
      Real.sqrt (q : ℝ) * Real.sqrt (∑ x : ZMod q, ‖α x‖ ^ 2) *
        Real.sqrt (∑ y : ZMod q, ‖β y‖ ^ 2) := by
…

theorem OAI.Problem337.residue_bilinear_finset_bound line 86

Source documentation

Equal finite sets give the classical sqrt(q) * |H| bilinear estimate.

theorem residue_bilinear_finset_bound {q : ℕ} [NeZero q]
    (H : Finset (ZMod q)) (c : (ZMod q)ˣ) :
    ‖∑ x ∈ H, ∑ y ∈ H, ZMod.stdAddChar ((c : ZMod q) * x * y)‖ ≤
      Real.sqrt (q : ℝ) * (H.card : ℝ) := by
…

lemma OAI.Problem337.probability_sum_sq_le line 103

Source documentation

A probability vector bounded by A has squared ℓ² norm at most A.

lemma probability_sum_sq_le {ι : Type*} [Fintype ι]
    (α : ι → ℝ) (A : ℝ) (hα : ∀ x, 0 ≤ α x)
    (hA : ∀ x, α x ≤ A) (hsum : ∑ x, α x = 1) :
    ∑ x, α x ^ 2 ≤ A := by
…

theorem OAI.Problem337.residue_bilinear_probability_bound line 114

Source documentation

The version for probability vectors used after controlling atom sizes in random products.

theorem residue_bilinear_probability_bound {q : ℕ} [NeZero q]
    (α β : ZMod q → ℝ) (A B : ℝ) (c : (ZMod q)ˣ)
    (hα : ∀ x, 0 ≤ α x) (hβ : ∀ y, 0 ≤ β y)
    (hA : ∀ x, α x ≤ A) (hB : ∀ y, β y ≤ B)
    (hsα : ∑ x, α x = 1) (hsβ : ∑ y, β y = 1) :
    ‖∑ x : ZMod q, ∑ y : ZMod q,
      (α x : ℂ) * (β y : ℂ) * ZMod.stdAddChar ((c : ZMod q) * x * y)‖ ≤
      Real.sqrt (q : ℝ) * Real.sqrt A * Real.sqrt B := by
…