OAI/Combinatorics/SumProduct/Alignment/ComparableBox01.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CorrectedBoxLeibman.corrected_box_leibman_binomial line 44
2. def OAI.ComparableBoxLeibman.rectMean line 122
3. lemma OAI.ComparableBoxLeibman.rectMean_eq_fin line 126
4. lemma OAI.ComparableBoxLeibman.rectMean_const line 147
5. lemma OAI.ComparableBoxLeibman.rectMean_sub line 153
6. lemma OAI.ComparableBoxLeibman.rectMean_norm_le line 157
7. lemma OAI.ComparableBoxLeibman.rectMean_norm_sub_le line 166
8. lemma OAI.ComparableBoxLeibman.rectMean_exists_norm_ge line 173
9. lemma OAI.ComparableBoxLeibman.rectMean_shift line 186
10. lemma OAI.ComparableBoxLeibman.rectMean_boxMean_comm line 209
11. lemma OAI.ComparableBoxLeibman.rectMean_cube_smoothing line 218
12. lemma OAI.ComparableBoxLeibman.rectMean_bad_cube line 242
13. lemma OAI.ComparableBoxLeibman.choose_rectangle_scale line 262