OAI/Analysis/Cotype/WalshDuality.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.average_norm_mul_le line 14
  2. def OAI.Cotype.dualPairing line 30
  3. theorem OAI.Cotype.dualPairing_bound line 33
  4. theorem OAI.Cotype.cubeL2_norms line 45
  5. theorem OAI.Cotype.exists_dualPairing_norming line 48
  6. def OAI.Cotype.walshBilinear line 76
  7. theorem OAI.Cotype.walshBilinear_eq_pairing line 80
  8. theorem OAI.Cotype.walshBilinear_bound line 86
  9. def OAI.Cotype.walshBilinearOutputs line 93
  10. theorem OAI.Cotype.walshBilinearOutputs_zero line 97
  11. theorem OAI.Cotype.walshBilinear_unit_bound line 102
  12. theorem OAI.Cotype.walshNorm_eq_bilinear line 111
  13. theorem OAI.Cotype.exists_walshBilinear_half line 127