OAI/NumberTheory/DirichletL/Moments/FirstChildProfileControl.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstChildProfileControl.mass line 20
2. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.mass_one line 23
3. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.mass_nonneg line 27
4. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.child_mass line 30
5. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.child_card line 38
6. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.slot_control_bound line 43
7. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.profile_cost_bound line 62
8. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.exceptional_slot_bound line 75
9. theorem OAI.SevenEighths.CenteredMomentFirstChildProfileControl.twice_controls line 98
10. def OAI.SevenEighths.CenteredMomentFirstChildProfileControl.exceptionalConstant line 116
11. lemma OAI.SevenEighths.CenteredMomentFirstChildProfileControl.exceptional_factor_bound line 125
12. theorem OAI.SevenEighths.CenteredMomentFirstChildProfileControl.twice_exceptional_factor line 142