OAI/NumberTheory/CubicMoment/Angular/AngularStoppedRadialForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A noncube Poisson annulus for literal early-stopped coefficients. The coefficient interval is an actual dyad; its normalized log range and ambient prime support are constructed here.

  1. theorem OAI.CubicFirstMoment.angular_stopped_noncube_radial_form line 19