OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/NormPhase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryLocalAdditive.phase line 24
2. lemma OAI.OrdinaryLocalAdditive.norm_phase line 25
3. lemma OAI.OrdinaryLocalAdditive.phase_add line 26
4. lemma OAI.OrdinaryLocalAdditive.phase_int line 32
5. lemma OAI.OrdinaryLocalAdditive.phase_sub_le line 37
6. lemma OAI.OrdinaryLocalAdditive.phase_rational_mod line 48
7. theorem OAI.OrdinaryLocalAdditive.rational_windowSmall line 60
8. lemma OAI.OrdinaryLocalAdditive.phase_inside_window line 69
9. lemma OAI.OrdinaryLocalAdditive.sharp_phase_pointwise line 78
10. lemma OAI.OrdinaryLocalAdditive.sharp_phase_l1 line 112