OAI/Analysis/DiamondDistortion/HeadProjections.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiamondDistortion.LpCut.linear line 17
2. lemma OAI.DiamondDistortion.LpCut.linear_apply line 24
3. lemma OAI.DiamondDistortion.LpCut.norm_linear line 26
4. def OAI.DiamondDistortion.LpCut.continuous line 31
5. lemma OAI.DiamondDistortion.LpCut.continuous_apply line 33
6. lemma OAI.DiamondDistortion.RecursiveModel.ancestors_linear line 38
7. lemma OAI.DiamondDistortion.RecursiveModel.ancestral_prefix line 65
8. lemma OAI.DiamondDistortion.PathModel.cut_branch line 91
9. lemma OAI.DiamondDistortion.PathModel.branch_cost line 113
10. lemma OAI.DiamondDistortion.PathModel.linear_cost_cut line 121
11. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_nested line 160
12. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_nested_right line 168
13. instance OAI.DiamondDistortion.RecursiveModel.(instance at line 175) line 175
14. lemma OAI.DiamondDistortion.RecursiveModel.head_upper line 176
15. lemma OAI.DiamondDistortion.RecursiveModel.head_nonempty line 183
16. lemma OAI.DiamondDistortion.PathModel.linear_forest_cut line 188
17. lemma OAI.DiamondDistortion.PathModel.linear_projection_contractive line 206