OAI/Probability/RandomSAT/Clauses.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Signed variable sets, clause cardinalities, and the exact probability of killing a nonempty solution set.

  1. def OAI.FixedClauseThreshold.clauseSupport line 18
  2. theorem OAI.FixedClauseThreshold.clauseSupport_card line 21
  3. theorem OAI.FixedClauseThreshold.mem_clauseSupport line 24
  4. abbrev OAI.FixedClauseThreshold.VariableSet line 28
  5. abbrev OAI.FixedClauseThreshold.SignedVariableSet line 30
  6. def OAI.FixedClauseThreshold.clauseFromSigns line 32
  7. theorem OAI.FixedClauseThreshold.clauseSupport_fromSigns line 42
  8. def OAI.FixedClauseThreshold.clauseToSigns line 47
  9. def OAI.FixedClauseThreshold.properClauseEquiv line 52
  10. theorem OAI.FixedClauseThreshold.card_variableSet line 81
  11. theorem OAI.FixedClauseThreshold.card_properClause line 85
  12. theorem OAI.FixedClauseThreshold.card_formula line 93
  13. theorem OAI.FixedClauseThreshold.nonempty_properClause line 97
  14. theorem OAI.FixedClauseThreshold.satisfiable_empty line 103
  15. theorem OAI.FixedClauseThreshold.properSATProbability_zero line 106
  16. theorem OAI.FixedClauseThreshold.properSATProbability_nonneg line 110
  17. theorem OAI.FixedClauseThreshold.properSATProbability_le_one line 115
  18. def OAI.FixedClauseThreshold.frozenCoordinates line 124
  19. def OAI.FixedClauseThreshold.KillsSolutions line 128
  20. theorem OAI.FixedClauseThreshold.kills_iff line 131
  21. def OAI.FixedClauseThreshold.forcedVariables line 162
  22. theorem OAI.FixedClauseThreshold.forcedVariables_empty line 165
  23. theorem OAI.FixedClauseThreshold.forcedVariables_eq_frozen line 169
  24. def OAI.FixedClauseThreshold.opposingClause line 180
  25. theorem OAI.FixedClauseThreshold.support_opposingClause line 183
  26. def OAI.FixedClauseThreshold.killingClauseEquiv line 187
  27. theorem OAI.FixedClauseThreshold.card_killingClauses line 216
  28. def OAI.FixedClauseThreshold.uniformProbability line 224
  29. theorem OAI.FixedClauseThreshold.uniformProbability_nonneg line 228
  30. theorem OAI.FixedClauseThreshold.uniformProbability_le_one line 233
  31. theorem OAI.FixedClauseThreshold.uniformProbability_mono line 242
  32. def OAI.FixedClauseThreshold.killingProbability line 251
  33. theorem OAI.FixedClauseThreshold.killingProbability_of_nonempty line 254
  34. theorem OAI.FixedClauseThreshold.killingProbability_empty line 263
  35. theorem OAI.FixedClauseThreshold.killingProbability_eq line 268