OAI/NumberTheory/DirichletL/Hecke/InverseAmplificationConjugation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeInverseAmplification.coefficient_inverse_conj line 13
2. theorem OAI.SevenEighths.HeckeInverseAmplification.conj_positive_cpow line 17
3. theorem OAI.SevenEighths.HeckeInverseAmplification.conj_shift line 23
4. theorem OAI.SevenEighths.HeckeInverseAmplification.conj_polynomial line 27
5. theorem OAI.SevenEighths.HeckeInverseAmplification.polynomial_inverse_norm line 42
6. theorem OAI.SevenEighths.HeckeInverseAmplification.conjugate_profile_support line 48
7. theorem OAI.SevenEighths.HeckeInverseAmplification.conjugate_profile_smooth line 53
8. theorem OAI.SevenEighths.HeckeInverseAmplification.scaleProfile_conjugate line 57
9. theorem OAI.SevenEighths.HeckeInverseAmplification.logProfile_conjugate line 63