OAI/Combinatorics/SumProduct/Alignment/AllLevel06.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeTaylorExpansion.choose_cast_int line 28
2. lemma OAI.CubeTaylorExpansion.word_eq_list line 33
3. lemma OAI.CubeTaylorExpansion.taylorPolynomial_int line 42
4. lemma OAI.CubeTaylorExpansion.cubePolynomial_integer_vertex line 52
5. lemma OAI.AllLevelFactorization.Factorization.smoothLimit_continuous line 81
6. lemma OAI.AllLevelFactorization.Factorization.smooth_coord_uniform line 86
7. theorem OAI.AllLevelFactorization.Factorization.smooth_neighborhood line 103
8. theorem OAI.CompactTwoScale.freezing line 152
9. def OAI.EmbeddedCubeHaar.frozenTest line 192
10. lemma OAI.EmbeddedCubeHaar.frozenTest_continuous line 198
11. abbrev OAI.AllLevelFactorization.Factorization.ResidueCover.CubeGroup line 224
12. abbrev OAI.AllLevelFactorization.Factorization.ResidueCover.CubeSpace line 225
13. def OAI.AllLevelFactorization.Factorization.ResidueCover.cubePoint line 227
14. instance OAI.AllLevelFactorization.Factorization.ResidueCover.compact_cubeSpace line 232
15. def OAI.AllLevelFactorization.Factorization.ResidueCover.haar line 239
16. instance OAI.AllLevelFactorization.Factorization.ResidueCover.haar_invariant line 244
17. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.haar_limit line 251
18. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.two_scale line 269