OAI/NumberTheory/DirichletL/Moments/UniformReflectionApproximation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.discarded_bound line 16
2. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.discarded_negligible line 39
3. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.deleted_discarded_negligible line 77
4. def OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.retainedSchwartz line 107
5. def OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.discardedSchwartz line 113
6. lemma OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.retainedSchwartz_eq line 119
7. lemma OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.restoration_summable line 137
8. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.original_split line 163
9. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.actual_original_approximation line 175
10. lemma OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.retainedSchwartz_uniformTwisted line 207
11. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.actual_twisted_approximation line 219
12. theorem OAI.SevenEighths.CenteredMomentUniformReflectionApproximation.detector_original_approximation line 249