OAI/Probability/ClassicalON/PlanarAlgebra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.planarCharacter line 12
  2. def OAI.ClassicalON.planarCos line 14
  3. def OAI.ClassicalON.planarSin line 16
  4. theorem OAI.ClassicalON.continuous_planarCos line 18
  5. theorem OAI.ClassicalON.continuous_planarSin line 22
  6. theorem OAI.ClassicalON.planarCharacter_add line 26
  7. theorem OAI.ClassicalON.planarCharacter_neg line 30
  8. theorem OAI.ClassicalON.planarCos_add_sub line 34
  9. theorem OAI.ClassicalON.planarCos_subtraction line 40
  10. def OAI.ClassicalON.planarEnergy line 48
  11. def OAI.ClassicalON.planarSine line 51
  12. theorem OAI.ClassicalON.continuous_planarEnergy line 54
  13. theorem OAI.ClassicalON.continuous_planarSine line 58
  14. theorem OAI.ClassicalON.planarEnergy_double_sum line 62
  15. theorem OAI.ClassicalON.planarEnergy_double_sub line 75