OAI/Probability/RandomSAT/Replacement.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Quantitative comparison of a shorter clause with a block of independent proper clauses, uniformly over the background solution set.

  1. def OAI.FixedClauseThreshold.killFraction line 18
  2. theorem OAI.FixedClauseThreshold.killFraction_nonneg line 20
  3. theorem OAI.FixedClauseThreshold.killFraction_zero line 24
  4. theorem OAI.FixedClauseThreshold.killFraction_succ line 27
  5. theorem OAI.FixedClauseThreshold.sub_ratio_le line 48
  6. theorem OAI.FixedClauseThreshold.killFraction_le_pow line 56
  7. theorem OAI.FixedClauseThreshold.killFraction_le_half_pow line 78
  8. theorem OAI.FixedClauseThreshold.nat_le_internal_choose line 87
  9. theorem OAI.FixedClauseThreshold.killFraction_small_forcing line 103
  10. theorem OAI.FixedClauseThreshold.succ_ratio_lower line 117
  11. theorem OAI.FixedClauseThreshold.killFraction_succ_lower line 132
  12. theorem OAI.FixedClauseThreshold.power_survival_bound line 140
  13. theorem OAI.FixedClauseThreshold.block_ge_of_double line 156
  14. theorem OAI.FixedClauseThreshold.uniformProbability_true line 169
  15. theorem OAI.FixedClauseThreshold.uniformProbability_false line 178
  16. theorem OAI.FixedClauseThreshold.uniformProbability_congr line 182
  17. theorem OAI.FixedClauseThreshold.uniformProbability_not line 187
  18. theorem OAI.FixedClauseThreshold.uniformProbability_forall line 193
  19. theorem OAI.FixedClauseThreshold.uniformProbability_exists line 204
  20. def OAI.FixedClauseThreshold.blockUNSATProbability line 215
  21. theorem OAI.FixedClauseThreshold.blockUNSAT_lower line 219
  22. theorem OAI.FixedClauseThreshold.replacement_numeric line 228
  23. def OAI.FixedClauseThreshold.replacementScale line 282
  24. def OAI.FixedClauseThreshold.replacementError line 284
  25. def OAI.FixedClauseThreshold.replacementBlock line 286
  26. theorem OAI.FixedClauseThreshold.replacementScale_pos line 288
  27. theorem OAI.FixedClauseThreshold.replacementScale_pow line 292
  28. theorem OAI.FixedClauseThreshold.replacementScale_one_le line 299
  29. theorem OAI.FixedClauseThreshold.replacementError_eq line 304
  30. theorem OAI.FixedClauseThreshold.replacementError_small line 312
  31. theorem OAI.FixedClauseThreshold.shorter_clause_replacement line 324