OAI/Analysis/LpDimension/GradientSampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.below_error_algebra line 12
2. lemma OAI.SubpolynomialLp.stable_gradient_weighted line 30
3. lemma OAI.SubpolynomialLp.moment_integral_mem line 68
4. lemma OAI.SubpolynomialLp.weighted_gradient_samples line 83
5. instance OAI.SubpolynomialLp.pairIndexDecidableEq line 119
6. lemma OAI.SubpolynomialLp.pairIndex_nonempty line 123
7. lemma OAI.SubpolynomialLp.pairIndex_connected line 126
8. lemma OAI.SubpolynomialLp.pairIndex_incident line 132
9. lemma OAI.SubpolynomialLp.normalizedGradient_apply line 148
10. lemma OAI.SubpolynomialLp.normalized_coordinate_gradient line 155
11. lemma OAI.SubpolynomialLp.sampled_labels_embedding line 171
12. lemma OAI.SubpolynomialLp.distortion_ratio line 219