OAI/Combinatorics/SparsestCut/DirectionAsymptotics.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.DirectionAsymptotics.grid_card_bound line 14
2. lemma OAI.UniformSparsestCut.DirectionAsymptotics.polynomial_exp_tendsto_zero line 31
3. lemma OAI.UniformSparsestCut.DirectionAsymptotics.large_fourier_exponent line 37
4. lemma OAI.UniformSparsestCut.DirectionAsymptotics.large_chart_exponent line 46
5. lemma OAI.UniformSparsestCut.DirectionAsymptotics.selection_majorant_tendsto line 52
6. lemma OAI.UniformSparsestCut.DirectionAsymptotics.eventual_selection_majorant line 64
7. lemma OAI.UniformSparsestCut.DirectionAsymptotics.normalized_fourier_exponent line 69
8. lemma OAI.UniformSparsestCut.DirectionAsymptotics.normalized_covariance_exponent line 78
9. lemma OAI.UniformSparsestCut.DirectionAsymptotics.probability_majorization line 84
10. lemma OAI.UniformSparsestCut.DirectionAsymptotics.projection_failure_bound line 125
11. lemma OAI.UniformSparsestCut.DirectionAsymptotics.eventual_bias_bound line 141
12. lemma OAI.UniformSparsestCut.DirectionAsymptotics.scalar_net_error line 153
13. lemma OAI.UniformSparsestCut.DirectionAsymptotics.covariance_net_error line 184
14. lemma OAI.UniformSparsestCut.DirectionAsymptotics.projection_net_error line 196