OAI/NumberTheory/CubicMoment/Angular/AngularPrimeTransitionHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The coarse height mean at the transition keeps the prime diagonal. It supplies the full Mellin complement without a logarithmic gap between the outer length and the square of the inner length.

  1. theorem OAI.CubicFirstMoment.angular_single_prime_transition_height_variance line 16