OAI/Probability/SwitchChain/FiniteObservableGeometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.FiniteObservableGeometry.probabilityVector line 12
  2. lemma OAI.Problem315.FiniteObservableGeometry.inner_probabilityVector line 15
  3. def OAI.Problem315.FiniteObservableGeometry.observable line 26
  4. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_observable line 29
  5. lemma OAI.Problem315.FiniteObservableGeometry.observable_probabilityVector line 38
  6. lemma OAI.Problem315.FiniteObservableGeometry.inner_eq_observable_average line 47
  7. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_add line 52
  8. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_sub line 57
  9. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_smul line 62
  10. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_mem line 67
  11. lemma OAI.Problem315.FiniteObservableGeometry.expectation_probabilityVector line 75
  12. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_indicator line 83
  13. lemma OAI.Problem315.FiniteObservableGeometry.probabilityVector_one line 86
  14. lemma OAI.Problem315.FiniteObservableGeometry.normalizedFlag_eq_probabilityVector line 91
  15. lemma OAI.Problem315.FiniteObservableGeometry.observable_constantVector line 103
  16. lemma OAI.Problem315.FiniteObservableGeometry.observable_eventVector line 107
  17. lemma OAI.Problem315.FiniteObservableGeometry.observable_normalizedFlag line 111
  18. lemma OAI.Problem315.FiniteObservableGeometry.expectation_constantVector line 118
  19. lemma OAI.Problem315.FiniteObservableGeometry.expectation_eventVector line 123
  20. lemma OAI.Problem315.FiniteObservableGeometry.expectation_normalizedFlag line 130