OAI/NumberTheory/CubicMoment/Angular/AngularTripleTransitionHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coarse height means for the actual two-prime/one-prime product at the transition, used only in the complementary Mellin integral.

  1. theorem OAI.CubicFirstMoment.angular_two_prime_transition_height line 15