OAI/Combinatorics/Ryser/Probability/Variance.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.FiniteLaw.variance line 15
  2. def OAI.RyserCoveringCounterexample.FiniteLaw.covariance line 18
  3. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_nonneg line 22
  4. theorem OAI.RyserCoveringCounterexample.FiniteLaw.covariance_self line 26
  5. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_add_sq_mean_sub_eq line 30
  6. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_eq_expectation_sq_sub_sq line 48
  7. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_le_expectation_sub_const_sq line 54
  8. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_le_expectation_sq line 60
  9. theorem OAI.RyserCoveringCounterexample.FiniteLaw.covariance_eq_expectation_mul_sub_mul line 64
  10. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_add line 82
  11. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_add_of_covariance_zero line 98
  12. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_add_le line 104
  13. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_finset_sum line 126
  14. theorem OAI.RyserCoveringCounterexample.FiniteLaw.covariance_finset_sum_left line 133
  15. theorem OAI.RyserCoveringCounterexample.FiniteLaw.covariance_finset_sum_right line 143
  16. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_sum_le line 153
  17. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_sum_of_pairwise_covariance_zero line 172
  18. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_sum_of_pairwise_expectation_mul line 191
  19. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_le_sq_of_bounds line 202
  20. theorem OAI.RyserCoveringCounterexample.FiniteLaw.chebyshev line 212
  21. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_gt_mean_bound_add_le line 225
  22. theorem OAI.RyserCoveringCounterexample.FiniteLaw.variance_le_sq_mul_prob_of_anchor line 238