SquarePullback.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The factor two in square pullbacks

The finite-fiber bound and Cauchy--Schwarz estimate used in the manuscript's equation tree-square-pullback. Multiplicative characters are extended by zero at zero, as in the manuscript. Evaluations in these lemmas are at units.

theorem OAI.Ostmann.square_fiber_card_le_two line 24

theorem OAI.Ostmann.unit_square_fiber_card_le_two line 47

Source documentation

Squaring has at most two preimages among the units of a prime field.

theorem unit_square_fiber_card_le_two {p : ℕ} [Fact p.Prime]
    (s : Finset (ZMod p)ˣ) (u : (ZMod p)ˣ) :
    (s.filter fun x => x ^ 2 = u).card ≤ 2 := by
…

theorem OAI.Ostmann.mulChar_square_fiber_card_le_two line 60

Source documentation

The same two-point bound applies on the character group of a prime field.

theorem mulChar_square_fiber_card_le_two {p : ℕ} [Fact p.Prime]
    (s : Finset (MulChar (ZMod p) ℂ)) (ρ : MulChar (ZMod p) ℂ) :
    (s.filter fun χ => χ ^ 2 = ρ).card ≤ 2 := by
…

theorem OAI.Ostmann.norm_sq_sum_le_two line 76

theorem OAI.Ostmann.norm_mulChar_unit line 88

Source documentation

A multiplicative character has modulus one at each unit.

theorem norm_mulChar_unit {p : ℕ} [Fact p.Prime]
    (χ : MulChar (ZMod p) ℂ) (u : (ZMod p)ˣ) : ‖χ u‖ = 1 := by
…

theorem OAI.Ostmann.square_pullback_coefficients line 94

Source documentation

The two surviving Mellin coefficients in a square pullback satisfy the factor-two estimate, including their unit phases.

theorem square_pullback_coefficients {p : ℕ} [Fact p.Prime]
    (s : Finset (MulChar (ZMod p) ℂ)) (c : MulChar (ZMod p) ℂ → ℂ)
    (K : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
    ‖∑ χ ∈ s.filter (fun χ => χ ^ 2 = ρ), c χ * χ K‖ ^ 2 ≤
      2 * ∑ χ ∈ s.filter (fun χ => χ ^ 2 = ρ), ‖c χ‖ ^ 2 := by
…