OAI/NumberTheory/DirichletL/Moments/ReflectedProfileMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.actual_profile_separation line 15
2. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.row_density_energy line 49
3. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.row_density_energy_two line 83
4. def OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.logWindow line 104
5. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.finite_annular_separation line 106
6. lemma OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.logWindow_support line 164
7. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.plain_annular_separation line 177
8. theorem OAI.SevenEighths.CenteredMomentReflectedProfileMeasure.actual_plain_profile_measure line 197