OAI/Probability/SATVariance/BlockKilling.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RandomKSAT.SetSAT line 13

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

  2. def OAI.RandomKSAT.blockKill line 16

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

  3. lemma OAI.RandomKSAT.setSAT_univ line 19
  4. lemma OAI.RandomKSAT.measurableSet_setSAT line 23
  5. lemma OAI.RandomKSAT.blockKill_nonneg line 39
  6. lemma OAI.RandomKSAT.blockKill_le_one line 42
  7. lemma OAI.RandomKSAT.blockKill_empty line 47
  8. lemma OAI.RandomKSAT.blockKill_compl line 52
  9. lemma OAI.RandomKSAT.clauseLaw_kills_toReal line 59
  10. lemma OAI.RandomKSAT.blockKill_one line 64
  11. lemma OAI.RandomKSAT.blockKill_individual line 76
  12. lemma OAI.RandomKSAT.set_survival_le line 98
  13. lemma OAI.RandomKSAT.frozen_card_le line 109
  14. lemma OAI.RandomKSAT.rate_toReal line 112
  15. lemma OAI.RandomKSAT.real_rate_nonneg line 118
  16. lemma OAI.RandomKSAT.survival_exp_bound line 121
  17. lemma OAI.RandomKSAT.blockKill_exp_full line 134
  18. lemma OAI.RandomKSAT.blockKill_exp_individual line 143
  19. lemma OAI.RandomKSAT.one_sub_exp_neg_two_mul_ge line 160
  20. lemma OAI.RandomKSAT.blockKill_long line 172
  21. def OAI.RandomKSAT.replacementK line 199
  22. lemma OAI.RandomKSAT.replacementK_succ line 201
  23. lemma OAI.RandomKSAT.replacement_numeric line 204
  24. lemma OAI.RandomKSAT.one_replacement line 277