OAI/NumberTheory/DirichletL/Moments/FirstAmplifiedPaidAdmission.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.sourceReserve line 34
2. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.sourceReserve_nonneg line 42
3. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.common_affine line 46
4. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.actual_main_admission line 54
5. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.actual_active_error_admission line 129
6. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.actual_width_admission line 213
7. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedPaidAdmission.common_preVolume_height line 225