OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pointwise geometric majorants beyond the finite coordinate boxes.

  1. def OAI.CubicFirstMoment.cubicThetaRadiusProfile line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRadiusProfile_derivative line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaRadiusProfile_antitone line 27
  4. def OAI.CubicFirstMoment.cubicThetaPrimaryTailMass line 38
  5. def OAI.CubicFirstMoment.cubicThetaRamifiedTailMass line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimaryTailMass_bound line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaRamifiedTailMass_bound line 61