OAI/NumberTheory/DirichletL/Moments/Primitive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentPrimitive.primitiveCharacter line 12
2. theorem OAI.SevenEighths.CenteredMomentPrimitive.primitiveCharacter_apply line 20
3. theorem OAI.SevenEighths.CenteredMomentPrimitive.primitiveCharacter_mk line 27
4. theorem OAI.SevenEighths.CenteredMomentPrimitive.primitive_gauss_transform line 36
5. lemma OAI.SevenEighths.CenteredMomentPrimitive.sqrt_absNorm line 56
6. theorem OAI.SevenEighths.CenteredMomentPrimitive.normalized_primitive_gauss_norm_le_one line 60