OAI/NumberTheory/DirichletL/Moments/NaturalRowSourceFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow line 14
2. def OAI.SevenEighths.CenteredMomentNaturalRowSource.naturalRow line 19
3. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.ideal line 24
4. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.element_zero line 28
5. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.masked_element line 36
6. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.masked_ideal line 45
7. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.masked_element_span line 52
8. theorem OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.nonprincipal line 61
9. def OAI.SevenEighths.CenteredMomentNaturalRowSource.fixedConductorFactor line 73
10. lemma OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.natural_modulus_bound line 75
11. theorem OAI.SevenEighths.CenteredMomentNaturalRowSource.NaturalRow.modulus_power_bound line 80