OAI/NumberTheory/DirichletL/Energy/CanonicalErrorPaid.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.castAllocation line 56
2. def OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.castDivisorAllocation line 60
3. def OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.restoreDivisorAllocation line 65
4. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.cast_child_energy line 70
5. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.restored_child_energy line 80
6. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.cast_preVolume line 91
7. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.cast_slot_sum line 99
8. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.restored_preVolume line 105
9. lemma OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.restored_slot_sum line 111
10. theorem OAI.SevenEighths.CenteredMomentEnergyCanonicalErrorPaid.actual_error_child_from_bands line 116