OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspExhaustionBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common square-integrable majorant for the exhaustion errors.

  1. lemma OAI.CubicFirstMoment.cubicThetaCuspExhaustion_sub_one_norm line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspExhaustion_value_bound line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspExhaustion_gradient_bound line 34