OAI/NumberTheory/CubicMoment/Decomposition/StoppedRadialForm.lean

GitHub source file

2 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. lemma OAI.CubicFirstMoment.stoppedIntervalSupport_scaled_norm line 17
  2. theorem OAI.CubicFirstMoment.stopped_noncube_radial_form line 25