OAI/NumberTheory/DirichletL/Detector/LowGramFixedCoefficient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.gramFixedModulus line 12
2. lemma OAI.SevenEighths.ProbePhysical.gramFixedModulus_nonzero line 17
3. def OAI.SevenEighths.ProbePhysical.gramCoefficientExtension line 24
4. lemma OAI.SevenEighths.ProbePhysical.gramCoefficientExtension_norm line 29
5. lemma OAI.SevenEighths.ProbePhysical.gramCoefficientExtension_zero line 37
6. theorem OAI.SevenEighths.ProbePhysical.lowGramCoefficient_eq_extension line 44
7. theorem OAI.SevenEighths.ProbePhysical.gramCoefficientExtension_periodic line 52
8. lemma OAI.SevenEighths.ProbePhysical.gramCoefficientExtension_scaled_periodic line 60