OAI/Probability/SATVariance/WeightedRewards.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.markovSum_projection line 13
  2. lemma OAI.RandomKSAT.rootSum_projection line 28
  3. lemma OAI.RandomKSAT.fibre_univ line 35
  4. lemma OAI.RandomKSAT.rootSum_test_bound line 38
  5. def OAI.RandomKSAT.incidentSet line 73
  6. def OAI.RandomKSAT.collisionSet line 76
  7. lemma OAI.RandomKSAT.testIndices_card_le line 79
  8. lemma OAI.RandomKSAT.incidentSet_sum line 86
  9. lemma OAI.RandomKSAT.available_of_no_collision line 96
  10. lemma OAI.RandomKSAT.uniqueTrue_injective line 103
  11. lemma OAI.RandomKSAT.available_except_one line 108
  12. lemma OAI.RandomKSAT.lifetimeBeta_bounds line 126
  13. def OAI.RandomKSAT.deletionQ line 139
  14. lemma OAI.RandomKSAT.deletionQ_nonneg line 141
  15. lemma OAI.RandomKSAT.lifetime_weight_product line 146
  16. lemma OAI.RandomKSAT.weighted_all_tests line 159
  17. lemma OAI.RandomKSAT.weighted_all_but_one_test line 178
  18. lemma OAI.RandomKSAT.scheduledStep_mul line 195
  19. lemma OAI.RandomKSAT.rootRewards_square_test_bound line 205
  20. def OAI.RandomKSAT.durationLog line 222
  21. lemma OAI.RandomKSAT.durationLog_one_le line 224
  22. lemma OAI.RandomKSAT.integrated_occupationReward line 231
  23. lemma OAI.RandomKSAT.rootRewards_square_no_collision line 284
  24. lemma OAI.RandomKSAT.rootRewards_square_one_collision line 309
  25. lemma OAI.RandomKSAT.dataRewards_nonneg line 334
  26. lemma OAI.RandomKSAT.dataRewards_le_length line 338
  27. lemma OAI.RandomKSAT.rootRewards_square_conditioned line 343
  28. lemma OAI.RandomKSAT.deletionQ_poly_bound line 382
  29. lemma OAI.RandomKSAT.deletionQ_sq_poly_bound line 396