OAI/Geometry/Cannon/Flows/Subdivision.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CannonFlow.Subdivision line 26
2. structure OAI.CannonFlow.Population line 33
3. def OAI.CannonFlow.Subdivision.Offspring line 41
4. instance OAI.CannonFlow.Subdivision.(instance at line 43) line 43
5. def OAI.CannonFlow.Subdivision.next line 45
6. def OAI.CannonFlow.Subdivision.parentOf line 50
7. def OAI.CannonFlow.Subdivision.probOf line 53
8. lemma OAI.CannonFlow.Subdivision.fiber_sum line 57
9. def OAI.CannonFlow.Subdivision.generation line 73
10. def OAI.CannonFlow.Subdivision.weights line 77
11. lemma OAI.CannonFlow.Subdivision.weights_pos line 82
12. def OAI.CannonFlow.Subdivision.flow line 90
13. theorem OAI.CannonFlow.Subdivision.flow_step line 101
14. def OAI.CannonFlow.FiniteFlow.ancestor line 112
15. theorem OAI.CannonFlow.FiniteFlow.conditional_weight line 116
16. theorem OAI.CannonFlow.FiniteFlow.ancestor_conserves line 130
17. theorem OAI.CannonFlow.FiniteFlow.descendant_displacement line 159
18. theorem OAI.CannonFlow.FiniteFlow.centers_separated line 183
19. theorem OAI.CannonNode.source_rule_of_subdivisions line 221
20. theorem OAI.CannonNode.exists_nonlocally_constant line 300
21. theorem OAI.CannonNode.root_at_scale line 317
22. structure OAI.CannonNode.SourceConstruction line 340
23. lemma OAI.CannonNode.exists_source_threshold line 369
24. theorem OAI.CannonNode.exists_source_construction line 387
25. lemma OAI.CannonFlow.Subdivision.generation_property line 523
26. lemma OAI.CannonFlow.Subdivision.generation_depth line 534
27. lemma OAI.CannonFlow.Subdivision.generation_siblings line 546