OAI/NumberTheory/TwoPoint/Fourier/MajorArcPerturbedGlobal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Major-arc perturbation for the literal typical coefficient. Very short prefixes use boundedness; every longer prefix uses the proved character mean.

  1. theorem OAI.TwoPointCorrelations.major_arc_typical_perturbed_global line 13