OAI/NumberTheory/CubicMoment/Estimates/CubicCoreCoverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual coverage of a noncube frequency by either the low-core set or a ramified/squarefree pair of large conductor. No decomposition is assumed.

  1. lemma OAI.CubicFirstMoment.norm_cube line 11
  2. lemma OAI.CubicFirstMoment.cube_part_norm_bound line 14
  3. lemma OAI.CubicFirstMoment.mem_lowNoncubeSupport_of_core line 28
  4. theorem OAI.CubicFirstMoment.noncube_large_core_decomposition line 37