OAI/NumberTheory/DirichletL/Moments/SecondWindowBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSecondWindowBudget.profileMoment line 13
2. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.profileMoment_nonneg line 16
3. def OAI.SevenEighths.CenteredMomentSecondWindowBudget.heightEnvelope line 19
4. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.heightEnvelope_pos line 21
5. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.heightCost_le_envelope line 23
6. def OAI.SevenEighths.CenteredMomentSecondWindowBudget.windowBudget line 29
7. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.windowBudget_nonneg line 31
8. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.shifted_window_budget line 35
9. theorem OAI.SevenEighths.CenteredMomentSecondWindowBudget.conjugate_shifted_window_budget line 49