OAI/Combinatorics/TreewidthL1/NoiseCube.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedTreewidthL1.NoiseCube.affine_interval_bound line 9
2. lemma OAI.BoundedTreewidthL1.NoiseCube.unit_affine_bound line 22
3. lemma OAI.BoundedTreewidthL1.NoiseCube.cube_strip line 33
4. lemma OAI.BoundedTreewidthL1.NoiseCube.cube_strip_any line 62
5. lemma OAI.BoundedTreewidthL1.NoiseCube.product_strip_first line 69
6. lemma OAI.BoundedTreewidthL1.NoiseCube.product_strip_second line 89
7. theorem OAI.BoundedTreewidthL1.NoiseCube.simultaneous_gap line 100
8. lemma OAI.BoundedTreewidthL1.RootedTree.join_prefix_data line 142
9. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.height_segment line 183
10. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.launch_segment line 215
11. lemma OAI.BoundedTreewidthL1.NoiseCube.flip_triple line 257
12. lemma OAI.BoundedTreewidthL1.NoiseCube.conditioned_gap line 266
13. lemma OAI.BoundedTreewidthL1.NoiseCube.pi_conditioned line 304