OAI/NumberTheory/DirichletL/Energy/CappedWidthInduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.bandWidth line 22
2. lemma OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.bandWidth_le line 23
3. lemma OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.bandWidth_le_schedule line 24
4. lemma OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.bandWidth_nonneg line 25
5. lemma OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.bandWidth_terminal line 31
6. lemma OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.actual_child_band line 36
7. def OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.CertifiedBand line 49
8. theorem OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.certified_floor line 63
9. theorem OAI.SevenEighths.CenteredMomentEnergyCappedWidthInduction.certified_terminal line 94