OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite boxes and the geometric tails bound the complete coordinate sums.

  1. lemma OAI.CubicFirstMoment.cubic_finite_complement_sum line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimary_coordinate_mass line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaRamified_coordinate_mass line 54