OAI/Probability/ThreeState/Expectations.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Expectations, second moments and the regular and Poisson offspring laws.

  1. def OAI.ThreeState.mean line 12
  2. def OAI.ThreeState.HasMean line 15
  3. lemma OAI.ThreeState.HasMean.abs line 18
  4. lemma OAI.ThreeState.HasMean.of_abs line 22
  5. lemma OAI.ThreeState.hasMean_const line 27
  6. lemma OAI.ThreeState.mean_const line 30
  7. lemma OAI.ThreeState.HasMean.add line 33
  8. lemma OAI.ThreeState.mean_add line 37
  9. lemma OAI.ThreeState.HasMean.mul_const line 41
  10. lemma OAI.ThreeState.mean_mul_const line 45
  11. lemma OAI.ThreeState.HasMean.const_mul line 49
  12. lemma OAI.ThreeState.mean_const_mul line 53
  13. lemma OAI.ThreeState.hasMean_of_square line 57
  14. lemma OAI.ThreeState.mass_pure line 64
  15. lemma OAI.ThreeState.mean_pure line 68
  16. lemma OAI.ThreeState.hasMean_pure line 72
  17. lemma OAI.ThreeState.mean_nonneg line 77
  18. lemma OAI.ThreeState.HasMean.bind line 80
  19. lemma OAI.ThreeState.mean_bind line 102
  20. lemma OAI.ThreeState.HasMean.map line 127
  21. lemma OAI.ThreeState.mean_map line 133
  22. lemma OAI.ThreeState.HasMean.mono line 143
  23. lemma OAI.ThreeState.mean_le line 148
  24. lemma OAI.ThreeState.mean_abs_le_one_add_square line 152
  25. lemma OAI.ThreeState.hasMean_bind_square line 159
  26. lemma OAI.ThreeState.hasMean_bind_abs_of_square line 166
  27. lemma OAI.ThreeState.mean_bind_of_square line 174
  28. lemma OAI.ThreeState.mean_bind_square line 180
  29. lemma OAI.ThreeState.HasMean.congr line 187
  30. lemma OAI.ThreeState.mean_congr line 191
  31. lemma OAI.ThreeState.hasMean_shift_square line 194
  32. lemma OAI.ThreeState.mean_shift_square line 199
  33. lemma OAI.ThreeState.hasMean_fintype line 207
  34. lemma OAI.ThreeState.mean_fintype line 210
  35. structure OAI.ThreeState.Moments line 215
  36. lemma OAI.ThreeState.Moments.hasMean line 220
  37. lemma OAI.ThreeState.Moments.map line 223
  38. lemma OAI.ThreeState.Moments.pure line 229
  39. lemma OAI.ThreeState.Moments.shift line 233
  40. lemma OAI.ThreeState.Moments.bind line 240
  41. lemma OAI.ThreeState.Moments.independent_add line 252
  42. lemma OAI.ThreeState.hasMean_bounded line 270
  43. lemma OAI.ThreeState.abs_mean_le line 274
  44. lemma OAI.ThreeState.mean_bind_bounded line 282
  45. lemma OAI.ThreeState.mean_map_bounded line 288
  46. def OAI.ThreeState.joint line 294
  47. lemma OAI.ThreeState.mean_joint_bounded line 297
  48. lemma OAI.ThreeState.mean_joint_fst line 305
  49. lemma OAI.ThreeState.mean_joint_snd line 311
  50. lemma OAI.ThreeState.HasMean.sub line 320
  51. lemma OAI.ThreeState.mean_sub line 324
  52. lemma OAI.ThreeState.poisson_mass line 329
  53. lemma OAI.ThreeState.poisson_mass_succ line 335
  54. lemma OAI.ThreeState.poisson_first_hasSum line 343
  55. lemma OAI.ThreeState.poisson_second_factorial_hasSum line 351
  56. theorem OAI.ThreeState.poisson_moments line 368
  57. lemma OAI.ThreeState.regular_moments line 378