OAI/Analysis/Cotype/WalshNorm.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.walshOutputs line 11
  2. def OAI.Cotype.walshNorm line 14
  3. theorem OAI.Cotype.walshOutputs_zero line 16
  4. theorem OAI.Cotype.walshOutputs_bddAbove line 19
  5. theorem OAI.Cotype.walshNorm_nonneg line 24
  6. theorem OAI.Cotype.le_walshNorm line 27
  7. theorem OAI.Cotype.walshNorm_le line 31
  8. theorem OAI.Cotype.vectorWalsh_smul line 36
  9. theorem OAI.Cotype.operatorWalsh_smul line 45
  10. theorem OAI.Cotype.operatorWalsh_le_walshNorm line 50
  11. theorem OAI.Cotype.walshNorm_le_of_bound line 63
  12. theorem OAI.Cotype.walshNorm_lipschitz line 70
  13. theorem OAI.Cotype.finiteRank_walshNorm_decay line 85
  14. theorem OAI.Cotype.operatorWalsh_zero_const line 91
  15. theorem OAI.Cotype.walshNorm_zero line 96