OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SourceLocalSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceTailoredBoxSieve.source_local_sum line 27
2. lemma OAI.OrdinaryCorrelations.SourceTailoredBoxSieve.source_boundary_numerator line 49
3. lemma OAI.OrdinaryCorrelations.SourceTailoredBoxSieve.eventually_boundary_margin line 93
4. lemma OAI.OrdinaryCorrelations.SourceTailoredBoxSieve.source_boundary_small line 114