OAI/Combinatorics/SumProduct/Alignment/CubeLocal09.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubeLocalHaar.source_comparable_boxes_cube_haar line 54
2. theorem OAI.CubeLocalHaar.imageProbability_continuous line 153
3. theorem OAI.CubeLocalHaar.haar_image_integral_continuous line 182
4. theorem OAI.CubeLocalHaar.haar_image_intervalIntegrable line 200
5. def OAI.CubeLocalHaar.physicalResidueRectangle line 222
6. lemma OAI.CubeLocalHaar.physicalResidueRectangle_mem line 226
7. lemma OAI.CubeLocalHaar.physicalResidueRectangle_affine line 232
8. theorem OAI.CubeLocalHaar.physicalResidueRectangle_expect line 250