OAI/NumberTheory/DirichletL/Moments/AmplificationLiveMask.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.CenteredMomentAmplificationLiveMask.profile_maskline 16 - theorem
OAI.SevenEighths.CenteredMomentAmplificationLiveMask.column_maskline 24 - def
OAI.SevenEighths.CenteredMomentAmplificationLiveMask.maskedLiveProfileline 38 - theorem
OAI.SevenEighths.CenteredMomentAmplificationLiveMask.original_masked_live_columnline 46