OAI/Probability/SwitchChain/CrossCovariance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CrossCovariance.jointMoment line 12
  2. def OAI.Problem315.CrossCovariance.mass line 16
  3. def OAI.Problem315.CrossCovariance.jointAverage line 19
  4. theorem OAI.Problem315.CrossCovariance.jointMoment_eq line 23
  5. theorem OAI.Problem315.CrossCovariance.mass_eq line 43
  6. theorem OAI.Problem315.CrossCovariance.covariance_rank_one line 49
  7. def OAI.Problem315.CrossCovariance.rightSliceAverage line 69
  8. theorem OAI.Problem315.CrossCovariance.rightSliceAverage_eq line 72
  9. theorem OAI.Problem315.CrossCovariance.rightSliceAverage_span line 94
  10. theorem OAI.Problem315.CrossCovariance.offCenter_jointMoment_zero line 102
  11. theorem OAI.Problem315.CrossCovariance.offCenter_covariance line 113