OAI/Probability/LatticeSurface/Coercivity/SparseWitnessModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseBlocks.q_nonneg line 252
2. lemma OAI.SparseBlocks.q_pos line 255
3. abbrev OAI.SparseBlocks.ShortChoice line 258
4. def OAI.SparseBlocks.shortEdges line 260
5. abbrev OAI.SparseBlocks.FarChoice line 263
6. def OAI.SparseBlocks.farEdges line 267
7. def OAI.SparseBlocks.tieEdges line 269
8. def OAI.SparseBlocks.shortTest line 272
9. def OAI.SparseBlocks.farTest line 275
10. def OAI.SparseBlocks.tieTest line 278
11. def OAI.SparseBlocks.witnessTest line 281
12. lemma OAI.SparseBlocks.bad_witness line 284
13. lemma OAI.SparseBlocks.witness_family line 335
14. lemma OAI.SparseBlocks.short_entropy line 356
15. lemma OAI.SparseBlocks.far_entropy line 363