OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrincipalDivergence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.UniformFamilyHalasz.PrincipalDivergence line 30
2. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.eventual_band_saving line 34
3. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_compact_weighted_small line 62
4. lemma OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_compact_unweighted_small line 136
5. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_global_derivative_small line 171
6. lemma OAI.OrdinaryCorrelations.UniformFamilyHalasz.square_bounded_logSeries_cauchy_derivative line 224
7. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_logcutoff_small line 238
8. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_cutoff_small line 278
9. theorem OAI.OrdinaryCorrelations.UniformFamilyHalasz.moving_square_complete_partial_small line 318