OAI/NumberTheory/CubicMoment/Decomposition/StoppedBoundedRadial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal bounded-coefficient Poisson annulus, with its square-root norm denominator and unrestricted original height.

  1. theorem OAI.CubicFirstMoment.bounded_coprime_radial_form line 14