OAI/Analysis/LpDimension/GridObstruction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubpolynomialLp.rowVector line 15
  2. def OAI.SubpolynomialLp.colVector line 16
  3. abbrev OAI.SubpolynomialLp.GridIndex line 17
  4. def OAI.SubpolynomialLp.gridVector line 18
  5. lemma OAI.SubpolynomialLp.row_disjoint line 26
  6. lemma OAI.SubpolynomialLp.col_disjoint line 34
  7. lemma OAI.SubpolynomialLp.row_col_not_disjoint line 42
  8. lemma OAI.SubpolynomialLp.grid_dimension_obstruction line 47
  9. lemma OAI.SubpolynomialLp.finite_memLp line 98
  10. def OAI.SubpolynomialLp.finiteToLp line 101
  11. lemma OAI.SubpolynomialLp.finiteToLp_sub line 104
  12. lemma OAI.SubpolynomialLp.finiteToLp_injective line 108
  13. lemma OAI.SubpolynomialLp.finiteToLp_norm line 115
  14. lemma OAI.SubpolynomialLp.finiteToLp_infinite line 123
  15. lemma OAI.SubpolynomialLp.finite_extend_card line 130
  16. lemma OAI.SubpolynomialLp.GoodDimension.finite_family line 141
  17. lemma OAI.SubpolynomialLp.coordinateDistance_rpow line 161
  18. lemma OAI.SubpolynomialLp.finiteToLp_norm_rpow line 167
  19. lemma OAI.SubpolynomialLp.exact_lower_of_goodDimension line 175