OAI/Probability/RandomSAT/Binomial.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Finite Bernoulli-count expectations and integrated telescoping estimates.

  1. def OAI.FixedClauseThreshold.binomialMean line 17
  2. theorem OAI.FixedClauseThreshold.binomialMean_congr line 22
  3. theorem OAI.FixedClauseThreshold.binomialMean_const line 30
  4. theorem OAI.FixedClauseThreshold.binomialMean_add line 35
  5. theorem OAI.FixedClauseThreshold.binomialMean_sub line 41
  6. theorem OAI.FixedClauseThreshold.binomialMean_mul_const line 47
  7. theorem OAI.FixedClauseThreshold.binomialMean_const_mul line 53
  8. theorem OAI.FixedClauseThreshold.binomialMean_sum line 57
  9. theorem OAI.FixedClauseThreshold.binomialMean_mono line 64
  10. theorem OAI.FixedClauseThreshold.binomialMean_nonneg line 73
  11. theorem OAI.FixedClauseThreshold.binomialMean_id line 77
  12. theorem OAI.FixedClauseThreshold.binomialMean_monotone_trials line 86
  13. theorem OAI.FixedClauseThreshold.uniformMean_binomialMean line 95
  14. theorem OAI.FixedClauseThreshold.sum_shift_difference_le line 104
  15. theorem OAI.FixedClauseThreshold.sum_two_shift_difference_le line 125
  16. def OAI.FixedClauseThreshold.replacementDifference line 142
  17. theorem OAI.FixedClauseThreshold.replacementDifference_mono line 145
  18. theorem OAI.FixedClauseThreshold.replacementDifference_sum_le line 152
  19. theorem OAI.FixedClauseThreshold.binomial_replacement_sum_le line 162