OAI/NumberTheory/DirichletL/Energy/OriginalSource.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyOriginalSource.completeInput line 25
2. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalSource.input_tuplePool line 52
3. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalSource.input_polynomial_difference line 57
4. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalSource.normalized_input_difference line 76
5. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalSource.input_energy_hasSum line 90
6. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalSource.kept_difference_energy line 106
7. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalSource.input_positive_summable line 132
8. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalSource.positive_energy_comparison line 143
9. def OAI.SevenEighths.CenteredMomentEnergyOriginalSource.naturalData line 225
10. def OAI.SevenEighths.CenteredMomentEnergyOriginalSource.naturalInput line 265
11. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalSource.natural_energy_comparison line 273