OAI/Analysis/Cotype/VectorWalsh.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.cubeL2_eq_piLp line 14
  2. theorem OAI.Cotype.cubeL2_add_le line 22
  3. theorem OAI.Cotype.cubeL2_sum_le line 31
  4. theorem OAI.Cotype.cubeL2_smul line 40
  5. theorem OAI.Cotype.cubeL2_const line 49
  6. theorem OAI.Cotype.cubeL2_mono line 53
  7. theorem OAI.Cotype.cubeL2_bound line 60
  8. theorem OAI.Cotype.norm_average_le line 65
  9. theorem OAI.Cotype.average_norm_le_cubeL2 line 72
  10. theorem OAI.Cotype.cubeL2_clm line 85
  11. theorem OAI.Cotype.abs_character line 91
  12. def OAI.Cotype.vectorWalsh line 95
  13. def OAI.Cotype.operatorWalsh line 98
  14. theorem OAI.Cotype.vectorWalsh_bound line 101
  15. theorem OAI.Cotype.vectorWalsh_L2_le line 107
  16. theorem OAI.Cotype.operatorWalsh_L2_le line 111
  17. theorem OAI.Cotype.vectorWalsh_sub line 115
  18. theorem OAI.Cotype.operatorWalsh_sub line 120
  19. theorem OAI.Cotype.operatorWalsh_L2_lipschitz line 124