OAI/NumberTheory/DirichletL/Moments/CommonAllowance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCommonAllowance.activeIndicator line 12
2. theorem OAI.SevenEighths.CenteredMomentCommonAllowance.netExponent_self line 14
3. theorem OAI.SevenEighths.CenteredMomentCommonAllowance.local_allowance line 19
4. theorem OAI.SevenEighths.CenteredMomentCommonAllowance.weighted_positive_part line 39
5. theorem OAI.SevenEighths.CenteredMomentCommonAllowance.weighted_allowance line 46
6. theorem OAI.SevenEighths.CenteredMomentCommonAllowance.actual_common_support_allowance line 65