OAI/Analysis/LpDimension/Sampling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.bounded_sample_exists line 12
2. lemma OAI.SubpolynomialLp.sample_convexHull line 84
3. lemma OAI.SubpolynomialLp.weighted_moments_samples line 110
4. lemma OAI.SubpolynomialLp.controlled_retraction_bounds line 142