OAI/Probability/RandomSAT/CenterBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Finite union bounds, a matching criterion for satisfiability, and positive finite bounds for the normalized centers.

  1. theorem OAI.FixedClauseThreshold.uniformProbability_exists_le line 18
  2. theorem OAI.FixedClauseThreshold.uniformProbability_forall_fintype line 36
  3. theorem OAI.FixedClauseThreshold.forcedVariables_singleton line 47
  4. theorem OAI.FixedClauseThreshold.randomClause_satisfies line 52
  5. theorem OAI.FixedClauseThreshold.first_moment_bound line 69
  6. theorem OAI.FixedClauseThreshold.uniformMean_lower_tail line 82
  7. theorem OAI.FixedClauseThreshold.uniformMean_upper_cutoff line 92
  8. theorem OAI.FixedClauseThreshold.center_lower_by_probability line 107
  9. theorem OAI.FixedClauseThreshold.center_upper_by_probability line 116
  10. theorem OAI.FixedClauseThreshold.satisfiable_of_matching line 130
  11. theorem OAI.FixedClauseThreshold.unsatisfiable_deficiency line 143
  12. def OAI.FixedClauseThreshold.firstMomentBase line 151
  13. theorem OAI.FixedClauseThreshold.firstMomentBase_nonneg line 153
  14. theorem OAI.FixedClauseThreshold.firstMomentBase_lt_one line 157
  15. theorem OAI.FixedClauseThreshold.first_moment_linear line 164
  16. theorem OAI.FixedClauseThreshold.center_first_moment line 181
  17. theorem OAI.FixedClauseThreshold.uniformProbability_equiv line 195
  18. theorem OAI.FixedClauseThreshold.uniformProbability_prod_first line 201
  19. theorem OAI.FixedClauseThreshold.uniformProbability_forall_mem line 216
  20. theorem OAI.FixedClauseThreshold.uniformMean_support line 234
  21. theorem OAI.FixedClauseThreshold.uniformProbability_support_subset line 249
  22. theorem OAI.FixedClauseThreshold.choose_quotient_le_pow line 281
  23. theorem OAI.FixedClauseThreshold.clause_subset_bound line 296
  24. theorem OAI.FixedClauseThreshold.unsatisfiable_container line 302
  25. theorem OAI.FixedClauseThreshold.deficiency_union_bound line 319
  26. theorem OAI.FixedClauseThreshold.choose_exp_bound line 366
  27. def OAI.FixedClauseThreshold.smallDensity line 384
  28. theorem OAI.FixedClauseThreshold.smallDensity_pos line 386
  29. theorem OAI.FixedClauseThreshold.smallDensity_le_one line 388
  30. theorem OAI.FixedClauseThreshold.smallDensity_calibration line 393
  31. theorem OAI.FixedClauseThreshold.hall_summand_bound line 400
  32. theorem OAI.FixedClauseThreshold.half_geometric_sum_le line 442
  33. theorem OAI.FixedClauseThreshold.small_density_probability_bound line 451
  34. def OAI.FixedClauseThreshold.lowerCenterBound line 471
  35. theorem OAI.FixedClauseThreshold.lowerCenterBound_pos line 473
  36. theorem OAI.FixedClauseThreshold.center_lower_explicit line 475
  37. theorem OAI.FixedClauseThreshold.center_bounds_eventually line 501