OAI/Combinatorics/IndependentSets/PCP/LabelCoverData.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LargeIndependentSets.LabelCoverData line 9
  2. def OAI.LargeIndependentSets.LabelCoverData.Satisfied line 14
  3. def OAI.LargeIndependentSets.MixedTuple line 18
  4. def OAI.LargeIndependentSets.MixedTuple.map line 21
  5. def OAI.LargeIndependentSets.mixedProject line 27
  6. abbrev OAI.LargeIndependentSets.LayerQuestion line 39
  7. abbrev OAI.LargeIndependentSets.LayerAnswer line 42
  8. inductive OAI.LargeIndependentSets.LayerImposed line 45
  9. def OAI.LargeIndependentSets.layeredSystem line 54
  10. def OAI.LargeIndependentSets.productLabeling line 58
  11. theorem OAI.LargeIndependentSets.productLabeling_consistent line 62
  12. theorem OAI.LargeIndependentSets.layered_completeness line 78
  13. def OAI.LargeIndependentSets.distanceBump line 92
  14. lemma OAI.LargeIndependentSets.distanceBump_bounds line 95
  15. lemma OAI.LargeIndependentSets.distanceBump_zero line 103
  16. lemma OAI.LargeIndependentSets.distanceBump_vanish line 106
  17. lemma OAI.LargeIndependentSets.distanceBump_difference line 115
  18. def OAI.LargeIndependentSets.setBump line 140
  19. lemma OAI.LargeIndependentSets.setBump_lipschitz line 143
  20. def OAI.LargeIndependentSets.oddBump line 156
  21. lemma OAI.LargeIndependentSets.oddBump_bounds line 159
  22. lemma OAI.LargeIndependentSets.oddBump_odd line 166
  23. lemma OAI.LargeIndependentSets.oddBump_lipschitz line 172
  24. lemma OAI.LargeIndependentSets.oddBump_eq_one line 178
  25. lemma OAI.LargeIndependentSets.linkLength_le_copyLength line 191
  26. lemma OAI.LargeIndependentSets.grid_independent_separation line 198
  27. def OAI.LargeIndependentSets.gridBump line 214
  28. theorem OAI.LargeIndependentSets.grid_independent_bump line 220
  29. def OAI.LargeIndependentSets.finiteMcShane line 265
  30. lemma OAI.LargeIndependentSets.finiteMcShane_le line 269
  31. lemma OAI.LargeIndependentSets.finiteMcShane_on_grid line 274
  32. lemma OAI.LargeIndependentSets.finiteMcShane_lipschitz line 285
  33. def OAI.LargeIndependentSets.clipUnit line 304
  34. lemma OAI.LargeIndependentSets.clipUnit_bounds line 306
  35. lemma OAI.LargeIndependentSets.clipUnit_eq line 309
  36. lemma OAI.LargeIndependentSets.clipUnit_lipschitz line 312
  37. def OAI.LargeIndependentSets.finiteOddExtension line 315
  38. lemma OAI.LargeIndependentSets.finiteOddExtension_bounds line 319
  39. lemma OAI.LargeIndependentSets.finiteOddExtension_odd line 327
  40. lemma OAI.LargeIndependentSets.finiteOddExtension_on_grid line 334
  41. lemma OAI.LargeIndependentSets.finiteOddExtension_lipschitz line 345
  42. def OAI.LargeIndependentSets.torusAntipode line 360
  43. lemma OAI.LargeIndependentSets.torusAntipode_involutive line 363
  44. lemma OAI.LargeIndependentSets.torusAntipode_isometry line 370
  45. def OAI.LargeIndependentSets.torusGrid line 375
  46. lemma OAI.LargeIndependentSets.torusGrid_antipode line 378
  47. def OAI.LargeIndependentSets.tupleExtension line 385
  48. lemma OAI.LargeIndependentSets.tupleExtension_bounds line 391