OAI/NumberTheory/CubicMoment/Estimates/CoprimeDispersionPoisson.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact cube/noncube splitting of the coprime portion of the variance. No diagonal or shared-prime contribution is silently included here.

  1. lemma OAI.CubicFirstMoment.tsum_split_nonzero_cubes line 12
  2. def OAI.CubicFirstMoment.coprimeDispersionGram line 43
  3. def OAI.CubicFirstMoment.cubePoissonContribution line 48
  4. theorem OAI.CubicFirstMoment.coprimeDispersionGram_split line 56