OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PhaseSubInt.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryAdditiveBilinear.phase_sub_int line 25
2. lemma OAI.OrdinaryAdditiveBilinear.phase_chord_bound line 30
3. lemma OAI.OrdinaryAdditiveBilinear.rational_integer_separation line 57
4. lemma OAI.OrdinaryAdditiveBilinear.near_rational_phase_gap line 75
5. theorem OAI.OrdinaryAdditiveBilinear.resonant_truncated_energy line 103
6. theorem OAI.OrdinaryAdditiveBilinear.resonant_weighted_packet line 166
7. theorem OAI.OrdinaryAdditiveBilinear.near_rational_weighted_packet line 206