OAI/NumberTheory/DirichletL/Energy/CanonicalAnnularLower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.parent_lower_ge line 20
2. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.exceptional_cap_antitone line 28
3. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.main_powers_antitone line 34
4. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.error_powers_antitone line 41
5. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.source_coefficients_mono line 48
6. theorem OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.actual_source_coefficients_lower line 67
7. theorem OAI.SevenEighths.CenteredMomentEnergyCanonicalAnnularLower.actual_high_annular_sum line 97