OAI/NumberTheory/DirichletL/Moments/FirstInactiveRadicalMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstInactiveRadicalMass.inactiveWeight line 19
2. lemma OAI.SevenEighths.CenteredMomentFirstInactiveRadicalMass.inactiveWeight_nonneg line 23
3. lemma OAI.SevenEighths.CenteredMomentFirstInactiveRadicalMass.inactiveWeight_le_one line 28
4. theorem OAI.SevenEighths.CenteredMomentFirstInactiveRadicalMass.actual_inactive_radical_mass line 41
5. theorem OAI.SevenEighths.CenteredMomentFirstInactiveRadicalMass.original_input_inactive_radical_mass line 64