OAI/Analysis/Cotype/WalshMainEstimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.operatorWalsh_comp_left line 13
2. theorem OAI.Cotype.operatorWalsh_comp_right line 18
3. theorem OAI.Cotype.walshNorm_comp_left line 21
4. theorem OAI.Cotype.walshNorm_comp_right line 30
5. theorem OAI.Cotype.compactMap_walsh_bound line 39
6. theorem OAI.Cotype.walshNorm_identity_ge_of_l1_family line 60
7. theorem OAI.Cotype.no_uniform_l1_of_walsh_decay line 78