OAI/Combinatorics/SumProduct/Alignment/CorrectedBox07.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CorrectedBoxLeibman.gridEval_integer_injective line 26
2. theorem OAI.ComparableBoxLeibman.haar_limit_of_horizontal_irrationality line 85
3. lemma OAI.CorrectedBoxLeibman.gridEval_mul line 150
4. lemma OAI.CorrectedBoxLeibman.gridTranslate_mul line 154
5. lemma OAI.CorrectedBoxLeibman.gridTranslate_cancel line 159
6. def OAI.CorrectedBoxLeibman.gridDilate line 169
7. lemma OAI.CorrectedBoxLeibman.gridDilate_eval line 172
8. lemma OAI.CorrectedBoxLeibman.gridAffine_unique line 180
9. theorem OAI.CorrectedBoxLeibman.gridAffine_recover_bound line 194
10. theorem OAI.ComparableBoxLeibman.haar_limit_fixed_progression line 260