OAI/Analysis/Cotype/WalshAmplification.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.l2AmplificationLinear line 13
  2. theorem OAI.Cotype.l2AmplificationLinear_bound line 20
  3. def OAI.Cotype.l2Amplification line 29
  4. theorem OAI.Cotype.l2Amplification_apply line 35
  5. theorem OAI.Cotype.cubeL2_piLp_sq line 39
  6. theorem OAI.Cotype.operatorWalsh_amplification_apply line 47
  7. theorem OAI.Cotype.operatorWalsh_amplification_bound line 54
  8. theorem OAI.Cotype.walshNorm_amplification_le line 69
  9. theorem OAI.Cotype.cubeL2_piLp_single line 74
  10. theorem OAI.Cotype.operatorWalsh_amplification_single line 78
  11. theorem OAI.Cotype.walshNorm_amplification line 91