OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactExponential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Entire dependence of the compact incoming correction. Only an integrable amplitude and a bounded continuous real exponent are needed.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompactExponential_differentiable line 13