OAI/NumberTheory/DirichletL/CubicSieve/FrequencyDyads.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CubicSieve.frequencyDyadline 11 - lemma
OAI.SevenEighths.CubicSieve.mem_frequencyDyadline 14 - lemma
OAI.SevenEighths.CubicSieve.frequencyDyad_boundsline 25 - def
OAI.SevenEighths.CubicSieve.frequencyDyadicEquivline 38 - theorem
OAI.SevenEighths.CubicSieve.tsum_frequencyDyadsline 50 - theorem
OAI.SevenEighths.CubicSieve.tsum_frequencyDyads_with_zeroline 70