OAI/NumberTheory/Ostmann/Characters/SparseKernelUnitFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unit-residue normalizing factor at the fixed kernel parameter

  1. def OAI.Ostmann.sparseKernelUnitFactor line 10
  2. theorem OAI.Ostmann.sparseKernelUnitFactor_lower line 13
  3. theorem OAI.Ostmann.sparseKernelUnitFactor_positive line 30
  4. theorem OAI.Ostmann.sparseKernelUnitFactor_mean line 40

    Source documentation

    The closed expression is the actual mean of (1+b)^2 on nonzero residues, with b the manuscript's fixed 17/20 kernel.

    theorem sparseKernelUnitFactor_mean {p : ℕ} [NeZero p]
    (E : Finset (ZMod p)) (hE : 0 ∉ E) (hsym : ∀ b, -b ∈ E ↔ b ∈ E)
    (hp : 1 < p) :
    ((sparseKernelUnitFactor p ((E.card : ℝ) / p) : ℝ) : ℂ) =
      ((p : ℂ) - 1)⁻¹ * ∑ x ∈ Finset.univ.erase 0,
        (1 + sparseAdditiveKernel E (17 / 20) x) ^ 2 := by
…

    Mentions: OAI.Ostmann.sparseKernelUnitFactor, OAI.Ostmann.sparseAdditiveKernel