OAI/NumberTheory/DirichletL/Moments/UniformRetainedEnergy.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.CenteredMomentUniformRetainedEnergy.twisted_zeroline 17 - lemma
OAI.SevenEighths.CenteredMomentUniformRetainedEnergy.normalized_zeroline 21 - lemma
OAI.SevenEighths.CenteredMomentUniformRetainedEnergy.retained_zeroline 29 - theorem
OAI.SevenEighths.CenteredMomentUniformRetainedEnergy.actual_retained_uniform_energyline 34