OAI/Probability/RandomSAT/Transfer.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

The exact probability of distinct variables, birthday bounds, and deletion and thinning comparisons transfer auxiliary probabilities to the proper-clause law.

  1. def OAI.FixedClauseThreshold.properFraction line 18
  2. theorem OAI.FixedClauseThreshold.card_injective_lists line 20
  3. theorem OAI.FixedClauseThreshold.properFraction_probability line 25
  4. theorem OAI.FixedClauseThreshold.properFraction_nonneg line 32
  5. theorem OAI.FixedClauseThreshold.properFraction_le_one line 36
  6. theorem OAI.FixedClauseThreshold.repetition_count_mono line 40
  7. theorem OAI.FixedClauseThreshold.properFraction_mul_kill line 67
  8. theorem OAI.FixedClauseThreshold.auxiliary_kill_le_repetition line 77
  9. theorem OAI.FixedClauseThreshold.clauseAverage_alive line 101
  10. theorem OAI.FixedClauseThreshold.auxiliaryAverage_le_proper line 117
  11. theorem OAI.FixedClauseThreshold.scaled_proper_le_auxiliaryAverage line 127
  12. theorem OAI.FixedClauseThreshold.auxiliaryProbability_le_proper line 143
  13. theorem OAI.FixedClauseThreshold.proper_scaled_le_auxiliaryProbability line 150
  14. def OAI.FixedClauseThreshold.repeatPairs line 184
  15. theorem OAI.FixedClauseThreshold.repeatPairs_zero line 186
  16. theorem OAI.FixedClauseThreshold.repeatPairs_succ line 188
  17. theorem OAI.FixedClauseThreshold.repeatPairs_nonneg line 192
  18. theorem OAI.FixedClauseThreshold.properFraction_succ line 194
  19. theorem OAI.FixedClauseThreshold.properFraction_lower line 201
  20. theorem OAI.FixedClauseThreshold.auxiliarySurvival_nonneg line 213
  21. theorem OAI.FixedClauseThreshold.auxiliarySurvival_le_one line 219
  22. theorem OAI.FixedClauseThreshold.auxiliaryProbability_nonneg line 228
  23. theorem OAI.FixedClauseThreshold.auxiliaryProbability_le_one line 231
  24. theorem OAI.FixedClauseThreshold.finite_model_sandwich line 234
  25. theorem OAI.FixedClauseThreshold.thinned_count_mean_bounds line 245
  26. theorem OAI.FixedClauseThreshold.exp_neg_two_le_one_sub line 262
  27. def OAI.FixedClauseThreshold.transferFactor line 271
  28. def OAI.FixedClauseThreshold.transferLower line 273
  29. theorem OAI.FixedClauseThreshold.transferFactor_pos line 275
  30. theorem OAI.FixedClauseThreshold.transferLower_pos line 277
  31. theorem OAI.FixedClauseThreshold.properFraction_pow_lower line 279
  32. theorem OAI.FixedClauseThreshold.auxiliaryProbability_center_lower line 297
  33. theorem OAI.FixedClauseThreshold.auxiliaryProbability_center_upper line 318
  34. theorem OAI.FixedClauseThreshold.binomialMean_square line 325
  35. theorem OAI.FixedClauseThreshold.binomialMean_centered_square line 345
  36. theorem OAI.FixedClauseThreshold.binomialMean_div_const line 357
  37. theorem OAI.FixedClauseThreshold.binomialMean_all_success line 361
  38. theorem OAI.FixedClauseThreshold.product_lower_two_deviations line 373
  39. def OAI.FixedClauseThreshold.samplingError line 392
  40. theorem OAI.FixedClauseThreshold.samplingError_nonneg line 395