OAI/NumberTheory/Ostmann/Characters/SquarePullbackNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The small-kernel quadratic pullback norm

  1. theorem OAI.Ostmann.square_pullback_energy_le line 14

    Source documentation

    Vanishing at nonunits means only unit square fibers contribute. The general unit-root bound loses at most an absolute factor two.

    theorem square_pullback_energy_le (q : ℕ) [NeZero q]
    (g : ZMod q → ℂ) (hg : ∀ x, ¬IsUnit x → g x = 0) (a : ZMod q) :
    (∑ x : ZMod q, ‖g (a * x ^ 2)‖ ^ 2) ≤
      (2 : ℝ) ^ (q.primeFactors.card + 1) * ∑ y : ZMod q, ‖g y‖ ^ 2 := by
…
  2. theorem OAI.Ostmann.square_pullback_norm_le line 67