OAI/NumberTheory/CubicMoment/Angular/AngularDivisorHighSaving.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.angular_divisor_high_poisson_log_saving line 16