OAI/NumberTheory/CubicMoment/Estimates/SquarefreeMassDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative identification of the ordinary squarefree model mass with the finite density in the positive variance term.

  1. lemma OAI.CubicFirstMoment.squarefree_density_scale line 13
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.squarefreeModelMass_density_error line 23