OAI/Probability/ClassicalON/FamilyKernel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.familyKernel line 14
  2. def OAI.ClassicalON.rowSquare line 16
  3. def OAI.ClassicalON.familyHSSquare line 18
  4. theorem OAI.ClassicalON.familyKernel_conj line 21
  5. theorem OAI.ClassicalON.rowSquare_nonneg line 25
  6. theorem OAI.ClassicalON.familyHSSquare_nonneg line 28
  7. theorem OAI.ClassicalON.kernel_diag_sq_le_row line 31
  8. theorem OAI.ClassicalON.kernel_diag_norm_le_sqrt line 35
  9. def OAI.ClassicalON.SpinSystem.coefficientObservable line 43
  10. def OAI.ClassicalON.SpinSystem.currentObservable line 49
  11. def OAI.ClassicalON.SpinSystem.conjugateObservable line 53
  12. theorem OAI.ClassicalON.SpinSystem.conjugateObservable_apply line 57
  13. theorem OAI.ClassicalON.SpinSystem.normObservable_conjugate line 61
  14. theorem OAI.ClassicalON.SpinSystem.currentObservable_conj line 67
  15. theorem OAI.ClassicalON.SpinSystem.coefficientObservable_conj line 74
  16. theorem OAI.ClassicalON.SpinSystem.familyKernel_differential line 81
  17. theorem OAI.ClassicalON.SpinSystem.row_current_moment line 87