OAI/NumberTheory/CubicMoment/Angular/AngularHeightPoissonAnnulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The genuine finite Poisson contribution inherits the averaged annular estimate with its exact geometric scalar A/(9L).

  1. theorem OAI.CubicFirstMoment.angular_height_poisson_annulus_saving line 16