OAI/Probability/RandomSAT/FiniteMean.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite expectations and variances.

  1. def OAI.FixedClauseThreshold.uniformMean line 17
  2. theorem OAI.FixedClauseThreshold.uniformMean_congr line 20
  3. theorem OAI.FixedClauseThreshold.uniformMean_const line 26
  4. theorem OAI.FixedClauseThreshold.uniformMean_zero line 31
  5. theorem OAI.FixedClauseThreshold.uniformMean_add line 35
  6. theorem OAI.FixedClauseThreshold.uniformMean_sub line 39
  7. theorem OAI.FixedClauseThreshold.uniformMean_mul_const line 43
  8. theorem OAI.FixedClauseThreshold.uniformMean_const_mul line 48
  9. theorem OAI.FixedClauseThreshold.uniformMean_sum line 53
  10. theorem OAI.FixedClauseThreshold.uniformMean_nonneg line 58
  11. theorem OAI.FixedClauseThreshold.uniformMean_mono line 62
  12. theorem OAI.FixedClauseThreshold.uniformMean_equiv line 66
  13. theorem OAI.FixedClauseThreshold.uniformMean_prod line 71
  14. theorem OAI.FixedClauseThreshold.uniformMean_comm line 77
  15. theorem OAI.FixedClauseThreshold.uniformProbability_eq_mean line 85
  16. theorem OAI.FixedClauseThreshold.uniformMean_sq_sub line 92
  17. theorem OAI.FixedClauseThreshold.uniformMean_sq_ge line 101
  18. def OAI.FixedClauseThreshold.uniformVariance line 107
  19. theorem OAI.FixedClauseThreshold.uniformVariance_eq line 110
  20. theorem OAI.FixedClauseThreshold.uniformVariance_le_sq_dist line 115