OAI/NumberTheory/PrimePackets/IntervalGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.cast_div_gt_sub_one line 34
2. lemma OAI.PrimeDegreePackets.cast_div_interval_bounds line 43
3. lemma OAI.PrimeDegreePackets.cast_div_interval_relative line 53
4. lemma OAI.PrimeDegreePackets.cast_div_interval_width line 66
5. lemma OAI.PrimeDegreePackets.div_square_lower line 76
6. lemma OAI.PrimeDegreePackets.weightedIdealInterval_split line 98
7. theorem OAI.PrimeDegreePackets.weightedIdeal_small_norm_bound line 119
8. lemma OAI.PrimeDegreePackets.weighted_cutoff_div_lower line 208
9. lemma OAI.PrimeDegreePackets.eventual_weighted_small_parameters line 231
10. lemma OAI.PrimeDegreePackets.weighted_cutoff_large_iff line 274
11. lemma OAI.PrimeDegreePackets.weighted_log_power_error line 286
12. lemma OAI.PrimeDegreePackets.eventual_weighted_tail_absorption line 296
13. lemma OAI.PrimeDegreePackets.dedekindZeta_real_one_le line 347
14. theorem OAI.PrimeDegreePackets.weightedIdeal_interval_zeta_bound line 356