OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MovingCompactUnweightedSmall.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OrdinaryCorrelations.PretentiousEuler.moving_compact_unweighted_smallline 24 - theorem
OAI.OrdinaryCorrelations.PretentiousEuler.moving_global_derivative_smallline 59