OAI/NumberTheory/DirichletL/Moments/OriginalRadialComparison.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CenteredMomentOriginalRadialComparison.radialEnergyline 15 - lemma
OAI.SevenEighths.CenteredMomentOriginalRadialComparison.sqrt_weightline 18 - lemma
OAI.SevenEighths.CenteredMomentOriginalRadialComparison.finite_weightedline 23 - theorem
OAI.SevenEighths.CenteredMomentOriginalRadialComparison.actual_original_radial_comparisonline 31