OAI/Combinatorics/Ramsey/Hypercube.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite Ramsey bounds, cross-edge colorings, and counterexample sequences for a proposed linear hypercube Ramsey bound.

  1. abbrev OAI.HypercubeRamsey.CubeVertex line 9
  2. def OAI.HypercubeRamsey.cube line 11
  3. def OAI.HypercubeRamsey.RamseyProperty line 16
  4. def OAI.HypercubeRamsey.ramseyNumber line 19
  5. theorem OAI.HypercubeRamsey.finite_clique_ramsey line 24
  6. theorem OAI.HypercubeRamsey.copy_of_clique line 73
  7. theorem OAI.HypercubeRamsey.ramseyProperty_exp_bound line 85
  8. theorem OAI.HypercubeRamsey.ramsey_set_nonempty line 93
  9. theorem OAI.HypercubeRamsey.ramseyNumber_spec line 97
  10. theorem OAI.HypercubeRamsey.ramseyNumber_le line 101
  11. theorem OAI.HypercubeRamsey.ramseyNumber_exp_bound line 105
  12. theorem OAI.HypercubeRamsey.ramseyNumber_mono line 109
  13. theorem OAI.HypercubeRamsey.card_le_ramseyNumber line 120
  14. theorem OAI.HypercubeRamsey.coloring_below_ramsey line 128
  15. theorem OAI.HypercubeRamsey.card_cubeVertex line 135
  16. theorem OAI.HypercubeRamsey.elementary_cube_bounds line 138
  17. theorem OAI.HypercubeRamsey.ramseyNumber_cube_zero line 145
  18. def OAI.HypercubeRamsey.crossGraph line 155
  19. def OAI.HypercubeRamsey.redCrossCopy line 163
  20. def OAI.HypercubeRamsey.blueCrossCopy line 180
  21. def OAI.HypercubeRamsey.splitEmbedding line 198
  22. theorem OAI.HypercubeRamsey.cross_coloring_below_ramsey line 201
  23. theorem OAI.HypercubeRamsey.large_cube_of_not_linear line 214
  24. theorem OAI.HypercubeRamsey.counterexample_sequence_of_not_linear line 244