OAI/Combinatorics/SumProduct/Alignment/CubeLocal02.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteHaarTests.two_scale_freezing line 30
2. theorem OAI.CubeLocalHaar.two_scale_cube_haar line 97
3. theorem OAI.CubeLocalHaar.smooth_local_freezing line 160
4. lemma OAI.CubeLocalHaar.normalized_vertex_close line 191
5. theorem OAI.CubeLocalHaar.smooth_two_scale_cube_haar line 241