Catalog/Sparsity/BipartiteRamsey/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 2 | import Catalog.Sparsity.ShallowTopologicalMinor.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.BipartiteRamsey |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 7 | |
| 8 | /-- Lemma 3.9: in a bipartite graph with sides `A` and `B`, if `|A|` is large |
| 9 | enough (as a function of `m`, `t`, `d`), then at least one of the following |
| 10 | holds: |
| 11 | (a) `A` contains `m` vertices with no common neighbor, |
| 12 | (b) `G` contains a `1`-subdivision of `K_t` with principal vertices in `A`, |
| 13 | (c) `B` contains a vertex of degree at least `d`. -/ |
| 14 | axiom bipartiteRamsey (m t d : ℕ) : |
| 15 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 16 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 17 | (A B : Finset V), |
| 18 | Disjoint A B → |
| 19 | (∀ u v, G.Adj u v → (u ∈ A ∧ v ∈ B) ∨ (u ∈ B ∧ v ∈ A)) → |
| 20 | N ≤ A.card → |
| 21 | (∃ A' : Finset V, A' ⊆ A ∧ m ≤ A'.card ∧ |
| 22 | (↑A' : Set V).Pairwise (fun u v => |
| 23 | ∀ w, ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 24 | (∃ M : ShallowTopologicalMinorModel |
| 25 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 26 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 27 | (∃ v ∈ B, d ≤ (G.neighborFinset v ∩ A).card) |
| 28 | |
| 29 | end Catalog.Sparsity.BipartiteRamsey |
| 30 |