OAI/Probability/RandomSAT/Interpolation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Auxiliary ordered clauses allow repeated variables. Commuting finite averaging operators give the fixed-count partition interpolation corresponding to the marked-Poisson comparison.

  1. abbrev OAI.FixedClauseThreshold.AuxiliaryClause line 19
  2. def OAI.FixedClauseThreshold.auxiliarySatisfies line 21
  3. def OAI.FixedClauseThreshold.finiteClauseAverage line 24
  4. theorem OAI.FixedClauseThreshold.finiteClauseAverage_mono line 28
  5. theorem OAI.FixedClauseThreshold.finiteClauseAverage_add line 34
  6. theorem OAI.FixedClauseThreshold.finiteClauseAverage_const_mul line 41
  7. theorem OAI.FixedClauseThreshold.finiteClauseAverage_mul_const line 47
  8. theorem OAI.FixedClauseThreshold.finiteClauseAverage_commute line 53
  9. theorem OAI.FixedClauseThreshold.finiteClauseAverage_binomialMean line 69
  10. theorem OAI.FixedClauseThreshold.iterate_compare_of_commute line 77
  11. def OAI.FixedClauseThreshold.mixedAverage line 92
  12. theorem OAI.FixedClauseThreshold.mixedAverage_mono line 95
  13. theorem OAI.FixedClauseThreshold.finiteClauseAverage_commute_mix line 102
  14. def OAI.FixedClauseThreshold.embedAuxiliaryClause line 112
  15. def OAI.FixedClauseThreshold.embeddedAverage line 115
  16. def OAI.FixedClauseThreshold.auxiliaryAverage line 119
  17. def OAI.FixedClauseThreshold.auxiliarySurvival line 123
  18. def OAI.FixedClauseThreshold.auxiliaryProbability line 126
  19. def OAI.FixedClauseThreshold.embeddedForced line 129
  20. theorem OAI.FixedClauseThreshold.mem_embeddedForced line 132
  21. theorem OAI.FixedClauseThreshold.embeddedForced_id line 135
  22. theorem OAI.FixedClauseThreshold.opposing_literal_iff line 138
  23. theorem OAI.FixedClauseThreshold.opposing_literal_probability line 156
  24. theorem OAI.FixedClauseThreshold.embedded_kill_probability line 179
  25. theorem OAI.FixedClauseThreshold.embeddedAverage_alive line 203
  26. theorem OAI.FixedClauseThreshold.auxiliaryAverage_alive line 229
  27. theorem OAI.FixedClauseThreshold.forced_card_partition line 236
  28. theorem OAI.FixedClauseThreshold.partition_kill_convex line 244
  29. theorem OAI.FixedClauseThreshold.globalAverage_ge_local line 264
  30. theorem OAI.FixedClauseThreshold.mixed_finiteAverage_iterate line 278
  31. def OAI.FixedClauseThreshold.blockSet line 305
  32. theorem OAI.FixedClauseThreshold.mem_blockSet line 310
  33. theorem OAI.FixedClauseThreshold.blockSet_univ line 315
  34. theorem OAI.FixedClauseThreshold.blockSet_nonempty line 319
  35. theorem OAI.FixedClauseThreshold.alive_blockSet line 329
  36. theorem OAI.FixedClauseThreshold.filter_blockSet_left line 334
  37. theorem OAI.FixedClauseThreshold.filter_blockSet_right line 349
  38. theorem OAI.FixedClauseThreshold.auxiliarySurvival_succ line 364
  39. theorem OAI.FixedClauseThreshold.local_iterates_block line 371
  40. theorem OAI.FixedClauseThreshold.auxiliary_interpolation line 397