OAI/NumberTheory/DirichletL/Moments/ReflectedUniformPair.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentReflectedUniformPair.heightScale line 12
2. def OAI.SevenEighths.CenteredMomentReflectedUniformPair.normalizedReflected line 14
3. def OAI.SevenEighths.CenteredMomentReflectedUniformPair.envelope line 18
4. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.heightScale_pos line 20
5. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.envelope_pos line 24
6. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.envelope_weight line 28
7. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.envelope_integrable line 33
8. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.envelope_integral line 38
9. lemma OAI.SevenEighths.CenteredMomentReflectedUniformPair.normalized_density_bound line 43
10. theorem OAI.SevenEighths.CenteredMomentReflectedUniformPair.actual_pair_uniform line 61