OAI/NumberTheory/DirichletL/Moments/FirstReferenceEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.supported line 29
2. def OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.ColumnBounds line 33
3. def OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.pairedBudget line 53
4. lemma OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.pairedBudget_nonneg line 55
5. def OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.sourceFactor line 59
6. lemma OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.sourceFactor_nonneg line 62
7. theorem OAI.SevenEighths.CenteredMomentFirstReferenceEnergy.actual_physical_mass line 69