OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/TentPhaseIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryLogIntegral.tentPhase_integral line 15
2. lemma OAI.OrdinaryLogIntegral.tentPhase_integral_span line 41
3. theorem OAI.OrdinaryLogIntegral.tent_progression_error line 65
4. theorem OAI.OrdinaryLogIntegral.tent_progression_bound line 82