OAI/NumberTheory/TwoPoint/Halasz/HalaszMomentInterpolation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The moment interpolation used to absorb colliding long variables. All functions live on the same finite coefficient torus.

  1. lemma OAI.TwoPointCorrelations.halasz_torus_geometric_mean line 12