OAI/Probability/SwitchChain/CrossIndependent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CrossBlock.independentMargin line 11
  2. theorem OAI.Problem315.CrossBlock.count_eq_independent_product line 19
  3. def OAI.Problem315.CrossBlock.countMoment line 53
  4. def OAI.Problem315.CrossBlock.countAverage line 57
  5. theorem OAI.Problem315.CrossBlock.countMoment_factor line 61
  6. theorem OAI.Problem315.CrossBlock.countAverage_independent line 78
  7. theorem OAI.Problem315.CrossCovariance.independent_of_left_flag_constant line 97
  8. theorem OAI.Problem315.CrossCovariance.independent_of_right_flag_constant line 126
  9. theorem OAI.Problem315.CrossCovariance.independent_of_left_event_zero line 155
  10. theorem OAI.Problem315.CrossCovariance.jointMoment_swap line 193
  11. theorem OAI.Problem315.CrossCovariance.jointAverage_swap line 204
  12. theorem OAI.Problem315.CrossCovariance.independent_of_right_event_zero line 211
  13. theorem OAI.Problem315.CrossCovariance.independent_of_center_zero line 226