OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrimeCountZeroIff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.primeCount_zero_iff line 22
2. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.multiples_Icc_card line 31
3. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.ramareArithmeticExceptions_card line 40
4. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.binnedRamare_arithmetic_energy line 69