OAI/Probability/SATVariance/FiniteVariance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.favg_sum line 13
  2. lemma OAI.RandomKSAT.favg_sq_sub_const line 18
  3. def OAI.RandomKSAT.fvariance line 24
  4. lemma OAI.RandomKSAT.fvariance_centered line 27
  5. lemma OAI.RandomKSAT.fvariance_nonneg line 31
  6. lemma OAI.RandomKSAT.favg_sq_le line 36
  7. lemma OAI.RandomKSAT.fvariance_le_sq_sub line 39
  8. lemma OAI.RandomKSAT.fvariance_equiv line 44
  9. lemma OAI.RandomKSAT.fvariance_prod line 49
  10. lemma OAI.RandomKSAT.favg_cons line 56
  11. lemma OAI.RandomKSAT.coordinate_omission line 61
  12. lemma OAI.RandomKSAT.integral_uniform line 105
  13. lemma OAI.RandomKSAT.variance_uniform line 114
  14. def OAI.RandomKSAT.finiteSAT line 123
  15. def OAI.RandomKSAT.finiteTime line 126
  16. def OAI.RandomKSAT.omittedTime line 129
  17. lemma OAI.RandomKSAT.omittedTime_update line 133
  18. lemma OAI.RandomKSAT.finiteSAT_stream line 143
  19. lemma OAI.RandomKSAT.sum_fin_indicator_lt line 151
  20. lemma OAI.RandomKSAT.finiteTime_stream line 168
  21. lemma OAI.RandomKSAT.capped_coordinate_omission line 184