OAI/NumberTheory/DirichletL/Moments/RetainedWeightedSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.CenteredMomentRetainedWeightedSource.sourcePrimes line 18
2. def OAI.SevenEighths.CenteredMomentRetainedWeightedSource.dualScale line 20
3. lemma OAI.SevenEighths.CenteredMomentRetainedWeightedSource.dualScale_pos line 24
4. def OAI.SevenEighths.CenteredMomentRetainedWeightedSource.retainedColumn line 35
5. lemma OAI.SevenEighths.CenteredMomentRetainedWeightedSource.retainedColumn_zero line 44
6. theorem OAI.SevenEighths.CenteredMomentRetainedWeightedSource.finiteAnnularColumn_normalized line 51
7. theorem OAI.SevenEighths.CenteredMomentRetainedWeightedSource.retainedOriginal_eq_weighted line 67
8. theorem OAI.SevenEighths.CenteredMomentRetainedWeightedSource.retainedOriginal_fiber_summable line 95
9. theorem OAI.SevenEighths.CenteredMomentRetainedWeightedSource.actual_retained_weighted_energy line 113