OAI/Combinatorics/SumProduct/Alignment/ComparableBox02.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComparableBoxLeibman.rectMean_smul line 26
2. lemma OAI.ComparableBoxLeibman.normalized_rect_observable line 31
3. theorem OAI.ComparableBoxLeibman.comparable_integer_box line 91
4. def OAI.ComparableBoxLeibman.integerLength line 135
5. lemma OAI.ComparableBoxLeibman.integerCoord_bounds line 137
6. lemma OAI.ComparableBoxLeibman.integerCoord_exists line 147
7. def OAI.ComparableBoxLeibman.integerBox line 159
8. lemma OAI.ComparableBoxLeibman.mem_integerBox line 163
9. lemma OAI.ComparableBoxLeibman.integerBox_average line 174
10. lemma OAI.ComparableBoxLeibman.integerLength_lower line 185
11. theorem OAI.ComparableBoxLeibman.comparable_real_box line 232