OAI/Combinatorics/SumProduct/Alignment/AllLevel08.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComparableBoxLeibman.halfOpen_bounds_scaled_uniform line 26
2. lemma OAI.ComparableBoxLeibman.affine_bounds_scaled_uniform line 50
3. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.local_halfOpen_uniform line 114
4. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.local_physical_uniform line 139
5. def OAI.AllLevelFactorization.Factorization.ResidueCover.cubeHaar line 185
6. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.integral_cubeHaar line 191
7. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.local_physical_compact line 198
8. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.source_physical_cube_law line 232