OAI/Probability/RandomSAT/CenterComparison.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Partition interpolation and concentration yield summable-error comparisons for centers of two blocks and of neighboring sizes.

  1. theorem OAI.FixedClauseThreshold.auxiliary_interpolation_center_lower line 18
  2. def OAI.FixedClauseThreshold.densityWindow line 93
  3. theorem OAI.FixedClauseThreshold.densityWindow_pos line 95
  4. theorem OAI.FixedClauseThreshold.fluctuationWindow_eq_mul line 98
  5. theorem OAI.FixedClauseThreshold.fluctuationWindow_one_le line 103
  6. theorem OAI.FixedClauseThreshold.densityWindow_antitone line 109
  7. theorem OAI.FixedClauseThreshold.densityWindow_tendsto line 114
  8. theorem OAI.FixedClauseThreshold.concentrationError_tendsto line 118
  9. theorem OAI.FixedClauseThreshold.samplingError_identity line 124
  10. theorem OAI.FixedClauseThreshold.samplingError_tendsto line 133
  11. theorem OAI.FixedClauseThreshold.fluctuationWindow_tendsto line 143
  12. theorem OAI.FixedClauseThreshold.center_lower_of_auxiliary_probability line 148
  13. theorem OAI.FixedClauseThreshold.center_sum_comparison_of_bounds line 169
  14. def OAI.FixedClauseThreshold.neighborFactor line 231
  15. def OAI.FixedClauseThreshold.neighborLower line 233
  16. theorem OAI.FixedClauseThreshold.neighborLower_pos line 235
  17. theorem OAI.FixedClauseThreshold.auxiliaryProbability_zero line 238
  18. theorem OAI.FixedClauseThreshold.neighbor_all_left line 241
  19. theorem OAI.FixedClauseThreshold.neighbor_pow_lower line 255
  20. theorem OAI.FixedClauseThreshold.center_neighbor_comparison_of_bounds line 276
  21. structure OAI.FixedClauseThreshold.CenterRegular line 316
  22. theorem OAI.FixedClauseThreshold.centerRegular_eventually line 327
  23. theorem OAI.FixedClauseThreshold.center_comparisons line 344