OAI/NumberTheory/CubicMoment/Estimates/ThinAnnulusCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A genuine thin-annulus lattice count. Disjoint half-unit disks around Eisenstein integers fit inside the thickened annulus.

  1. lemma OAI.CubicFirstMoment.eisenstein_dist_ge_one line 13
  2. lemma OAI.CubicFirstMoment.complex_ball_real_volume line 20
  3. theorem OAI.CubicFirstMoment.eisenstein_annulus_card line 25
  4. theorem OAI.CubicFirstMoment.eisenstein_thin_annulus_card line 94