OAI/NumberTheory/CubicMoment/Estimates/CoprimePoissonSeries.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Identify the complete nonzero dyadic Poisson series with the original coprime portion of the dispersion Gram form.

  1. lemma OAI.CubicFirstMoment.coprimeDispersionGram_eq_poisson_series line 13