OAI/Probability/SwitchChain/FiniteEventVectors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.FiniteEventVectors.probability line 13
  2. def OAI.Problem315.FiniteEventVectors.rawIndicator line 15
  3. def OAI.Problem315.FiniteEventVectors.eventVector line 18
  4. def OAI.Problem315.FiniteEventVectors.constantVector line 21
  5. theorem OAI.Problem315.FiniteEventVectors.inner_rawIndicator_right line 23
  6. theorem OAI.Problem315.FiniteEventVectors.inner_eventVector_right line 32
  7. theorem OAI.Problem315.FiniteEventVectors.inner_constantVector_right line 37
  8. theorem OAI.Problem315.FiniteEventVectors.inner_normalizedFlag_right line 41
  9. theorem OAI.Problem315.FiniteEventVectors.inner_rawIndicator line 51
  10. theorem OAI.Problem315.FiniteEventVectors.inner_eventVector line 66
  11. theorem OAI.Problem315.FiniteEventVectors.inner_eventVector_self line 77
  12. theorem OAI.Problem315.FiniteEventVectors.inner_eventVector_constant line 81
  13. theorem OAI.Problem315.FiniteEventVectors.inner_constantVector_self line 85
  14. theorem OAI.Problem315.FiniteEventVectors.inner_eventVector_of_disjoint line 91
  15. theorem OAI.Problem315.FiniteEventVectors.probability_pos line 97
  16. theorem OAI.Problem315.FiniteEventVectors.probability_add_lt_one line 106
  17. theorem OAI.Problem315.FiniteEventVectors.normalized_events_gram line 126