OAI/Combinatorics/SparsestCut/CubeGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.CubeGeometry.pi_uniform line 18
2. lemma OAI.UniformSparsestCut.CubeGeometry.cube_ac line 28
3. lemma OAI.UniformSparsestCut.CubeGeometry.uniform_mem line 36
4. lemma OAI.UniformSparsestCut.CubeGeometry.cube_mem line 41
5. lemma OAI.UniformSparsestCut.CubeGeometry.uniform_pow line 49
6. lemma OAI.UniformSparsestCut.CubeGeometry.uniform_pow_integrable line 56
7. lemma OAI.UniformSparsestCut.CubeGeometry.coordinate_preserving line 62
8. lemma OAI.UniformSparsestCut.CubeGeometry.coordinate_pow line 67
9. lemma OAI.UniformSparsestCut.CubeGeometry.coordinate_pow_integrable line 72
10. lemma OAI.UniformSparsestCut.CubeGeometry.cube_norm line 75
11. lemma OAI.UniformSparsestCut.CubeGeometry.bounded_integrable line 87
12. lemma OAI.UniformSparsestCut.CubeGeometry.pair_norm_bound line 91
13. lemma OAI.UniformSparsestCut.CubeGeometry.pair_norm_integrable line 100
14. lemma OAI.UniformSparsestCut.CubeGeometry.coordinate_difference_sq line 104
15. lemma OAI.UniformSparsestCut.CubeGeometry.coordinate_difference_sq_integrable line 125
16. lemma OAI.UniformSparsestCut.CubeGeometry.pair_norm_sq_integral line 134
17. lemma OAI.UniformSparsestCut.CubeGeometry.pair_norm_average line 145