OAI/NumberTheory/Ostmann/Construction/PrimeGroupBins.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.PrimeGroupSample line 13
2. def OAI.Ostmann.Construction.primeGroupPrior line 15
3. def OAI.Ostmann.Construction.primeGroupLog line 18
4. def OAI.Ostmann.Construction.primeGroupBalanced line 21
5. def OAI.Ostmann.Construction.primeGroupBinMass line 24
6. theorem OAI.Ostmann.Construction.primeGroupBalanced_mean_lower line 28
7. theorem OAI.Ostmann.Construction.primeGroupLog_bounds line 38
8. theorem OAI.Ostmann.Construction.exists_primeGroup_bin line 50
9. theorem OAI.Ostmann.Construction.harmonicBand_log_support line 74