OAI/Probability/SATVariance/MarkovReplacement.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RandomKSAT.favg line 13

    Also declared: ComparatorChallenges/SATSharpness.lean:44 (same declaration text).

  2. lemma OAI.RandomKSAT.favg_mono line 16
  3. lemma OAI.RandomKSAT.favg_const line 20
  4. lemma OAI.RandomKSAT.favg_add line 24
  5. lemma OAI.RandomKSAT.favg_sub line 28
  6. lemma OAI.RandomKSAT.favg_equiv line 32
  7. lemma OAI.RandomKSAT.favg_comm line 36
  8. lemma OAI.RandomKSAT.favg_prod line 42
  9. lemma OAI.RandomKSAT.uniformOn_real line 48
  10. lemma OAI.RandomKSAT.prefixLaw line 56
  11. def OAI.RandomKSAT.residual line 65
  12. lemma OAI.RandomKSAT.residual_comm line 69
  13. lemma OAI.RandomKSAT.residual_cons line 76
  14. def OAI.RandomKSAT.clauseStep line 82

    Also declared: ComparatorChallenges/SATSharpness.lean:47 (same declaration text).

  15. def OAI.RandomKSAT.alive line 86

    Also declared: ComparatorChallenges/SATSharpness.lean:51 (same declaration text).

  16. lemma OAI.RandomKSAT.clauseStep_mono line 88
  17. lemma OAI.RandomKSAT.clauseStep_const line 92
  18. lemma OAI.RandomKSAT.clauseStep_add line 98
  19. lemma OAI.RandomKSAT.clauseStep_comm line 103
  20. lemma OAI.RandomKSAT.clauseStep_iterate_avg line 117
  21. lemma OAI.RandomKSAT.blockKill_iterate line 132
  22. lemma OAI.RandomKSAT.iterate_add_const line 149
  23. lemma OAI.RandomKSAT.markov_telescoping line 157
  24. lemma OAI.RandomKSAT.clauseStep_add_const line 180
  25. lemma OAI.RandomKSAT.sequential_replacement line 185
  26. lemma OAI.RandomKSAT.favg_mul line 208
  27. lemma OAI.RandomKSAT.favg_nonneg line 213
  28. lemma OAI.RandomKSAT.residual_subset line 217
  29. lemma OAI.RandomKSAT.residual_mono line 221
  30. lemma OAI.RandomKSAT.alive_nonneg line 225
  31. lemma OAI.RandomKSAT.alive_le_one line 229
  32. lemma OAI.RandomKSAT.alive_mono line 233
  33. def OAI.RandomKSAT.survival line 241

    Also declared: ComparatorChallenges/SATSharpness.lean:53 (same declaration text).

  34. lemma OAI.RandomKSAT.survival_avg line 244
  35. lemma OAI.RandomKSAT.survival_zero line 248
  36. lemma OAI.RandomKSAT.survival_empty line 250
  37. lemma OAI.RandomKSAT.survival_nonneg line 253
  38. lemma OAI.RandomKSAT.survival_le_one line 258
  39. lemma OAI.RandomKSAT.survival_mono line 264
  40. lemma OAI.RandomKSAT.survival_eq_prob line 269
  41. lemma OAI.RandomKSAT.survival_summable line 276
  42. lemma OAI.RandomKSAT.survival_add line 288
  43. lemma OAI.RandomKSAT.survival_submultiplicative line 294
  44. def OAI.RandomKSAT.lifetime line 308

    Also declared: ComparatorChallenges/SATSharpness.lean:56 (same declaration text).

  45. lemma OAI.RandomKSAT.lifetime_nonneg line 310
  46. lemma OAI.RandomKSAT.lifetime_empty line 313
  47. lemma OAI.RandomKSAT.lifetime_block line 315
  48. def OAI.RandomKSAT.lifetimeBeta line 338
  49. def OAI.RandomKSAT.lifetimeC line 340
  50. lemma OAI.RandomKSAT.replacementK_one_le line 342
  51. lemma OAI.RandomKSAT.lifetimeBeta_succ line 347
  52. lemma OAI.RandomKSAT.lifetimeC_pos line 352
  53. lemma OAI.RandomKSAT.replacement_block_choice line 357
  54. lemma OAI.RandomKSAT.lifetime_product line 381
  55. lemma OAI.RandomKSAT.lifetime_level line 427