OAI/NumberTheory/DirichletL/Moments/UniformReflectionProfile.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentUniformReflectionProfile.source_separation line 14
2. theorem OAI.SevenEighths.CenteredMomentUniformReflectionProfile.actual_one_uniform line 38
3. lemma OAI.SevenEighths.CenteredMomentUniformReflectionProfile.inverse_annular_frequency line 93
4. theorem OAI.SevenEighths.CenteredMomentUniformReflectionProfile.actual_inverse_uniform line 111
5. lemma OAI.SevenEighths.CenteredMomentUniformReflectionProfile.paperRadialFourier_real_smul line 134
6. lemma OAI.SevenEighths.CenteredMomentUniformReflectionProfile.polynomial_const_mul line 139
7. lemma OAI.SevenEighths.CenteredMomentUniformReflectionProfile.reflected_polynomial_real_smul line 152
8. theorem OAI.SevenEighths.CenteredMomentUniformReflectionProfile.detector_source_control line 165
9. theorem OAI.SevenEighths.CenteredMomentUniformReflectionProfile.detector_inverse_uniform line 177