OAI/NumberTheory/DirichletL/Hecke/InverseAmplificationBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeInverseAmplification.amplificationPower line 9
2. def OAI.SevenEighths.HeckeInverseAmplification.sourceExponent line 10
3. theorem OAI.SevenEighths.HeckeInverseAmplification.amplificationPower_nonneg line 12
4. theorem OAI.SevenEighths.HeckeInverseAmplification.amplificationPower_upper line 14
5. theorem OAI.SevenEighths.HeckeInverseAmplification.amplified_exponent line 20
6. theorem OAI.SevenEighths.HeckeInverseAmplification.amplified_exponent_le line 29
7. theorem OAI.SevenEighths.HeckeInverseAmplification.exists_amplification_budget line 41
8. theorem OAI.SevenEighths.HeckeInverseAmplification.logarithmic_cost_eventually line 62