OAI/Combinatorics/SparsestCut/PivotFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.PivotFamily.standard_density_le_one line 16
2. lemma OAI.UniformSparsestCut.PivotFamily.standard_small_ball line 24
3. lemma OAI.UniformSparsestCut.PivotFamily.coordinate_small_ball line 37
4. lemma OAI.UniformSparsestCut.PivotFamily.all_coordinate_small_ball line 52
5. theorem OAI.UniformSparsestCut.PivotFamily.select_on_nets_extra line 69
6. lemma OAI.UniformSparsestCut.PivotFamily.select_source_nets_pivot line 112
7. structure OAI.UniformSparsestCut.PivotFamily.PFamily line 146
8. lemma OAI.UniformSparsestCut.PivotFamily.pivot_family_at_large line 149
9. lemma OAI.UniformSparsestCut.PivotFamily.pivot_majorant_tendsto line 191
10. theorem OAI.UniformSparsestCut.PivotFamily.pivot_directions_exist line 200