OAI/Probability/RandomSAT/ClauseProcess.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Coordinate erasure, independent clause averaging, survival probabilities, and iterated replacement.

  1. theorem OAI.FixedClauseThreshold.support_card_cons line 18
  2. def OAI.FixedClauseThreshold.prependAbsent line 25
  3. def OAI.FixedClauseThreshold.prependPresent line 28
  4. def OAI.FixedClauseThreshold.clauseHeadSplit line 35
  5. def OAI.FixedClauseThreshold.clauseHeadEquiv line 50
  6. theorem OAI.FixedClauseThreshold.satisfiesClause_prependAbsent line 66
  7. theorem OAI.FixedClauseThreshold.satisfiesClause_prependPresent line 71
  8. def OAI.FixedClauseThreshold.addClause line 76
  9. theorem OAI.FixedClauseThreshold.mem_addClause line 79
  10. theorem OAI.FixedClauseThreshold.addClause_comm line 84
  11. def OAI.FixedClauseThreshold.restrictSolutions line 91
  12. theorem OAI.FixedClauseThreshold.mem_restrictSolutions line 95
  13. theorem OAI.FixedClauseThreshold.restrictSolutions_zero line 100
  14. theorem OAI.FixedClauseThreshold.restrictSolutions_cons line 105
  15. theorem OAI.FixedClauseThreshold.restrictSolutions_comm line 113
  16. theorem OAI.FixedClauseThreshold.uniformMean_fin_succ line 120
  17. def OAI.FixedClauseThreshold.alive line 129
  18. theorem OAI.FixedClauseThreshold.alive_nonneg line 131
  19. theorem OAI.FixedClauseThreshold.alive_le_one line 135
  20. theorem OAI.FixedClauseThreshold.alive_mono line 139
  21. def OAI.FixedClauseThreshold.clauseAverage line 148
  22. def OAI.FixedClauseThreshold.survival line 152
  23. theorem OAI.FixedClauseThreshold.survival_zero line 155
  24. theorem OAI.FixedClauseThreshold.survival_succ line 158
  25. theorem OAI.FixedClauseThreshold.survival_eq_mean line 164
  26. theorem OAI.FixedClauseThreshold.properSATProbability_eq_survival line 179
  27. theorem OAI.FixedClauseThreshold.survival_nonneg line 193
  28. theorem OAI.FixedClauseThreshold.survival_le_one line 197
  29. theorem OAI.FixedClauseThreshold.survival_mono_solutions line 203
  30. theorem OAI.FixedClauseThreshold.survival_antitone line 213
  31. theorem OAI.FixedClauseThreshold.properSATProbability_antitone line 223
  32. theorem OAI.FixedClauseThreshold.clauseAverage_mono line 229
  33. theorem OAI.FixedClauseThreshold.clauseAverage_sub_const line 234
  34. theorem OAI.FixedClauseThreshold.clauseAverage_commute line 240
  35. theorem OAI.FixedClauseThreshold.clauseAverage_iterate_mono line 252
  36. theorem OAI.FixedClauseThreshold.clauseAverage_iterate_sub_const line 261
  37. theorem OAI.FixedClauseThreshold.survival_shift line 272
  38. theorem OAI.FixedClauseThreshold.survival_add line 277
  39. theorem OAI.FixedClauseThreshold.survival_eq_probability line 281
  40. theorem OAI.FixedClauseThreshold.blockUNSAT_eq line 292
  41. theorem OAI.FixedClauseThreshold.kills_iff_addClause line 298
  42. theorem OAI.FixedClauseThreshold.singleUNSAT_eq line 303
  43. theorem OAI.FixedClauseThreshold.shorter_survival_replacement line 318
  44. theorem OAI.FixedClauseThreshold.shorter_survival_replacement_many line 325
  45. theorem OAI.FixedClauseThreshold.uniformMean_sum_type line 358
  46. theorem OAI.FixedClauseThreshold.head_incidence_ratio line 370
  47. theorem OAI.FixedClauseThreshold.clauseHead_mean line 394