OAI/Combinatorics/TreewidthL1/CachedEnsemble.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreewidthL1.TreeCache.index_transport line 18
2. lemma OAI.BoundedTreewidthL1.TreeCache.index_retained line 40
3. lemma OAI.BoundedTreewidthL1.TreeCache.index_avoids line 52
4. def OAI.BoundedTreewidthL1.CachedEnsemble.data line 81
5. lemma OAI.BoundedTreewidthL1.CachedEnsemble.height line 96
6. lemma OAI.BoundedTreewidthL1.CachedEnsemble.launch line 141
7. lemma OAI.BoundedTreewidthL1.NoiseCube.OrdinarySeed.good_location line 191
8. lemma OAI.BoundedTreewidthL1.NoiseCube.node_gap line 201
9. lemma OAI.BoundedTreewidthL1.event_lower_integral line 249
10. lemma OAI.BoundedTreewidthL1.gap_proxy line 267
11. lemma OAI.BoundedTreewidthL1.gap_budget line 275
12. def OAI.BoundedTreewidthL1.AnchorTreeParticles.positive line 298
13. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.positive_affine line 301
14. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.measurable_positive line 329