OAI/NumberTheory/CubicMoment/Theta/CubicThetaJointMajorant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Summable bounds for the actual full differential on positive strips.

  1. lemma OAI.CubicFirstMoment.cubicThetaAngular_uniform_terms line 9
  2. lemma OAI.CubicFirstMoment.cubicThetaAngular_uniform_vertical_terms line 34
  3. theorem OAI.CubicFirstMoment.cubicThetaAngular_uniform_differentials line 59