OAI/Combinatorics/SumProduct/Alignment/BracketDrift01.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BracketDrift.small_drift_alternative line 27
2. lemma OAI.BracketDrift.circle_sum line 231
3. lemma OAI.BracketDrift.circle_int_mul line 238
4. lemma OAI.BracketDrift.circle_integer line 242
5. lemma OAI.BracketDrift.circle_dot_congr line 246
6. lemma OAI.BracketDrift.snoc_norm_le line 255
7. lemma OAI.BracketDrift.finite_frequency_bound line 263
8. theorem OAI.BracketDrift.arbitrary_drift_alternative line 278