OAI/Probability/RandomSAT/Variance.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Stopped satisfiable lifetimes, insertion delays, and the coordinate-omission variance bound in terms of integrated forcing.

  1. theorem OAI.FixedClauseThreshold.addClause_subset line 18
  2. theorem OAI.FixedClauseThreshold.addClause_mono line 21
  3. theorem OAI.FixedClauseThreshold.addClause_empty line 27
  4. theorem OAI.FixedClauseThreshold.alive_empty line 30
  5. theorem OAI.FixedClauseThreshold.survival_empty line 32
  6. def OAI.FixedClauseThreshold.lifetime line 37
  7. theorem OAI.FixedClauseThreshold.lifetime_zero line 42
  8. theorem OAI.FixedClauseThreshold.lifetime_cons line 45
  9. theorem OAI.FixedClauseThreshold.lifetime_empty line 49
  10. theorem OAI.FixedClauseThreshold.lifetime_nonneg line 54
  11. theorem OAI.FixedClauseThreshold.lifetime_le line 60
  12. theorem OAI.FixedClauseThreshold.lifetime_mono line 68
  13. def OAI.FixedClauseThreshold.lifetimeMean line 76
  14. def OAI.FixedClauseThreshold.lifetimeVariance line 79
  15. theorem OAI.FixedClauseThreshold.lifetimeMean_succ line 82
  16. theorem OAI.FixedClauseThreshold.clauseAverage_sum line 90
  17. theorem OAI.FixedClauseThreshold.lifetimeMean_eq_sum line 95
  18. def OAI.FixedClauseThreshold.killingChance line 111
  19. theorem OAI.FixedClauseThreshold.killingChance_nonneg line 114
  20. theorem OAI.FixedClauseThreshold.killingChance_le_one line 119
  21. theorem OAI.FixedClauseThreshold.killingChance_eq_mean line 123
  22. theorem OAI.FixedClauseThreshold.killingChance_eq_probability line 129
  23. theorem OAI.FixedClauseThreshold.survival_le_geometric line 135
  24. def OAI.FixedClauseThreshold.insertionDelay line 146
  25. def OAI.FixedClauseThreshold.insertionSecond line 150
  26. theorem OAI.FixedClauseThreshold.insertionDelay_zero line 154
  27. theorem OAI.FixedClauseThreshold.insertionDelay_cons line 158
  28. theorem OAI.FixedClauseThreshold.pivot_sq line 164
  29. theorem OAI.FixedClauseThreshold.insertionDelay_cross line 170
  30. theorem OAI.FixedClauseThreshold.insertionDelay_cons_sq line 186
  31. theorem OAI.FixedClauseThreshold.insertionSecond_zero line 196
  32. theorem OAI.FixedClauseThreshold.insertionSecond_succ line 204
  33. theorem OAI.FixedClauseThreshold.killing_geometric_sum line 225
  34. def OAI.FixedClauseThreshold.truncatedKilling line 240
  35. theorem OAI.FixedClauseThreshold.pivotal_local_bound line 243
  36. def OAI.FixedClauseThreshold.occupation line 261
  37. theorem OAI.FixedClauseThreshold.occupation_eq_sum line 266
  38. theorem OAI.FixedClauseThreshold.occupation_nonneg line 279
  39. theorem OAI.FixedClauseThreshold.insertionSecond_le_occupation line 285
  40. theorem OAI.FixedClauseThreshold.uniformVariance_const_add line 305
  41. theorem OAI.FixedClauseThreshold.uniformVariance_product line 314
  42. theorem OAI.FixedClauseThreshold.uniformVariance_fin_succ line 322
  43. theorem OAI.FixedClauseThreshold.lifetimeVariance_succ_le line 330
  44. theorem OAI.FixedClauseThreshold.clauseAverage_const_mul line 356
  45. theorem OAI.FixedClauseThreshold.lifetimeVariance_le_occupation line 361
  46. theorem OAI.FixedClauseThreshold.killingChance_eq_killingProbability line 378
  47. def OAI.FixedClauseThreshold.forcedFraction line 387
  48. theorem OAI.FixedClauseThreshold.forcedFraction_nonneg line 390
  49. theorem OAI.FixedClauseThreshold.forcedFraction_le_one line 394
  50. theorem OAI.FixedClauseThreshold.killingChance_le_forced_pow line 400
  51. theorem OAI.FixedClauseThreshold.truncatedKilling_le_forced line 412
  52. theorem OAI.FixedClauseThreshold.clauseAverage_iterate_eq_mean line 444
  53. theorem OAI.FixedClauseThreshold.occupation_forced_eq line 462
  54. theorem OAI.FixedClauseThreshold.occupation_mono line 470
  55. theorem OAI.FixedClauseThreshold.occupation_const_mul line 476
  56. theorem OAI.FixedClauseThreshold.lifetimeVariance_forcing_bound line 487