OAI/Analysis/Cotype/WalshMonotonicity.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.operatorWalsh_joinline 10 - theorem
OAI.Cotype.operatorWalsh_add_leline 17 - theorem
OAI.Cotype.walshNorm_add_leline 47 - theorem
OAI.Cotype.walshNorm_antitoneline 51