OAI/NumberTheory/GaussianMoat/DenseBins.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GaussianMoat.PrimeLogMass.dyadicBatch line 14
2. lemma OAI.GaussianMoat.PrimeLogMass.mem_dyadicBatch line 17
3. lemma OAI.GaussianMoat.PrimeLogMass.logBin_mem line 22
4. lemma OAI.GaussianMoat.PrimeLogMass.prime_log_mass_le_theta line 28
5. def OAI.GaussianMoat.PrimeLogMass.dyadicMass line 40
6. lemma OAI.GaussianMoat.PrimeLogMass.dyadicMass_nonneg line 43
7. lemma OAI.GaussianMoat.PrimeLogMass.dyadicMass_le line 49
8. lemma OAI.GaussianMoat.PrimeLogMass.dyadicMass_le_card line 68
9. theorem OAI.GaussianMoat.PrimeLogMass.many_dense_bins line 82
10. def OAI.GaussianMoat.PrimeLogMass.splitWindow line 124
11. def OAI.GaussianMoat.PrimeLogMass.windowBins line 127
12. lemma OAI.GaussianMoat.PrimeLogMass.split_residue_mass line 130
13. lemma OAI.GaussianMoat.PrimeLogMass.window_mass_le_bins line 138
14. lemma OAI.GaussianMoat.PrimeLogMass.windowBin_bounds line 167
15. lemma OAI.GaussianMoat.PrimeLogMass.windowBins_card line 186
16. theorem OAI.GaussianMoat.PrimeLogMass.eventually_dense_split_bins line 203