OAI/Geometry/HyperbolicGroups/StarMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.sum_subtype_eq_ite line 15
2. abbrev OAI.HyperbolicObstruction.StarModel.starCount line 26
3. lemma OAI.HyperbolicObstruction.StarModel.starCount_branch line 30
4. lemma OAI.HyperbolicObstruction.StarModel.starCount_leaf line 44
5. lemma OAI.HyperbolicObstruction.StarModel.branchDeviation_subtype line 54
6. lemma OAI.HyperbolicObstruction.StarModel.expect_starCount_branch line 60
7. lemma OAI.HyperbolicObstruction.StarModel.expect_starCount_leaf line 80
8. lemma OAI.HyperbolicObstruction.StarModel.extensionMean_pos line 97
9. lemma OAI.HyperbolicObstruction.StarModel.starMean_pos line 108