OAI/Analysis/LpDimension/Packing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.packing_card_bound line 14
2. lemma OAI.SubpolynomialLp.packing_family_bound line 55
3. lemma OAI.SubpolynomialLp.coordinateDistance_norm line 75
4. lemma OAI.SubpolynomialLp.equilateral_lp line 82
5. lemma OAI.SubpolynomialLp.packing_lower_of_goodDimension line 108
6. lemma OAI.SubpolynomialLp.exact_goodDimension line 151
7. lemma OAI.SubpolynomialLp.GoodDimension.mono_distortion line 159
8. lemma OAI.SubpolynomialLp.dimension_good line 166
9. lemma OAI.SubpolynomialLp.dimension_le_exact line 171
10. lemma OAI.SubpolynomialLp.exact_dimension_bounds line 176
11. lemma OAI.SubpolynomialLp.quadratic_growth_log_limit line 183
12. lemma OAI.SubpolynomialLp.exact_dimension_log_limit line 225
13. lemma OAI.SubpolynomialLp.dimension_packing_lower line 236