OAI/Analysis/Cotype/FiniteRankWalsh.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.cubeL2_smul_const line 12
2. theorem OAI.Cotype.vectorWalsh_smul_const line 19
3. theorem OAI.Cotype.vectorWalsh_finset_sum line 26
4. theorem OAI.Cotype.finiteRank_expansion line 32
5. theorem OAI.Cotype.operatorWalsh_expansion line 47
6. theorem OAI.Cotype.finite_expansion_Walsh_bound line 56
7. theorem OAI.Cotype.finiteRank_Walsh_decay line 77