OAI/NumberTheory/Ostmann/Characters/SparseUnitPolydisc.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sparseUnitPolynomial line 11
2. theorem OAI.Ostmann.small_unit_ratio line 15
3. theorem OAI.Ostmann.sparseUnitPolynomial_norm_le line 23
4. theorem OAI.Ostmann.sparseUnitPolynomial_mean line 62

   Source documentation

   Exact unit mean for both complex polynomial coefficients.

   theorem sparseUnitPolynomial_mean {p : ℕ} [NeZero p]
       (E : Finset (ZMod p)) (hE : 0 ∉ E) (hsym : ∀ b, -b ∈ E ↔ b ∈ E)
       (hp : 1 < p) (c d : ℂ) :
       sparseUnitPolynomial p ((E.card : ℝ) / p) c d =
         ((p : ℂ) - 1)⁻¹ * ∑ x ∈ Finset.univ.erase 0,
           (1 + c * localSparseKernel E x + d * localSparseSquare E x) := by
   …

   Mentions: OAI.Ostmann.sparseUnitPolynomial, OAI.Ostmann.localSparseKernel, OAI.Ostmann.localSparseSquare

5. theorem OAI.Ostmann.sparse_unit_polydisc_bound line 83

   Source documentation

   The scalar mean on the same polydisc as the operator has a uniform 1+6/p bound, independent of the dimension of the residue space.

   theorem sparse_unit_polydisc_bound {p : ℕ} [Fact p.Prime]
       (E : Finset (ZMod p)) (hE : 0 ∉ E) (hsym : ∀ b, -b ∈ E ↔ b ∈ E)
       (ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hcard : (E.card : ℝ) ≤ ε * p)
       (u v : ℂ) (hu : ‖u‖ ≤ 103 / 100) (hv : ‖v‖ ≤ 103 / 100) :
       ‖((p : ℂ) - 1)⁻¹ * ∑ x ∈ Finset.univ.erase 0,
         (1 + u * localSparseKernel E x) * (1 + v * localSparseKernel E x)‖ ≤
         1 + 6 / (p : ℝ) := by
   …

   Mentions: OAI.Ostmann.localSparseKernel