OAI/Probability/RandomSAT/Convergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A balanced-block geometric potential proves convergence from boundedness and summable-min comparisons, including block counts that are not powers of two.

  1. def OAI.FixedClauseThreshold.balanceConstant line 18
  2. theorem OAI.FixedClauseThreshold.balanceConstant_pos line 20
  3. theorem OAI.FixedClauseThreshold.balanced_power_potential line 23
  4. theorem OAI.FixedClauseThreshold.balanced_blocks_bound line 41
  5. theorem OAI.FixedClauseThreshold.balanced_tail_bound line 123
  6. theorem OAI.FixedClauseThreshold.summable_min_convergence line 141