OAI/NumberTheory/CubicGram/CubeEstimates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Geometric decay, cube frequency dyads and numerical block inequalities.

  1. lemma OAI.CubicFirstMoment.geometric_decay_step line 16
  2. lemma OAI.CubicFirstMoment.geometric_decay_partial_sum line 35
  3. lemma OAI.CubicFirstMoment.geometric_decay_tsum line 52
  4. lemma OAI.CubicFirstMoment.rpow_cutoff_comparison line 60
  5. lemma OAI.CubicFirstMoment.real_dyadic_decay line 79
  6. def OAI.CubicFirstMoment.squarefreePrimaryDyad line 117
  7. lemma OAI.CubicFirstMoment.mem_squarefreePrimaryDyad line 120
  8. def OAI.CubicFirstMoment.cubeDyadTriples line 124
  9. lemma OAI.CubicFirstMoment.mem_cubeDyadTriples line 128
  10. lemma OAI.CubicFirstMoment.cubeDyadTriples_card line 133
  11. lemma OAI.CubicFirstMoment.eisenstein_norm_pow line 139

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/CubeLattice.lean:20 (different declaration text). Qualify references as OAI.CubicFirstMoment.eisenstein_norm_pow@path.

  12. def OAI.CubicFirstMoment.cubeFrequencyCover line 144
  13. lemma OAI.CubicFirstMoment.frequencyDyad_subset_cubeCover line 148
  14. lemma OAI.CubicFirstMoment.finiteCubicBound_biUnion line 188
  15. theorem OAI.CubicFirstMoment.finiteCubicBound_frequency_cube line 210
  16. lemma OAI.CubicFirstMoment.rpow_third_cube line 233
  17. lemma OAI.CubicFirstMoment.rpow_two_thirds_cube line 237
  18. lemma OAI.CubicFirstMoment.cube_block_numerical line 241