OAI/Analysis/LpDimension/ConvexRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.independent_of_affine_sum line 12
2. lemma OAI.SubpolynomialLp.hyperplane_convex_representation line 24
3. lemma OAI.SubpolynomialLp.compact_convexHull_hyperplane line 40
4. lemma OAI.SubpolynomialLp.normalized_integral_mem line 71