OAI/NumberTheory/CubicMoment/Estimates/TripleTransitionSmoothed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full Mellin transfer of the exceptional triple transition estimate. The complementary integral is retained and bounded using the genuine height mean through B^(7/20), then rapid transform decay.

  1. theorem OAI.CubicFirstMoment.two_prime_transition_smoothed line 17