OAI/Combinatorics/SparsestCut/DirectionInterpolation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformSparsestCut.DirectionInterpolation.empiricalSin line 16
2. def OAI.UniformSparsestCut.DirectionInterpolation.empiricalCov line 18
3. lemma OAI.UniformSparsestCut.DirectionInterpolation.sin_vector_lipschitz line 21
4. lemma OAI.UniformSparsestCut.DirectionInterpolation.empiricalSin_lipschitz line 34
5. lemma OAI.UniformSparsestCut.DirectionInterpolation.gaussian_norm_sq_mean line 49
6. lemma OAI.UniformSparsestCut.DirectionInterpolation.gaussianTransform_lipschitz line 58
7. lemma OAI.UniformSparsestCut.DirectionInterpolation.covariance_lipschitz line 71
8. lemma OAI.UniformSparsestCut.DirectionInterpolation.covariance_net_bound line 94
9. lemma OAI.UniformSparsestCut.DirectionInterpolation.fourier_net_bound line 106
10. lemma OAI.UniformSparsestCut.DirectionInterpolation.projection_interpolate line 137