OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/NormalizedPrimeBlockBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SourcePrimeFactor.normalizedPrimeBlockBudget line 24
2. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.prime_block_normalized_budget line 29
3. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.actual_short_minor_arc_blocks_normalized line 53