OAI/NumberTheory/DirichletL/Moments/FirstActiveRadicalBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.active_exponent_budget line 18
2. theorem OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.radical_squared_active_dvd line 23
3. theorem OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.radical_active_norm line 43
4. theorem OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.active_root_le_radical line 54
5. theorem OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.actual_first_weighted_mass line 66
6. theorem OAI.SevenEighths.CenteredMomentFirstActiveRadicalBudget.original_first_weighted_mass line 87