OAI/Probability/RandomSAT/Forcing.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Deletion and erasure of a coordinate, permutation symmetry, and the integrated forcing bound.

  1. abbrev OAI.FixedClauseThreshold.SplitClause line 18
  2. def OAI.FixedClauseThreshold.DeletedSatisfied line 20
  3. def OAI.FixedClauseThreshold.ErasedSatisfied line 24
  4. def OAI.FixedClauseThreshold.deletedSolutions line 28
  5. def OAI.FixedClauseThreshold.erasedSolutions line 31
  6. theorem OAI.FixedClauseThreshold.mem_deletedSolutions line 34
  7. theorem OAI.FixedClauseThreshold.mem_erasedSolutions line 39
  8. theorem OAI.FixedClauseThreshold.erasedSolutions_subset line 44
  9. theorem OAI.FixedClauseThreshold.satisfies_head_split line 55
  10. theorem OAI.FixedClauseThreshold.head_erasure_extension line 65
  11. theorem OAI.FixedClauseThreshold.head_deletion_projection line 76
  12. theorem OAI.FixedClauseThreshold.head_forced_reduction line 88
  13. theorem OAI.FixedClauseThreshold.head_forced_indicator_le line 108
  14. theorem OAI.FixedClauseThreshold.deletedSolutions_cons_inl line 120
  15. theorem OAI.FixedClauseThreshold.deletedSolutions_cons_inr line 128
  16. theorem OAI.FixedClauseThreshold.erasedSolutions_cons_inl line 135
  17. theorem OAI.FixedClauseThreshold.erasedSolutions_cons_inr line 143
  18. def OAI.FixedClauseThreshold.deletedMean line 151
  19. def OAI.FixedClauseThreshold.erasedMean line 155
  20. theorem OAI.FixedClauseThreshold.deletedMean_zero line 159
  21. theorem OAI.FixedClauseThreshold.erasedMean_zero line 167
  22. theorem OAI.FixedClauseThreshold.deletedMean_succ line 175
  23. theorem OAI.FixedClauseThreshold.erasedMean_succ line 195
  24. theorem OAI.FixedClauseThreshold.clauseAverage_binomialMean line 214
  25. theorem OAI.FixedClauseThreshold.clauseAverage_survival line 220
  26. theorem OAI.FixedClauseThreshold.clauseAverage_short_survival line 224
  27. theorem OAI.FixedClauseThreshold.deletedMean_eq_binomial line 239
  28. theorem OAI.FixedClauseThreshold.erasedMean_replacement line 265
  29. theorem OAI.FixedClauseThreshold.replacementBlock_pos line 318
  30. theorem OAI.FixedClauseThreshold.replacementError_nonneg line 324
  31. def OAI.FixedClauseThreshold.headForcedMean line 328
  32. theorem OAI.FixedClauseThreshold.headForcedMean_le_difference line 333
  33. theorem OAI.FixedClauseThreshold.headForcedMean_replacement line 345
  34. theorem OAI.FixedClauseThreshold.integrated_head_forcing line 386
  35. def OAI.FixedClauseThreshold.renameClause line 417
  36. def OAI.FixedClauseThreshold.renameClauseEquiv line 424
  37. def OAI.FixedClauseThreshold.renameAssignment line 430
  38. def OAI.FixedClauseThreshold.renameFormula line 433
  39. def OAI.FixedClauseThreshold.renameFormulaEquiv line 436
  40. theorem OAI.FixedClauseThreshold.renameFormulaEquiv_apply line 439
  41. theorem OAI.FixedClauseThreshold.satisfiesClause_rename line 442
  42. theorem OAI.FixedClauseThreshold.satisfies_rename line 452
  43. theorem OAI.FixedClauseThreshold.satisfies_rename_inverse line 457
  44. theorem OAI.FixedClauseThreshold.satisfiable_rename line 467
  45. theorem OAI.FixedClauseThreshold.mem_forced_formula line 475
  46. theorem OAI.FixedClauseThreshold.forcedVariables_rename line 480
  47. theorem OAI.FixedClauseThreshold.forced_coordinate_mean line 493
  48. def OAI.FixedClauseThreshold.forcedFractionMean line 521
  49. theorem OAI.FixedClauseThreshold.forcedFractionMean_eq_head line 525
  50. theorem OAI.FixedClauseThreshold.integrated_forcing_finite line 539