OAI/NumberTheory/CubicMoment/Estimates/SievedModelAssembly.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact finite sieve assembly and its error norm. These identities retain the actual joined square divisors and their Möbius weights.

  1. lemma OAI.CubicFirstMoment.collectedSieve_weighted_sum line 13
  2. lemma OAI.CubicFirstMoment.sievedDispersionVariance_pair_sum line 35
  3. def OAI.CubicFirstMoment.finiteSieveDensity line 46
  4. lemma OAI.CubicFirstMoment.finiteSieve_model_identity line 50
  5. lemma OAI.CubicFirstMoment.sieved_model_error_bound line 62