OAI/NumberTheory/DirichletL/Moments/AmplificationRadicalFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.radicalBound line 28
2. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.radicalBound_error_power line 32
3. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.exists_radical_row line 45
4. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.exists_radical_height line 62
5. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.exists_radical_family line 80
6. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.exists_actual_error_family line 102
7. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.original_errors_to_children line 124
8. theorem OAI.SevenEighths.CenteredMomentAmplificationRadicalFamily.exists_original_error_ball_family line 200