OAI/NumberTheory/CubicMoment/Estimates/CoreBlockGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The geometric cube cutoff in each actual core block has precisely the mass scale needed by the noncube moment estimates.

  1. lemma OAI.CubicFirstMoment.coreDyadicCubeFactors_spec line 11
  2. lemma OAI.CubicFirstMoment.rpow_eight_third line 21
  3. lemma OAI.CubicFirstMoment.coreDyadicCubeFactors_card_eight_weight line 26