OAI/NumberTheory/DirichletL/Moments/ReflectionTailMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentReflectionTailMass.subset_norm_le line 13
2. lemma OAI.SevenEighths.CenteredMomentReflectionTailMass.restoration_norm_one line 19
3. lemma OAI.SevenEighths.CenteredMomentReflectionTailMass.dual_scale_bounds line 23
4. theorem OAI.SevenEighths.CenteredMomentReflectionTailMass.coefficient_column_bound line 39
5. theorem OAI.SevenEighths.CenteredMomentReflectionTailMass.actual_deleted_discarded_negligible line 73