OAI/NumberTheory/CubicMoment/Estimates/WidePoissonRecurrence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common-factor quotient rows retain a fixed compact norm range; the wide Mellin operator bound supplies their exact Poisson recurrence.

  1. theorem OAI.CubicFirstMoment.wide_coprimePoissonDyad_norm_recurrence line 14