Grace/Cumulus/Combinatorics/RamseyInfinite.g17

Open in Workbench Download source

Imports

RamseyChain

Declarations

Source

1-- The infinite Ramsey theorem: for every n, every infinite set S, and every2-- colouring of the n-subsets of S with finitely many colours, some infinite3-- H ⊆ S has all its n-subsets of one colour. The chain of stages supplies4-- points a₀, a₁, … with colours c₀, c₁, …; one colour occurs5-- infinitely often, and the points of that colour form H: an6-- (n + 1)-subset of H with least index j is insert(aⱼ, T) for an7-- n-subset T of Sⱼ₊₁.8-- Part of Cumulus, the Grace17 mathematics library.9-- Copyright (c) 2026 Grant Passmore.10-- Released under the Apache License 2.0. See LICENSE in the repository root.11-- Authors: Grant Passmore1213module Grace.Cumulus.Combinatorics.RamseyInfinite14import RamseyChain1516-- The colours and the points of the chain, as graphs on ℕ.1718defgraph ramseyColourMap (C S K : Set, n : Nat) (i ∈ ℕ) : K :=19  ramseyColour(C, S, K, n, i)20requires ramsey : RamseyProperty(n, K)21requires colouring : C : subsetsOfSize(S, n + 1) → K22requires infinite : Infinite(S)23proof24  have iNat := nat.omega.backward with member25  exact ramseyColour.member at C, S, K, n, i with *2627defgraph ramseyPointMap (C S K : Set, n : Nat) (i ∈ ℕ) : S :=28  ramseyPoint(C, S, K, n, i)29requires ramsey : RamseyProperty(n, K)30requires colouring : C : subsetsOfSize(S, n + 1) → K31requires infinite : Infinite(S)32proof33  have iNat := nat.omega.backward with member34  exact ramseyPoint.in_set at C, S, K, n, i with *3536-- The stages whose colour is c, and the points of those stages.3738def ramseyIndices (C S K c : Set, n : Nat) : Set :=39  functionPreimage(ramseyColourMap(C, S, K, n), ℕ, {c})4041theorem ramseyIndices.value (C S K c : Set, n : Nat)42  shows ramseyIndices(C, S, K, c, n) =43    functionPreimage(ramseyColourMap(C, S, K, n), ℕ, {c})44proof45  simp [ramseyIndices]4647def ramseyHomogeneous (C S K c : Set, n : Nat) : Set :=48  functionImage(ramseyPointMap(C, S, K, n), ramseyIndices(C, S, K, c, n), S)4950theorem ramseyHomogeneous.value (C S K c : Set, n : Nat)51  shows ramseyHomogeneous(C, S, K, c, n) =52    functionImage(ramseyPointMap(C, S, K, n), ramseyIndices(C, S, K, c, n), S)53proof54  simp [ramseyHomogeneous]5556-- The indices of colour c whose points lie in U.57def ramseyIndicesOf (C S K c U : Set, n : Nat) : Set :=58  { i ∈ ramseyIndices(C, S, K, c, n) | ramseyPoint(C, S, K, n, i) ∈ U }5960section RamseyInfinite61variable (C S K : Set) (n : Nat)62hypothesis ramsey : RamseyProperty(n, K)63hypothesis colouring : FunctionBetween(C, subsetsOfSize(S, n + 1), K)64hypothesis infinite : Infinite(S)6566theorem ramseyIndices.subset (c : Set)67  shows ramseyIndices(C, S, K, c, n) ⊆ ℕ68proof69  rw ramseyIndices.value70  exact functionPreimage.subset at ramseyColourMap(C, S, K, n), ℕ, {c}7172theorem ramseyIndices.membership (c i : Set)73  shows i ∈ ramseyIndices(C, S, K, c, n) ↔74    i ∈ ℕ ∧ ramseyColour(C, S, K, n, i) = c75proof76  rw ramseyIndices.value77  constructor78  . intro h79    obtain ⟨hi, valueC⟩ := functionPreimage.point_membership.forward with h80    have value := ramseyColourMap.value at C, S, K, n, i with *81    rw value at valueC82    exact ⟨hi, valueC⟩83  . intro h84    obtain ⟨hi, valueC⟩ := h85    have value := ramseyColourMap.value at C, S, K, n, i with *86    apply functionPreimage.point_membership.backward87    rw value88    exact ⟨hi, valueC⟩8990theorem ramseyHomogeneous.subset (c : Set)91  shows ramseyHomogeneous(C, S, K, c, n) ⊆ S92proof93  rw ramseyHomogeneous.value94  exact functionImage.subset at95    ramseyPointMap(C, S, K, n), ramseyIndices(C, S, K, c, n), S9697theorem ramseyHomogeneous.membership (c x : Set)98  shows x ∈ ramseyHomogeneous(C, S, K, c, n) ↔99    ∃ i ∈ ramseyIndices(C, S, K, c, n), x = ramseyPoint(C, S, K, n, i)100proof101  have indices := ramseyIndices.subset at C, S, K, n, c with *102  rw ramseyHomogeneous.value103  constructor104  . intro h105    obtain ⟨_, i, hi, shape⟩ := functionImage.membership.forward with h106    have hiN := indices with i, hi107    have value := ramseyPointMap.value at C, S, K, n, i with *108    rw value at shape109    exact ⟨i, hi, shape⟩110  . intro h111    obtain ⟨i, hi, shape⟩ := h112    have hiN := indices with i, hi113    have iNat := nat.omega.backward with hiN114    have value := ramseyPointMap.value at C, S, K, n, i with *115    have inS := ramseyPoint.in_set at C, S, K, n, i with *116    apply functionImage.membership.backward117    constructor118    . rw shape119      exact inS120    . refine ⟨i, hi, ?_⟩121      rw [shape, value]122      rfl123124-- The points are pairwise distinct, so H is as large as its index set.125theorem ramseyPointMap.injective126  shows InjectiveBetween(ramseyPointMap(C, S, K, n), ℕ, S)127proof128  have graph := ramseyPointMap.function at C, S, K, n with *129  apply Injective.of_pointwise with graph130  intros i hi j hj same131  have iNat := nat.omega.backward with hi132  have jNat := nat.omega.backward with hj133  have valueI := ramseyPointMap.value at C, S, K, n, i with *134  have valueJ := ramseyPointMap.value at C, S, K, n, j with *135  rw [valueI, valueJ] at same136  exact ramseyPoint.injective_on at C, S, K, n, i, j with *137138theorem ramseyHomogeneous.infinite (c : Set)139  requires indicesInfinite : Infinite(ramseyIndices(C, S, K, c, n))140  shows Infinite(ramseyHomogeneous(C, S, K, c, n))141proof142  have injective := ramseyPointMap.injective at C, S, K, n with *143  have graph := ramseyPointMap.function at C, S, K, n with *144  have indices := ramseyIndices.subset at C, S, K, n, c with *145  have restricted := restrict.injective with injective, indices146  have imageInfinite := Infinite.injective_image with147    restricted, indicesInfinite148  have sameImage := functionImage.restrict with graph, indices149  rw sameImage at imageInfinite150  rw ramseyHomogeneous.value151  exact imageInfinite152153-- An (n + 1)-subset U of H whose least index is j is insert(aⱼ, T) for the154-- n-subset T = U ∖ {aⱼ} of Sⱼ₊₁, so its colour is cⱼ = c.155theorem ramseyHomogeneous.colour_of_least (c U : Set) (j : Nat)156  requires hU : U ∈ subsetsOfSize(ramseyHomogeneous(C, S, K, c, n), n + 1)157  requires jIndex : j ∈ ramseyIndices(C, S, K, c, n)158  requires jIn : ramseyPoint(C, S, K, n, j) ∈ U159  requires least : ∀ i ∈ ramseyIndices(C, S, K, c, n),160    ramseyPoint(C, S, K, n, i) ∈ U → j ≤ i161  shows C(U) = c162proof163  have subsetU := subsetsOfSize.subset with hU164  have indices := ramseyIndices.subset at C, S, K, n, c with *165  have jParts := ramseyIndices.membership.forward with jIndex166  have restSubset : U ∖ {ramseyPoint(C, S, K, n, j)} ⊆ ramseyStage(C, S, K, n, j + 1)167    intros x hx168    obtain ⟨xIn, xNe⟩ := difference.singleton_membership.forward with hx169    have xH := subsetU with x, xIn170    obtain ⟨i, hi, shape⟩ := ramseyHomogeneous.membership.forward with xH171    have hiN := indices with i, hi172    have iNat := nat.omega.backward with hiN173    have pointIn : ramseyPoint(C, S, K, n, i) ∈ U174      rw ← shape175      exact xIn176    have jLe := least with i, hi, pointIn177    have jNe : j ≠ i178      intro same179      apply xNe180      cc181    have jLt := Less.of_LessEqual_ne with jLe, jNe182    have later := ramseyPoint.later_member at C, S, K, n, j, i with *183    rw shape184    exact later185  have counted := subsetsOfSize.counted with hU186  have one : n + 1 = succ(n) := add.right_one with *187  rw one at counted188  have restCounted := HasCardinality.remove with counted, jIn189  have restIn := subsetsOfSize.of_subset with restSubset, restCounted190  have law := ramseyColour.law at191    C, S, K, n, U ∖ {ramseyPoint(C, S, K, n, j)}, j with *192  have restored := insert.restore with jIn193  rw restored at law194  rw law195  exact jParts.right196197theorem ramseyHomogeneous.homogeneous (c U : Set)198  requires hU : U ∈ subsetsOfSize(ramseyHomogeneous(C, S, K, c, n), n + 1)199  shows C(U) = c200proof201  have subsetU := subsetsOfSize.subset with hU202  have indices := ramseyIndices.subset at C, S, K, n, c with *203  obtain ⟨u, hu⟩ := subsetsOfSize.exists_member with hU204  have uH := subsetU with u, hu205  obtain ⟨i0, hi0, shape0⟩ := ramseyHomogeneous.membership.forward with uH206  have pointIn0 : ramseyPoint(C, S, K, n, i0) ∈ U207    rw ← shape0208    exact hu209  have candidate : i0 ∈ ramseyIndicesOf(C, S, K, c, U, n) :=210    ramseyIndicesOf.membership.backward with ⟨hi0, pointIn0⟩211  have inhabited : Nonempty(ramseyIndicesOf(C, S, K, c, U, n)) :=212    ⟨i0, candidate⟩213  have naturals : ramseyIndicesOf(C, S, K, c, U, n) ⊆ ℕ214    intros i hi215    have parts := ramseyIndicesOf.membership.forward with hi216    exact indices with i, parts.left217  have jMember := leastNatural.member with inhabited, naturals218  obtain ⟨jIndex, jIn⟩ := ramseyIndicesOf.membership.forward with jMember219  have jN := indices with220    leastNatural(ramseyIndicesOf(C, S, K, c, U, n)), jIndex221  have jNat := nat.omega.backward with jN222  have least : ∀ i ∈ ramseyIndices(C, S, K, c, n),223      ramseyPoint(C, S, K, n, i) ∈ U →224        leastNatural(ramseyIndicesOf(C, S, K, c, U, n)) ≤ i225    intros i hi pointIn226    have iNat := nat.omega.backward with (indices with i, hi)227    have member : i ∈ ramseyIndicesOf(C, S, K, c, U, n) :=228      ramseyIndicesOf.membership.backward with ⟨hi, pointIn⟩229    exact leastNatural.least with inhabited, naturals, member230  exact ramseyHomogeneous.colour_of_least at231    C, S, K, n, c, U, leastNatural(ramseyIndicesOf(C, S, K, c, U, n)) with *232233end RamseyInfinite234235-- The induction on n.236237theorem RamseyProperty.zero (K : Set)238  shows RamseyProperty(0, K)239proof240  intros S C infinite colouring241  have emptyIn : ∅ ∈ subsetsOfSize(S, 0)242    rw subsetsOfSize.zero243    exact singleton.self at ∅244  have value := FunctionBetween.apply_closed with colouring, emptyIn245  refine ⟨S, Subset.reflexive at S, infinite, C(∅), value, ?_⟩246  intros U hU247  rw subsetsOfSize.zero at hU248  have equal := singleton.membership.forward with hU249  rw equal250  rfl251252theorem RamseyProperty.succ (K : Set) (n : Nat)253  requires finite : Finite(K)254  requires ramsey : RamseyProperty(n, K)255  shows RamseyProperty(n + 1, K)256proof257  intros S C infinite colouring258  have colourGraph := ramseyColourMap.function at C, S, K, n with *259  have omegaInfinite : Infinite(ℕ) := omega.infinite260  obtain ⟨c, hc, indicesInfinite⟩ :=261    pigeonhole.infinite_fiber with colourGraph, omegaInfinite, finite262  rw ← ramseyIndices.value at indicesInfinite263  have subset := ramseyHomogeneous.subset at C, S, K, n, c with *264  have hInfinite := ramseyHomogeneous.infinite at C, S, K, n, c with *265  refine ⟨ramseyHomogeneous(C, S, K, c, n), subset, hInfinite, c, hc, ?_⟩266  intros U hU267  exact ramseyHomogeneous.homogeneous at C, S, K, n, c, U with *268269theorem RamseyProperty.all (K : Set) (n : Nat)270  requires finite : Finite(K)271  shows RamseyProperty(n, K)272proof273  induction n274  | zero => exact RamseyProperty.zero at K275  | k + 1 using ih => exact RamseyProperty.succ at K, k with finite, ih276277-- The infinite Ramsey theorem, for any finite set of colours.278theorem ramsey.infinite_colours (n : Nat) (S C K : Set)279  requires infinite : Infinite(S)280  requires finite : Finite(K)281  requires colouring : C : subsetsOfSize(S, n) → K282  shows ∃ H, H ⊆ S ∧ Infinite(H) ∧283    ∃ c ∈ K, ∀ U ∈ subsetsOfSize(H, n), C(U) = c284proof285  have ramsey := RamseyProperty.all at K, n with finite286  exact ramsey with S, C, infinite, colouring287288-- The infinite Ramsey theorem for two colours.289theorem ramsey.infinite (n : Nat) (S C : Set)290  requires infinite : Infinite(S)291  requires colouring : C : subsetsOfSize(S, n) → 2292  shows ∃ H, H ⊆ S ∧ Infinite(H) ∧293    ∃ c ∈ 2, ∀ U ∈ subsetsOfSize(H, n), C(U) = c294proof295  have finite := Finite.natural at 2296  exact ramsey.infinite_colours with infinite, finite, colouring297298-- The infinite Ramsey theorem for k colours.299theorem ramsey.infinite_numeral (n k : Nat) (S C : Set)300  requires infinite : Infinite(S)301  requires colouring : C : subsetsOfSize(S, n) → k302  shows ∃ H, H ⊆ S ∧ Infinite(H) ∧303    ∃ c ∈ k, ∀ U ∈ subsetsOfSize(H, n), C(U) = c304proof305  have finite := Finite.natural at k306  exact ramsey.infinite_colours with infinite, finite, colouring307