OAI/NumberTheory/DirichletL/Energy/FirstAnnularAdmission.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_dyad_retained line 24
2. lemma OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_dyad_gt_one line 32
3. lemma OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_nominal_positive line 40
4. lemma OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_nominal_span line 50
5. def OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.amplifierCap line 57
6. theorem OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_amplifier_packet line 60
7. lemma OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.source_frequency_ledger line 97
8. theorem OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.fixed_endpoint_radius line 108
9. theorem OAI.SevenEighths.CenteredMomentEnergyFirstAnnularAdmission.eventually_source_admission line 119