OAI/NumberTheory/DirichletL/Moments/UncenteredTerminal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentUncenteredTerminal.uncenteredProfileCoefficient line 15
2. def OAI.SevenEighths.CenteredMomentUncenteredTerminal.comparisonScale line 24
3. lemma OAI.SevenEighths.CenteredMomentUncenteredTerminal.comparisonScale_pos line 26
4. lemma OAI.SevenEighths.CenteredMomentUncenteredTerminal.comparison_product line 31
5. theorem OAI.SevenEighths.CenteredMomentUncenteredTerminal.comparison_first_zero line 35
6. theorem OAI.SevenEighths.CenteredMomentUncenteredTerminal.profileCoefficient_eq_uncentered line 54
7. theorem OAI.SevenEighths.CenteredMomentUncenteredTerminal.smooth_subset_uncentered_absolute_energy line 66
8. theorem OAI.SevenEighths.CenteredMomentUncenteredTerminal.actual_small_width_uncentered_energy line 100