OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/QuadraticGeometricLimit.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OrdinaryMellinModulus.quadratic_geometric_limitline 23 - lemma
OAI.OrdinaryMellinModulus.choose_initial_offsetline 36 - lemma
OAI.OrdinaryMellinModulus.powered_rateline 52