OAI/NumberTheory/Ostmann/QuadraticCenter/FourthMomentFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the nonprincipal fourth moment over bottom-pair characters

Only the common mass bound, the maximum squared mass, and the total squared mass of the nonnegative Fourier weights enter this calculation.

  1. theorem OAI.Ostmann.nonprincipal_fourth_family_bound line 22