OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/VerticalSeries.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.PretentiousEuler.verticalSeries line 16
2. lemma OAI.OrdinaryCorrelations.PretentiousEuler.cutoff_power_lower line 21
3. lemma OAI.OrdinaryCorrelations.PretentiousEuler.weighted_distance_lower line 29
4. theorem OAI.OrdinaryCorrelations.PretentiousEuler.vertical_series_norm_le line 59
5. theorem OAI.OrdinaryCorrelations.PretentiousEuler.compact_vertical_saving line 87