OAI/NumberTheory/DirichletL/Moments/SecondExceptionalFamilyUniform.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.fixedExpandedCost line 17
2. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.fixedExpandedCost_pos line 20
3. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.expandedFactor_real line 31
4. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.expanded_real_bounds line 37
5. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.live_expanded_real_bounds line 60
6. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.eventually_uniform_live_caps line 84
7. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamilyUniform.exists_uniform_exceptional_family line 115