OAI/Combinatorics/EuclideanRamsey/CorrectionPaths.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.GradedPaths.maxCost line 35
  2. lemma OAI.EuclideanRamsey.GradedPaths.single_le_maxCost line 36
  3. def OAI.EuclideanRamsey.GradedPaths.normalCost line 38
  4. lemma OAI.EuclideanRamsey.GradedPaths.prod_single_eq line 61
  5. lemma OAI.EuclideanRamsey.GradedPaths.bounded_tuple line 74
  6. lemma OAI.EuclideanRamsey.GradedPaths.correction_cost line 86
  7. lemma OAI.EuclideanRamsey.OrbitWords.path line 105
  8. theorem OAI.EuclideanRamsey.averaged_equal_endpoints line 114
  9. def OAI.EuclideanRamsey.permute line 164
  10. lemma OAI.EuclideanRamsey.permute_apply line 167
  11. lemma OAI.EuclideanRamsey.permute_mul line 169
  12. lemma OAI.EuclideanRamsey.permute_one line 171
  13. theorem OAI.EuclideanRamsey.permutation_equal_endpoints line 174