OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrimeBlockPacket.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SourcePrimeFactor.primeBlockPacket line 24
2. def OAI.OrdinaryCorrelations.SourcePrimeFactor.primeBlockBudget line 29
3. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.prime_block_minor_arc line 33
4. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_packet_partition line 58
5. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_packet_minor_arc_blocks line 69
6. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.actual_short_minor_arc_blocks line 88