OAI/Probability/SATVariance/LifetimePotential.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.favg_tsum line 13
  2. lemma OAI.RandomKSAT.lifetime_mono line 19
  3. lemma OAI.RandomKSAT.lifetime_bellman line 24
  4. lemma OAI.RandomKSAT.alive_le_lifetime line 38
  5. def OAI.RandomKSAT.markovSum line 43
  6. lemma OAI.RandomKSAT.markovSum_mono line 47
  7. lemma OAI.RandomKSAT.markovSum_potential line 56
  8. lemma OAI.RandomKSAT.markovSum_level line 76
  9. def OAI.RandomKSAT.scheduledStep line 100
  10. lemma OAI.RandomKSAT.scheduledStep_mono line 105
  11. lemma OAI.RandomKSAT.scheduledStep_const line 114
  12. lemma OAI.RandomKSAT.scheduledStep_add_const line 124
  13. lemma OAI.RandomKSAT.scheduledStep_drift line 136
  14. lemma OAI.RandomKSAT.scheduled_occupation line 148
  15. lemma OAI.RandomKSAT.markovSum_const line 174
  16. lemma OAI.RandomKSAT.scheduled_occupation_le_length line 185
  17. lemma OAI.RandomKSAT.tailIndicator_antitone line 194
  18. lemma OAI.RandomKSAT.integral_tailIndicator line 203
  19. lemma OAI.RandomKSAT.favg_integral line 209
  20. lemma OAI.RandomKSAT.scheduledStep_antitone line 215
  21. lemma OAI.RandomKSAT.scheduledStep_integral line 224
  22. lemma OAI.RandomKSAT.scheduledSum_antitone line 238
  23. lemma OAI.RandomKSAT.scheduledSum_integral line 247
  24. lemma OAI.RandomKSAT.scheduled_layercake line 272
  25. lemma OAI.RandomKSAT.scheduled_reward_tail line 286
  26. lemma OAI.RandomKSAT.scheduled_reward_tail_bound line 319
  27. lemma OAI.RandomKSAT.scheduled_reward_integrated_subcritical line 333
  28. lemma OAI.RandomKSAT.scheduled_reward_integrated_critical line 348
  29. def OAI.RandomKSAT.occupationGamma line 369
  30. lemma OAI.RandomKSAT.occupationGamma_succ line 371
  31. lemma OAI.RandomKSAT.occupationGamma_pos line 378
  32. def OAI.RandomKSAT.occupationReward line 383
  33. lemma OAI.RandomKSAT.occupationReward_nonneg line 386
  34. lemma OAI.RandomKSAT.occupationReward_le_one line 393
  35. lemma OAI.RandomKSAT.occupationReward_product line 401