OAI/NumberTheory/CubicMoment/Estimates/CubicDyadicCoverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A finite cover of all noncube frequencies outside the small-core set by the actual coprime ramified/squarefree blocks used in the moment bounds.

  1. def OAI.CubicFirstMoment.coreDyadicConductor line 14
  2. lemma OAI.CubicFirstMoment.coreDyadicConductor_pos line 16
  3. def OAI.CubicFirstMoment.largeCoreDyadicIndices line 20
  4. def OAI.CubicFirstMoment.coreDyadicCubeFactors line 25
  5. def OAI.CubicFirstMoment.coreDyadicBlock line 28
  6. lemma OAI.CubicFirstMoment.squarefreePrimaryDyad_gramDyad line 32
  7. lemma OAI.CubicFirstMoment.real_cube_scale_bound line 44
  8. theorem OAI.CubicFirstMoment.noncube_mem_coreDyadicBlock line 53