OAI/NumberTheory/DirichletL/Energy/Profiles.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentEnergyProfiles.Test line 12
2. def OAI.SevenEighths.CenteredMomentEnergyProfiles.lower line 16
3. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.lower_pos line 20
4. def OAI.SevenEighths.CenteredMomentEnergyProfiles.derivativeChoice line 25
5. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.derivativeChoice_apply line 28
6. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.derivativeChoice_support line 35
7. def OAI.SevenEighths.CenteredMomentEnergyProfiles.step line 41
8. theorem OAI.SevenEighths.CenteredMomentEnergyProfiles.step_control line 46
9. inductive OAI.SevenEighths.CenteredMomentEnergyProfiles.Path line 79
10. theorem OAI.SevenEighths.CenteredMomentEnergyProfiles.path_control line 86
11. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.lower_antitone line 113
12. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.support_at_depth line 118
13. theorem OAI.SevenEighths.CenteredMomentEnergyProfiles.paths_upto_control line 124
14. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.annulus_support line 155
15. def OAI.SevenEighths.CenteredMomentEnergyProfiles.annulusTemplate line 161
16. lemma OAI.SevenEighths.CenteredMomentEnergyProfiles.annulusTemplate_apply line 166
17. def OAI.SevenEighths.CenteredMomentEnergyProfiles.annulusSeed line 168