OAI/Combinatorics/SumProduct/Alignment/AllLevel10.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComparableBoxLeibman.halfOpen_bounds_scaled line 25
2. lemma OAI.ComparableBoxLeibman.affine_bounds_scaled line 47
3. lemma OAI.GlobalPointLaw.cell_expect_rectangle line 103
4. lemma OAI.GlobalPointLaw.cell_expect_progression line 146
5. lemma OAI.GlobalPointLaw.floor_rectangle_bounds line 155
6. def OAI.AllLevelFactorization.Factorization.ResidueCover.pointImage line 190
7. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointImage_continuous line 194
8. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointImage_cubePoint line 199
9. def OAI.AllLevelFactorization.Factorization.ResidueCover.pointHaar line 210
10. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointHaar_integral line 213
11. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.structured_local_haar line 221