OAI/NumberTheory/DirichletL/Moments/SourceInputTailUniform.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSourceInputTailUniform.plainControl line 23
2. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.plainControl_nonneg line 27
3. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.volume_pos line 33
4. theorem OAI.SevenEighths.CenteredMomentSourceInputTailUniform.input_mass line 37
5. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.input_column_bound line 71
6. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.kernel_inverse_cap line 97
7. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.eventually_tail_threshold line 119
8. lemma OAI.SevenEighths.CenteredMomentSourceInputTailUniform.choose_tail_order line 130
9. theorem OAI.SevenEighths.CenteredMomentSourceInputTailUniform.second_input_tail_arbitrary_saving line 159