OAI/Analysis/Cotype/Damping.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.xorCube line 11
  2. theorem OAI.Cotype.sign_xor line 13
  3. theorem OAI.Cotype.character_xor line 17
  4. def OAI.Cotype.setIndex line 25
  5. theorem OAI.Cotype.character_setIndex line 27
  6. theorem OAI.Cotype.character_rectangle line 31
  7. def OAI.Cotype.rowCube line 39
  8. def OAI.Cotype.columnCube line 41
  9. theorem OAI.Cotype.character_rectangle_row line 43
  10. theorem OAI.Cotype.character_rectangle_column line 52
  11. theorem OAI.Cotype.biasedExpectation_setIndex line 61
  12. theorem OAI.Cotype.biasedExpectation_rectangle line 66
  13. def OAI.Cotype.dampedSample line 75
  14. def OAI.Cotype.dampedExpectation line 78
  15. theorem OAI.Cotype.dampedExpectation_bound line 82
  16. theorem OAI.Cotype.dampedExpectation_odd_rectangle line 91
  17. theorem OAI.Cotype.dampedExpectation_fourier line 101