OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/GlobalPacket.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SourcePrimeFactor.globalPacket line 26
2. def OAI.OrdinaryCorrelations.SourcePrimeFactor.globalCoprimePacket line 31
3. def OAI.OrdinaryCorrelations.SourcePrimeFactor.additiveBudget line 36
4. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_packet_minor_arc line 40
5. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_coprime_error line 65
6. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.sum_range_succ_Ioc line 105
7. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_coprime_is_bilinear line 120