OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/TwistNormLe.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.PretentiousStability.twist_norm_le line 24
2. lemma OAI.OrdinaryCorrelations.PretentiousStability.summand_nonneg line 32
3. lemma OAI.OrdinaryCorrelations.PretentiousStability.distanceSq_nonneg line 42
4. lemma OAI.OrdinaryCorrelations.PretentiousStability.sq_distance line 47
5. lemma OAI.OrdinaryCorrelations.PretentiousStability.summand_difference line 51
6. theorem OAI.OrdinaryCorrelations.PretentiousStability.distanceSq_change line 75
7. theorem OAI.OrdinaryCorrelations.PretentiousStability.uniformlyNonpretentious_change line 99