Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Fourier decay from realized residues

Abstract

Fourier decay from realized residues.

Theorem 1.1 (Fourier decay from realized residues).

Lean statement: D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCount.tendsto_sum_char_mul_cardNormLeResidue_div_of_realized

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCount.tendsto_sum_char_mul_cardNormLeResidue_div_of_realized (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

Fourier decay from realized residues. Let S ≤ (ℤ/c)ˣ be a subgroup all of whose elements are realized as ideal-norm residues (hS). Then for every nontrivial character χ of S, the χ-twisted norm-residue count average over S tends to 0: (∑_{s ∈ S} χ(s)·#{N(I) ≤ N, N(I) ≡ s}) / N → 0.

References