OAI/Combinatorics/SparsestCut/DirectionFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.DirectionFamily.normBounds_of_not_bad line 18
2. lemma OAI.UniformSparsestCut.DirectionFamily.inner_empiricalSin line 24
3. lemma OAI.UniformSparsestCut.DirectionFamily.net_fourier_scalar line 37
4. lemma OAI.UniformSparsestCut.DirectionFamily.net_covariance_scalar line 53
5. lemma OAI.UniformSparsestCut.DirectionFamily.source_nets line 66
6. lemma OAI.UniformSparsestCut.DirectionFamily.select_source_nets line 91
7. lemma OAI.UniformSparsestCut.DirectionFamily.badCount_le_of_imp line 114
8. lemma OAI.UniformSparsestCut.DirectionFamily.good_chart_interpolation line 122
9. structure OAI.UniformSparsestCut.DirectionFamily.Family line 138
10. lemma OAI.UniformSparsestCut.DirectionFamily.family_at_large line 148
11. theorem OAI.UniformSparsestCut.DirectionFamily.directions_exist line 190