OAI/Analysis/Cotype/ScalarWalsh.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.cubeL2_nonneg line 12
2. theorem OAI.Cotype.cubeL2_sq line 16
3. def OAI.Cotype.scalarWalsh line 22
4. theorem OAI.Cotype.scalarWalsh_twice line 24
5. theorem OAI.Cotype.scalarWalsh_L2_sq line 33
6. theorem OAI.Cotype.scalarWalsh_L2 line 40
7. theorem OAI.Cotype.scalar_rademacher_pairing line 45
8. theorem OAI.Cotype.scalar_rademacher_L2_sq line 64