OAI/Probability/SATVariance/Subcube.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RandomKSAT.subcube line 12
2. lemma OAI.RandomKSAT.mem_subcube line 15
3. lemma OAI.RandomKSAT.subcube_nonempty line 19
4. lemma OAI.RandomKSAT.subcube_sat_of_disjoint line 22
5. lemma OAI.RandomKSAT.frozen_subcube line 55
6. lemma OAI.RandomKSAT.frozen_subcube_card line 74
7. lemma OAI.RandomKSAT.subcube_one line 84
8. lemma OAI.RandomKSAT.subcube_killing_indicator line 88
9. lemma OAI.RandomKSAT.favg_pi_pair line 126
10. lemma OAI.RandomKSAT.support_probability line 131
11. lemma OAI.RandomKSAT.overlap_favg line 136
12. lemma OAI.RandomKSAT.blockKill_favg line 156
13. lemma OAI.RandomKSAT.subcube_block_upper line 168
14. lemma OAI.RandomKSAT.bernoulli_quadratic line 203
15. lemma OAI.RandomKSAT.subcube_block_lower line 215