OAI/NumberTheory/CubicMoment/Estimates/FiniteSieveDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Identify the finite square-divisor density with the already proved convergent Möbius residue series.

  1. lemma OAI.CubicFirstMoment.collectedSieve_weighted_sum_real line 12
  2. lemma OAI.CubicFirstMoment.collectedSieve_eq_zero_off_image line 19
  3. lemma OAI.CubicFirstMoment.finiteSieveDensity_eq_sum line 26
  4. lemma OAI.CubicFirstMoment.finiteSieveDensity_eq_residue line 32
  5. theorem OAI.CubicFirstMoment.finiteSieveDensity_error line 52