OAI/Probability/RandomSAT/Concentration.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Normalized capped centers and polynomial concentration of the proper-clause satisfiability probability.

  1. def OAI.FixedClauseThreshold.capMultiplier line 18
  2. def OAI.FixedClauseThreshold.mainCap line 20
  3. def OAI.FixedClauseThreshold.center line 22
  4. def OAI.FixedClauseThreshold.varianceConstant line 25
  5. theorem OAI.FixedClauseThreshold.capMultiplier_pos line 28
  6. theorem OAI.FixedClauseThreshold.replacementBlock_le line 32
  7. theorem OAI.FixedClauseThreshold.replacementError_mul line 39
  8. theorem OAI.FixedClauseThreshold.integrated_forcing_capped line 49
  9. theorem OAI.FixedClauseThreshold.variance_capped line 80
  10. theorem OAI.FixedClauseThreshold.uniform_chebyshev line 94
  11. theorem OAI.FixedClauseThreshold.alive_univ line 106
  12. theorem OAI.FixedClauseThreshold.uniformProbability_fin_succ line 109
  13. theorem OAI.FixedClauseThreshold.lifetime_tail_probability line 118
  14. theorem OAI.FixedClauseThreshold.properSATProbability_eq_lifetime_tail line 156
  15. def OAI.FixedClauseThreshold.delta line 164
  16. def OAI.FixedClauseThreshold.eta line 166
  17. def OAI.FixedClauseThreshold.fluctuationWindow line 168
  18. def OAI.FixedClauseThreshold.concentrationError line 170
  19. theorem OAI.FixedClauseThreshold.delta_pos line 172
  20. theorem OAI.FixedClauseThreshold.delta_lt_half line 177
  21. theorem OAI.FixedClauseThreshold.eta_eq_twice_delta line 182
  22. theorem OAI.FixedClauseThreshold.varianceConstant_nonneg line 186
  23. theorem OAI.FixedClauseThreshold.fluctuationWindow_pos line 190
  24. theorem OAI.FixedClauseThreshold.concentrationError_nonneg line 193
  25. theorem OAI.FixedClauseThreshold.variance_window_identity line 196
  26. theorem OAI.FixedClauseThreshold.concentration_capped line 214
  27. theorem OAI.FixedClauseThreshold.center_nonneg line 239
  28. theorem OAI.FixedClauseThreshold.center_le_capMultiplier line 243
  29. theorem OAI.FixedClauseThreshold.properSATProbability_center_upper line 252
  30. theorem OAI.FixedClauseThreshold.properSATProbability_center_lower line 260