OAI/Probability/SATVariance/CapBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.T_eq_min_natH_ae line 13
  2. lemma OAI.RandomKSAT.cap_error_eq_nat_ae line 23
  3. lemma OAI.RandomKSAT.natH_integral line 30
  4. lemma OAI.RandomKSAT.summable_sub_sq_geometric line 41
  5. lemma OAI.RandomKSAT.tsum_sub_sq_geometric line 50
  6. lemma OAI.RandomKSAT.cap_error_geom line 66
  7. lemma OAI.RandomKSAT.U_pos line 95
  8. lemma OAI.RandomKSAT.cap_geometric_uniform line 100
  9. def OAI.RandomKSAT.bridgeC line 114
  10. lemma OAI.RandomKSAT.bridgeC_nonneg line 117
  11. lemma OAI.RandomKSAT.cap_error_uniform line 121
  12. lemma OAI.RandomKSAT.variance_bridge line 134
  13. lemma OAI.RandomKSAT.H_variance_le_cap line 155
  14. lemma OAI.RandomKSAT.cap_variance_le_H line 162
  15. theorem OAI.RandomKSAT.uncapped_variance_upper line 175