OAI/NumberTheory/DirichletL/Moments/ChildEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentChildEnergy.leftColumn_eq_gaussPolynomial line 13
2. theorem OAI.SevenEighths.CenteredMomentChildEnergy.rightColumn_eq_star_gaussPolynomial line 23
3. theorem OAI.SevenEighths.CenteredMomentChildEnergy.whole_kernel_gauss_child_bound line 33