OAI/Combinatorics/GraphSpectrum/SampledChromatic.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Colin de Verdiere matrix definitions and chromatic bounds for graphs sampled from a binary hole relation.

  1. def OAI.CdV.WellSigned line 13
  2. def OAI.CdV.OneNegativeEigenvalue line 17
  3. def OAI.CdV.StrongArnold line 22
  4. def OAI.CdV.nullity line 26
  5. def OAI.CdV.Admissible line 29
  6. def OAI.CdV.admissibleNullities line 32
  7. def OAI.CdV.mu line 35
  8. def OAI.CdV.chi line 37
  9. def OAI.CdV.ChromaticConjecture line 39
  10. lemma OAI.CdV.rank_add_nullity line 43
  11. lemma OAI.CdV.nullity_le_card line 48
  12. lemma OAI.CdV.admissibleNullities_bddAbove line 52
  13. lemma OAI.CdV.nullity_le_mu line 58
  14. lemma OAI.CdV.mu_le_card line 62
  15. lemma OAI.CdV.exists_nullity_eq_mu line 67
  16. lemma OAI.CdV.strongArnold_of_isUnit line 74
  17. lemma OAI.CdV.neg_card_of_trace line 83
  18. def OAI.CdV.seedMatrix line 119
  19. lemma OAI.CdV.seedMatrix_isSymm line 124
  20. lemma OAI.CdV.seedMatrix_diag line 130
  21. lemma OAI.CdV.seedMatrix_offDiag line 137
  22. lemma OAI.CdV.seedMatrix_offDiag_norm_sum line 144
  23. lemma OAI.CdV.seedMatrix_trace line 156
  24. lemma OAI.CdV.seedMatrix_neg_eigenvalues line 168
  25. lemma OAI.CdV.seedMatrix_isUnit line 204
  26. lemma OAI.CdV.exists_admissible line 215
  27. lemma OAI.CdV.admissibleNullities_nonempty line 237
  28. lemma OAI.CdV.exists_maximizing_admissible line 242
  29. def OAI.CdV.RankObstruction line 246
  30. lemma OAI.CdV.mu_gap_of_rankObstruction line 250
  31. lemma OAI.CdV.chi_colorable line 261
  32. lemma OAI.CdV.card_le_indepNum_mul_chi line 266
  33. lemma OAI.CdV.half_order_le_chi line 285
  34. lemma OAI.CdV.indepNum_le_two_of_no_independent_triple line 293
  35. lemma OAI.CdV.inequalities_of_rankObstruction line 305
  36. lemma OAI.CdV.not_chromaticConjecture_of_gap line 311
  37. def OAI.CdV.cliqueBlowup line 321
  38. lemma OAI.CdV.indepNum_cliqueBlowup_le line 329
  39. lemma OAI.CdV.indepNum_cliqueBlowup line 348
  40. lemma OAI.CdV.cliqueBlowup_independence_and_colouring line 368
  41. abbrev OAI.CdV.Geometry.F line 378
  42. def OAI.CdV.Geometry.Hole line 383
  43. lemma OAI.CdV.Geometry.hole_symm line 393
  44. lemma OAI.CdV.Geometry.hole_irrefl line 397
  45. lemma OAI.CdV.Geometry.hole_triangle_free line 404
  46. def OAI.CdV.Geometry.sampledGraph line 435
  47. lemma OAI.CdV.Geometry.sampledGraph_adj_of_same_type line 443
  48. lemma OAI.CdV.Geometry.sampledGraph_indepNum_le_two line 451
  49. lemma OAI.CdV.Geometry.sampledGraph_half_order_le_chi line 468