OAI/Probability/SATVariance/FirstFailure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.prefixSAT_zero line 13
  2. lemma OAI.RandomKSAT.prefixSAT_mono line 16
  3. lemma OAI.RandomKSAT.lt_firstFailure_iff line 21
  4. lemma OAI.RandomKSAT.firstFailure_le_iff line 37
  5. lemma OAI.RandomKSAT.firstFailure_pos line 41
  6. lemma OAI.RandomKSAT.assignment_survival line 44
  7. lemma OAI.RandomKSAT.first_moment_tail line 57
  8. lemma OAI.RandomKSAT.measurableSet_prefixSAT line 70
  9. lemma OAI.RandomKSAT.firstFailure_eq_succ_iff line 82
  10. lemma OAI.RandomKSAT.measurable_firstFailure line 93
  11. lemma OAI.RandomKSAT.measurable_H line 112
  12. lemma OAI.RandomKSAT.measurable_T line 115
  13. lemma OAI.RandomKSAT.survival_rate_lt_one line 119
  14. lemma OAI.RandomKSAT.firstFailure_finite_ae line 123
  15. lemma OAI.RandomKSAT.T_nonneg line 142
  16. lemma OAI.RandomKSAT.T_le_cap line 146
  17. lemma OAI.RandomKSAT.T_memLp line 150