OAI/NumberTheory/CubicMoment/Theta/CubicThetaAngularLeftBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds on far-left lines for the actual continued angular series.

  1. theorem OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_left_bound line 11