FiveProducts.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.FiveProducts.character_map_sum line 8

theorem OAI.Problem337.FiveProducts.character_sum line 17

Source documentation

Orthogonality for the standard character on a finite cyclic group.

theorem character_sum {p : ℕ} [NeZero p] (t : ZMod p) :
    (∑ r : ZMod p, ZMod.stdAddChar (t * r)) =
      if t = 0 then (p : ℂ) else 0 := by
…

theorem OAI.Problem337.FiveProducts.moment_eq_zero_of_no_zero_sum line 25

Source documentation

The character moment vanishes if no tuple has zero sum.

theorem moment_eq_zero_of_no_zero_sum {p : ℕ} [NeZero p]
    {X : Type*} [Fintype X] (f : X → ZMod p) (n : ℕ)
    (h : ∀ v : Fin n → X, ∑ i, f (v i) ≠ 0) :
    (∑ r : ZMod p, (∑ x : X, ZMod.stdAddChar (f x * r)) ^ n) = 0 := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.FiveProducts.exists_zero_sum_of_character_bound line 44

Source documentation

A strict spectral bound forces a zero-sum tuple. The estimate uses p rather than p-1, which is convenient and sufficient for five products.

theorem exists_zero_sum_of_character_bound {p : ℕ} [NeZero p]
    {X : Type*} [Fintype X] (f : X → ZMod p) (n : ℕ) (B : ℝ)
    (hB : 0 ≤ B)
    (hchar : ∀ r : ZMod p, r ≠ 0 →
      ‖∑ x : X, ZMod.stdAddChar (f x * r)‖ ≤ B)
    (hsize : (p : ℝ) * B ^ n < (Fintype.card X : ℝ) ^ n) :
    ∃ v : Fin n → X, ∑ i, f (v i) = 0 := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.FiveProducts.character_parseval line 84

Source documentation

Parseval for the standard character restricted to a set.

theorem character_parseval {p : ℕ} [Fact p.Prime] (H : Finset (ZMod p))
    (r : ZMod p) (hr : r ≠ 0) :
    (∑ a : ZMod p, ‖∑ b ∈ H, ZMod.stdAddChar (b * a * r)‖ ^ 2) =
      (p : ℝ) * H.card := by
…

theorem OAI.Problem337.FiveProducts.bilinear_character_bound line 120

Source documentation

The finite-field bilinear character bound, in unnormalised form.

theorem bilinear_character_bound {p : ℕ} [Fact p.Prime]
    (H : Finset (ZMod p)) (r : ZMod p) (hr : r ≠ 0) :
    ‖∑ a ∈ H, ∑ b ∈ H, ZMod.stdAddChar (b * a * r)‖ ≤
      Real.sqrt p * H.card := by
…

theorem OAI.Problem337.FiveProducts.five_products_zero_of_power_bound line 154
Source documentation
Five products from a sufficiently large set in a prime field have sum zero. The integral threshold is slightly stronger than the optimal Fourier threshold only in its strictness, and is implied by |H| > p^(3/4).
```
theorem five_products_zero_of_power_bound {p : ℕ} [Fact p.Prime]
    (H : Finset (ZMod p)) (hsize : p ^ 7 < H.card ^ 10) :
    ∃ a b : Fin 5 → H, ∑ i, (a i : ZMod p) * (b i : ZMod p) = 0 := by
…
```

theorem OAI.Problem337.FiveProducts.five_products_zero line 188

Source documentation

The five-product conclusion at the p^(3/4) threshold used in rational-divisor supply.

theorem five_products_zero {p : ℕ} [Fact p.Prime]
    (H : Finset (ZMod p)) (hsize : (p : ℝ) ^ (3 / 4 : ℝ) < H.card) :
    ∃ a b : Fin 5 → H, ∑ i, (a i : ZMod p) * (b i : ZMod p) = 0 := by
…