OAI/NumberTheory/DirichletL/Energy/WidthRanges.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyWidthRanges.step line 12
2. def OAI.SevenEighths.CenteredMomentEnergyWidthRanges.range line 13
3. def OAI.SevenEighths.CenteredMomentEnergyWidthRanges.sourceCap line 16
4. def OAI.SevenEighths.CenteredMomentEnergyWidthRanges.finalSourceCap line 17
5. def OAI.SevenEighths.CenteredMomentEnergyWidthRanges.fineMesh line 18
6. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.range_nonneg line 20
7. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.range_mono line 25
8. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.range_original line 32
9. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.step_admits line 35
10. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.range_envelope line 52
11. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.ready_exponent_le line 66
12. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.sourceCap_nonneg line 79
13. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.fineMesh_pos line 84
14. lemma OAI.SevenEighths.CenteredMomentEnergyWidthRanges.support_step line 89