OAI/Combinatorics/EuclideanRamsey/TensorNecessity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EuclideanRamsey.sum_floor_bounds line 13
  2. theorem OAI.EuclideanRamsey.floor_coloring_obstruction line 26
  3. abbrev OAI.EuclideanRamsey.RealTensor line 67
  4. abbrev OAI.EuclideanRamsey.RealArray line 68
  5. abbrev OAI.EuclideanRamsey.SeparationSpace line 69
  6. def OAI.EuclideanRamsey.realAugmented line 71
  7. def OAI.EuclideanRamsey.arrayEvaluation line 75
  8. def OAI.EuclideanRamsey.spatialMultiply line 85
  9. def OAI.EuclideanRamsey.arrayMap line 94
  10. def OAI.EuclideanRamsey.RealCriterion line 98
  11. theorem OAI.EuclideanRamsey.separate_arrayMap line 101
  12. def OAI.EuclideanRamsey.diagonalArray line 128
  13. def OAI.EuclideanRamsey.gradientRankOne line 132
  14. def OAI.EuclideanRamsey.affineEvaluation line 135
  15. lemma OAI.EuclideanRamsey.arrayEvaluation_diagonal line 138
  16. lemma OAI.EuclideanRamsey.spatialMultiply_diagonal line 151
  17. theorem OAI.EuclideanRamsey.exists_separated_functions line 157
  18. def OAI.EuclideanRamsey.isometryRows line 186
  19. lemma OAI.EuclideanRamsey.isometryRows_apply line 189
  20. lemma OAI.EuclideanRamsey.isometryRows_gram line 198
  21. theorem OAI.EuclideanRamsey.separated_copy_sum line 206
  22. theorem OAI.EuclideanRamsey.ramsey_realCriterion line 227