Homogeneous rectangles for colorings of pairs of tuples
Lax185574.BipartiteHomogeneity · concepts/Lax185574/BipartiteHomogeneity.lean · lax-185574
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
For a tuple ā = (a₁, …, a_ℓ) ∈ [n]^ℓ, the order type otp(ā) of ā is the atomic type of ā in the ordered set ([n], ≤). It stores, for each i, j ∈ [ℓ], whether aᵢ < aⱼ, aᵢ = aⱼ or aᵢ > aⱼ.
For every k, ℓ ∈ ℕ there is an unbounded, non-decreasing function U_{k,ℓ} : ℕ → ℕ with the following property. For every t ∈ ℕ and coloring
c : [t]^ℓ × [t]^ℓ → [k]
there are subsets I, J ⊆ [t] of size U_{k,ℓ}(t) such that c(ā, b̄) only depends on otp(ā) and otp(b̄), for all ā ∈ I^ℓ and b̄ ∈ J^ℓ.
This is a version of Ramsey's theorem, see Lemma 4.4 of the cited work on flip-breakability.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
In the paper
- page 60 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.Card |
| 2 | import Mathlib.Order.Monotone.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Homogeneous rectangles for colorings of pairs of tuples |
| 7 | type: lemma |
| 8 | --- |
| 9 | For a tuple ā = (a₁, …, a_ℓ) ∈ [n]^ℓ, the *order type* otp(ā) of ā is |
| 10 | the atomic type of ā in the ordered set ([n], ≤). It stores, for each |
| 11 | i, j ∈ [ℓ], whether aᵢ < aⱼ, aᵢ = aⱼ or aᵢ > aⱼ. |
| 12 | |
| 13 | For every k, ℓ ∈ ℕ there is an unbounded, non-decreasing function |
| 14 | U_{k,ℓ} : ℕ → ℕ with the following property. For every t ∈ ℕ and |
| 15 | coloring |
| 16 | |
| 17 | c : [t]^ℓ × [t]^ℓ → [k] |
| 18 | |
| 19 | there are subsets I, J ⊆ [t] of size U_{k,ℓ}(t) such that c(ā, b̄) only |
| 20 | depends on otp(ā) and otp(b̄), for all ā ∈ I^ℓ and b̄ ∈ J^ℓ. |
| 21 | |
| 22 | This is a version of Ramsey's theorem, see Lemma 4.4 of the cited work |
| 23 | on flip-breakability. |
| 24 | |
| 25 | # Formalization notes |
| 26 | |
| 27 | The set [t] is `Fin t`, with the same order, and the colors [k] are |
| 28 | `Fin k`. The order type of a tuple records `compare` for every pair of |
| 29 | positions. "c(ā, b̄) only depends on otp(ā) and otp(b̄)" says that any |
| 30 | two pairs of tuples from I^ℓ × J^ℓ with the same order types get the |
| 31 | same color. Unboundedness says that every value is reached. The sets |
| 32 | I and J have exactly U_{k,ℓ}(t) elements. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax185574.BipartiteHomogeneity |
| 36 | |
| 37 | /-- The order type `otp(ā)` of a tuple of elements of `[t]`: the |
| 38 | comparison of every pair of its entries. -/ |
| 39 | def orderType {ℓ t : ℕ} (a : Fin ℓ → Fin t) : Fin ℓ → Fin ℓ → Ordering := |
| 40 | fun i j => compare (a i) (a j) |
| 41 | |
| 42 | /-- **Homogeneous rectangles.** Every coloring of pairs of |
| 43 | `ℓ`-tuples from `[t]` with `k` colors is determined by the order types |
| 44 | on `I^ℓ × J^ℓ`, for some sets `I` and `J` of size `U_{k,ℓ}(t)`, where |
| 45 | `U_{k,ℓ}` is unbounded and non-decreasing. -/ |
| 46 | axiom exists_orderType_homogeneous (k ℓ : ℕ) : |
| 47 | ∃ U : ℕ → ℕ, Monotone U ∧ (∀ m : ℕ, ∃ t : ℕ, m ≤ U t) ∧ |
| 48 | ∀ (t : ℕ) (c : (Fin ℓ → Fin t) → (Fin ℓ → Fin t) → Fin k), |
| 49 | ∃ I J : Finset (Fin t), I.card = U t ∧ J.card = U t ∧ |
| 50 | ∀ a a' b b' : Fin ℓ → Fin t, |
| 51 | (∀ i, a i ∈ I) → (∀ i, a' i ∈ I) → (∀ i, b i ∈ J) → (∀ i, b' i ∈ J) → |
| 52 | orderType a = orderType a' → orderType b = orderType b' → |
| 53 | c a b = c a' b' |
| 54 | |
| 55 | end Lax185574.BipartiteHomogeneity |
| 56 |
Formalization notes
The set [t] is , with the same order, and the colors [k] are . The order type of a tuple records for every pair of positions. "c(ā, b̄) only depends on otp(ā) and otp(b̄)" says that any two pairs of tuples from I^ℓ × J^ℓ with the same order types get the same color. Unboundedness says that every value is reached. The sets I and J have exactly U_{k,ℓ}(t) elements.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments