OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/RationalPrimeBlockBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SourcePrimeFactor.rationalPrimeBlockBudget line 25
2. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.prime_block_near_rational line 29
3. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.global_packet_near_rational_blocks line 55
4. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.actual_short_near_rational_blocks line 74
5. def OAI.OrdinaryCorrelations.SourcePrimeFactor.normalizedRationalPrimeBlockBudget line 115
6. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.prime_block_normalized_rational_budget line 120
7. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.actual_short_near_rational_blocks_normalized line 144