OAI/NumberTheory/DirichletL/Moments/HeckeCancellation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CenteredMomentHeckeCancellation.idealSumline 13 - def
OAI.SevenEighths.CenteredMomentHeckeCancellation.volumeControlline 16 - def
OAI.SevenEighths.CenteredMomentHeckeCancellation.densityControlline 19 - lemma
OAI.SevenEighths.CenteredMomentHeckeCancellation.volumeControl_nonnegline 22 - lemma
OAI.SevenEighths.CenteredMomentHeckeCancellation.densityControl_nonnegline 25 - theorem
OAI.SevenEighths.CenteredMomentHeckeCancellation.actual_rectangle_savingline 29