OAI/NumberTheory/Ostmann/Characters/SquareAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Domination of a uniform square-coset average

The square map on the unit group has fibers of size at most two. Its pushforward therefore has density at most two against the uniform law.

  1. theorem OAI.Ostmann.sum_square_coset_le_twice line 17
  2. theorem OAI.Ostmann.sum_inverse_square_coset_le_twice line 49

    Source documentation

    Inverting the sampling coordinate preserves the same square-coset bound.

    theorem sum_inverse_square_coset_le_twice {p : ℕ} [Fact p.Prime]
    (K : (ZMod p)ˣ) (f : (ZMod p)ˣ → ℝ) (hf : ∀ u, 0 ≤ f u) :
    (∑ z : (ZMod p)ˣ, f (K * (z⁻¹) ^ 2)) ≤ 2 * ∑ u : (ZMod p)ˣ, f u := by
…