OAI/Combinatorics/SumProduct/Alignment/CubeLocal05.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedLipschitzCompact.compact_envelope line 27
2. theorem OAI.CubeLocalHaar.source_bounded_lipschitz_cube_haar line 91
3. def OAI.CubeLocalHaar.physicalProgressionBox line 157
4. lemma OAI.CubeLocalHaar.physicalProgressionBox_mem line 162
5. lemma OAI.CubeLocalHaar.physicalProgressionBox_affine line 169
6. theorem OAI.CubeLocalHaar.physicalProgressionBox_expect line 189
7. theorem OAI.CubeLocalHaar.source_physical_cube_haar line 260