OAI/NumberTheory/DirichletL/Moments/SecondBlockRadicalHarmonicMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.radicalWeight line 20
2. lemma OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.radicalWeight_nonneg line 22
3. lemma OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.active_mass_le_partition line 26
4. lemma OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.active_blocks_sum_eq line 46
5. theorem OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.actual_active_radical_mass line 54
6. theorem OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.actual_block_radical_mass line 74
7. theorem OAI.SevenEighths.CenteredMomentSecondBlockRadicalHarmonicMass.actual_original_block_radical_mass line 111