OAI/NumberTheory/CubicMoment/Estimates/TripleTransitionHeight.lean

GitHub source file

2 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. lemma OAI.CubicFirstMoment.two_prime_unit_energy line 12
  2. theorem OAI.CubicFirstMoment.two_prime_transition_height line 31