Dev/MonadicDependence/BipartiteRamsey/Contract.lean
| 1 | import Mathlib.Data.Finset.Card |
| 2 | import Mathlib.Order.Monotone.Basic |
| 3 | import Catalog.Sparsity.Preliminaries.Contract |
| 4 | |
| 5 | namespace Dev.MonadicDependence.BipartiteRamsey |
| 6 | |
| 7 | /-- Order type of a tuple `a : Fin ℓ → V` (`V` linearly ordered). For |
| 8 | each pair `(i, j) : Fin ℓ × Fin ℓ`, records whether `a i < a j`, |
| 9 | `a i = a j`, or `a i > a j`. Mählmann p. 28 writes this as `otp(a)`. -/ |
| 10 | def orderType {V : Type*} [LinearOrder V] {ℓ : ℕ} (a : Fin ℓ → V) : |
| 11 | Fin ℓ × Fin ℓ → Ordering := |
| 12 | fun p => compare (a p.1) (a p.2) |
| 13 | |
| 14 | /-- Mählmann Lemma 4.15 (Bipartite Ramsey). For every `k, ℓ₁, ℓ₂ : ℕ` |
| 15 | there exists a monotone, unbounded function `U : ℕ → ℕ` (depending only |
| 16 | on `k, ℓ₁, ℓ₂`) such that, for every `n` and every coloring |
| 17 | `c : (Fin ℓ₁ → Fin n) → (Fin ℓ₂ → Fin n) → Fin k`, there exist |
| 18 | `I₁, I₂ : Finset (Fin n)` with `U n ≤ |I₁|`, `U n ≤ |I₂|`, and a |
| 19 | function |
| 20 | `f : (Fin ℓ₁ × Fin ℓ₁ → Ordering) → (Fin ℓ₂ × Fin ℓ₂ → Ordering) → Fin k` |
| 21 | such that `c a b = f (orderType a) (orderType b)` whenever every |
| 22 | coordinate of `a` lies in `I₁` and every coordinate of `b` in `I₂`. -/ |
| 23 | axiom bipartiteRamsey (k ℓ₁ ℓ₂ : ℕ) (hk : 0 < k) : |
| 24 | ∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧ |
| 25 | ∀ (n : ℕ) (c : (Fin ℓ₁ → Fin n) → (Fin ℓ₂ → Fin n) → Fin k), |
| 26 | ∃ I₁ I₂ : Finset (Fin n), |
| 27 | U n ≤ I₁.card ∧ U n ≤ I₂.card ∧ |
| 28 | ∃ f : (Fin ℓ₁ × Fin ℓ₁ → Ordering) → |
| 29 | (Fin ℓ₂ × Fin ℓ₂ → Ordering) → Fin k, |
| 30 | ∀ (a : Fin ℓ₁ → Fin n) (b : Fin ℓ₂ → Fin n), |
| 31 | (∀ i, a i ∈ I₁) → (∀ j, b j ∈ I₂) → |
| 32 | c a b = f (orderType a) (orderType b) |
| 33 | |
| 34 | end Dev.MonadicDependence.BipartiteRamsey |
| 35 |