OAI/NumberTheory/CubicMoment/Estimates/DivisorHighSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A small square divisor preserves the positive-power separation between the high-frequency cutoff and its actual Poisson scale.

  1. theorem OAI.CubicFirstMoment.divisor_high_poisson_log_saving line 15