OAI/Combinatorics/SparsestCut/ChartLinear.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.ChartLinear.gram_injective line 17
2. def OAI.UniformSparsestCut.ChartLinear.gramEquiv line 29
3. def OAI.UniformSparsestCut.ChartLinear.pseudoInverse line 36
4. lemma OAI.UniformSparsestCut.ChartLinear.pseudoInverse_comp line 40
5. lemma OAI.UniformSparsestCut.ChartLinear.gramInverse_norm line 45
6. lemma OAI.UniformSparsestCut.ChartLinear.pseudoInverse_equation line 61
7. lemma OAI.UniformSparsestCut.ChartLinear.residual_orthogonal line 66
8. lemma OAI.UniformSparsestCut.ChartLinear.residual_pythagoras line 72
9. lemma OAI.UniformSparsestCut.ChartLinear.pseudoInverse_norm line 79
10. lemma OAI.UniformSparsestCut.ChartLinear.residual_norm line 89
11. lemma OAI.UniformSparsestCut.ChartLinear.pseudoInverse_column line 96
12. def OAI.UniformSparsestCut.FrameCharts.chart line 109
13. lemma OAI.UniformSparsestCut.FrameCharts.chart_apply line 113
14. lemma OAI.UniformSparsestCut.FrameCharts.chart_energy line 116
15. lemma OAI.UniformSparsestCut.FrameCharts.chart_adjoint_single line 121
16. lemma OAI.UniformSparsestCut.FrameCharts.extend_covariance line 130
17. lemma OAI.UniformSparsestCut.FrameCharts.normalized_energy line 163
18. lemma OAI.UniformSparsestCut.FrameCharts.normalized_bounds line 170
19. lemma OAI.UniformSparsestCut.FrameCharts.normalized_norms line 188