OAI/Combinatorics/SparsestCut/GradientBudget.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.GradientBudget.directional_control line 16
2. lemma OAI.UniformSparsestCut.GradientBudget.good_chart_average line 43
3. lemma OAI.UniformSparsestCut.GradientBudget.total_gradient line 60
4. def OAI.UniformSparsestCut.ConvolutionBounds.smooth line 92
5. lemma OAI.UniformSparsestCut.ConvolutionBounds.smooth_eq line 96
6. lemma OAI.UniformSparsestCut.ConvolutionBounds.smooth_deriv line 99
7. lemma OAI.UniformSparsestCut.ConvolutionBounds.smooth_deriv_integrable line 109
8. lemma OAI.UniformSparsestCut.ConvolutionBounds.integral_l1_bound line 118
9. lemma OAI.UniformSparsestCut.ConvolutionBounds.mismatch line 127
10. lemma OAI.UniformSparsestCut.ConvolutionBounds.error line 157
11. def OAI.UniformSparsestCut.GradientCalculus.vector line 191
12. lemma OAI.UniformSparsestCut.GradientCalculus.vector_norm line 192
13. lemma OAI.UniformSparsestCut.GradientCalculus.vector_inner line 194
14. lemma OAI.UniformSparsestCut.GradientCalculus.vector_coordinate line 196
15. lemma OAI.UniformSparsestCut.GradientCalculus.norm_le_partials line 200
16. lemma OAI.UniformSparsestCut.GradientCalculus.vector_representation line 209
17. lemma OAI.UniformSparsestCut.GradientCalculus.gradient_mismatch line 215
18. lemma OAI.UniformSparsestCut.GradientCalculus.gradient_budget line 239