OAI/NumberTheory/DirichletL/Moments/Cauchy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentCauchy.bounded_row_cauchy line 11
2. def OAI.SevenEighths.CenteredMomentCauchy.leftColumn line 23
3. def OAI.SevenEighths.CenteredMomentCauchy.rightColumn line 27
4. lemma OAI.SevenEighths.CenteredMomentCauchy.paired_columns_integrable line 31
5. theorem OAI.SevenEighths.CenteredMomentCauchy.common_density_cauchy line 49
6. theorem OAI.SevenEighths.CenteredMomentCauchy.whole_kernel_row_estimate line 99