The key inequality of the successor step

Let N be closed over M, let ν satisfy J over M, and force the signs of the set X of new vertices with infinite trace. For finitely many patterns P i over N and nonnegative weights ρ i, the expected weighted cost, after choosing the signs of the remaining roots W (new vertices with finite trace) jointly and optimally, is at most ∑ ρ i C |S i|.

Proof. Fix k and take ⌈k ρ i⌉ copies of each S i over its roots inside N \ M, pairwise disjoint and avoiding all roots, by ClosedOver. Together with stars from each root y ∈ X to a y 0, …, a y (L - 1) they form one pattern over M, to which J applies. Almost surely, once L exceeds the number of disagreements along a y plus the total copy weight, every cheap extension gives each y its forced sign, so the pattern costs at least k times the left-hand integrand. Fatou's lemma in L, division by k, and k → ∞ give the bound.

Monochromatic counts

theorem Erdos111.monoCount_le_of_subset {V : Type u_1} {E F : Finset (Sym2 V)} (h : E ⊆ F) (τ : V → Bool) : monoCount E τ ≤ monoCount F τ

The monochromatic count is monotone in the edge set.

theorem Erdos111.injOn_sym2Map_of_injOn {V : Type u_1} {φ : V → V} {A : Set V} (hφ : Set.InjOn φ A) {E : Finset (Sym2 V)} (hE : ∀ e ∈ E, ∀ v ∈ e, v ∈ A) : Set.InjOn (Sym2.map φ) ↑E

Sym2.map φ is injective on the edges inside a set on which φ is injective.

theorem Erdos111.monoCount_image_sym2Map {V : Type u_1} {E : Finset (Sym2 V)} {φ : V → V} (hφ : Set.InjOn (Sym2.map φ) ↑E) (τ : V → Bool) : monoCount (Finset.image (Sym2.map φ) E) τ = monoCount E (τ ∘ φ)

Transport of the monochromatic count along a map injective on the edges.

Copies of patterns

structure Erdos111.IsCopy {V : Type u_1} (G : SimpleGraph V) (M N : Set V) (D : Finset V) (P : Pattern V) (φ : V → V) : Prop

φ copies the pattern P into N: it fixes every vertex off P.S, maps P.S injectively into N away from M and D, and maps the edges of P to edges of G.

• eq_self (v : V) : v ∉ P.S → φ v = v

  Every vertex off the new vertices is fixed.

• injOn : Set.InjOn φ ↑P.S

  The new vertices are copied injectively.

• mem (v : V) : v ∈ P.S → φ v ∈ N ∧ φ v ∉ M ∧ φ v ∉ D

  The copied new vertices lie in N, outside M and D.

• edges (e : Sym2 V) : e ∈ P.E → Sym2.map φ e ∈ G.edgeSet

  The copied edges are edges of G.

theorem Erdos111.exists_copy {V : Type u_1} {G : SimpleGraph V} {M N : Set V} (hMN : ClosedOver G M N) {P : Pattern V} (hP : Pattern.IsOver G N P) {D : Finset V} (hD : ↑D ⊆ N) : ∃ (φ : V → V), IsCopy G M N D P φ

A pattern over N has a copy in N avoiding M and a finite D ⊆ N.

theorem Erdos111.exists_copies {V : Type u_1} {G : SimpleGraph V} {M N : Set V} (hMN : ClosedOver G M N) {ι : Type u_2} [Finite ι] (Q : ι → Pattern V) (hQ : ∀ (j : ι), Pattern.IsOver G N (Q j)) {D : Finset V} (hD : ↑D ⊆ N) : ∃ (φ : ι → V → V), (∀ (j : ι), IsCopy G M N D (Q j) (φ j)) ∧ ∀ (j j' : ι), j ≠ j' → ∀ v ∈ (Q j).S, ∀ v' ∈ (Q j').S, φ j v ≠ φ j' v'

Finitely many patterns over N have copies in N avoiding M and a finite D ⊆ N, with pairwise disjoint images of their new vertices.

theorem Erdos111.IsCopy.injOn_union {V : Type u_1} {G : SimpleGraph V} {M N : Set V} {D : Finset V} {P : Pattern V} {φ : V → V} (h : IsCopy G M N D P φ) (hRD : P.R ⊆ D) (hRS : ∀ v ∈ P.R, v ∉ P.S) : Set.InjOn φ ↑(P.R ∪ P.S)

A copy fixes the roots and is injective on the roots and new vertices together.

theorem Erdos111.IsCopy.extCost_le_monoCount {V : Type u_1} {G : SimpleGraph V} {M N : Set V} {D : Finset V} {P : Pattern V} {φ : V → V} (h : IsCopy G M N D P φ) (hRD : P.R ⊆ D) (hRS : ∀ v ∈ P.R, v ∉ P.S) (hE : ∀ e ∈ P.E, ∀ v ∈ e, v ∈ P.R ∨ v ∈ P.S) {τ τ₀ : V → Bool} (hτ : ∀ v ∈ P.R, τ v = τ₀ v) : extCost P.S P.E τ₀ ≤ monoCount (Finset.image (Sym2.map φ) P.E) τ

A copy of P costs at least the extension cost of P under any signs agreeing on the roots.

theorem Erdos111.IsCopy.disjoint_edges {V : Type u_1} {G : SimpleGraph V} {M N : Set V} {D : Finset V} {P Q : Pattern V} {φ ψ : V → V} (hφ : IsCopy G M N D P φ) (hψ : IsCopy G M N D Q ψ) (hP : Pattern.IsOver G N P) (hQ : Pattern.IsOver G N Q) (hQD : Q.R ⊆ D) (h : ∀ v ∈ P.S, ∀ v' ∈ Q.S, φ v ≠ ψ v') : Disjoint (Finset.image (Sym2.map φ) P.E) (Finset.image (Sym2.map ψ) Q.E)

Copies with disjoint new vertices avoiding all roots have disjoint edge sets.

theorem Erdos111.monoCount_biUnion_of_pairwiseDisjoint {V : Type u_1} {ι : Type u_2} {s : Finset ι} {t : ι → Finset (Sym2 V)} (h : (↑s).PairwiseDisjoint t) (τ : V → Bool) : monoCount (s.biUnion t) τ = ∑ j ∈ s, monoCount (t j) τ

The monochromatic count over a disjoint union of edge sets is the sum of the counts.

theorem Erdos111.sum_sigma_fin {r : ℕ} (m : Fin r → ℕ) (x : Fin r → ENNReal) : ∑ j : (i : Fin r) × Fin (m i), x j.fst = ∑ i : Fin r, ↑(m i) * x i

A sum over the copies is a sum over the patterns weighted by the numbers of copies.

theorem Erdos111.sum_sigma_fin_nat {r : ℕ} (m x : Fin r → ℕ) : ∑ j : (i : Fin r) × Fin (m i), x j.fst = ∑ i : Fin r, m i * x i

The natural-number version of sum_sigma_fin.

theorem Erdos111.le_of_forall_nat_mul_le {I T B : ENNReal} (hB : B ≠ ⊤) (h : ∀ (k : ℕ), 0 < k → ↑k * I ≤ ↑k * T + B) : I ≤ T

An inequality k I ≤ k T + B for all k ≥ 1 with B finite gives I ≤ T.

The pattern of stars and copies

noncomputable def Erdos111.allRoots {V : Type u_1} {r : ℕ} (P : Fin r → Pattern V) : Finset V

The roots of the patterns P i.

Equations

• Erdos111.allRoots P = Finset.univ.biUnion fun (i : Fin r) => (P i).R

noncomputable def Erdos111.starCopy {V : Type u_1} {r : ℕ} (P : Fin r → Pattern V) {m : Fin r → ℕ} (φ : (i : Fin r) × Fin (m i) → V → V) (M X : Set V) (W : Finset V) (a : V → ℕ → V) (L : ℕ) : Pattern V

The pattern made of the stars from the roots y ∈ X to a y 0, …, a y (L - 1) and the copies φ j of the patterns P j.1, with the roots in X and W as new vertices and the roots in M as roots.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos111.starCopy_isOver {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M N X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (hX : X ⊆ N \ M) (d : ForcingData G C M X ν) {r : ℕ} {P : Fin r → Pattern V} (hP : ∀ (i : Fin r), Pattern.IsOver G N (P i)) {W : Finset V} (hW : ∀ (i : Fin r), ∀ v ∈ (P i).R, v ∈ M ∨ v ∈ X ∨ v ∈ W) (hWN : ↑W ⊆ N \ M) {m : Fin r → ℕ} {φ : (i : Fin r) × Fin (m i) → V → V} {D : Finset V} (hφ : ∀ (j : (i : Fin r) × Fin (m i)), IsCopy G M N D (P j.fst) (φ j)) (L : ℕ) : Pattern.IsOver G M (starCopy P φ M X W d.a L)

The stars and copies form a pattern over M.

theorem Erdos111.card_starCopy_S_le {V : Type u_1} {r : ℕ} (P : Fin r → Pattern V) {m : Fin r → ℕ} (φ : (i : Fin r) × Fin (m i) → V → V) (M X : Set V) (W : Finset V) (a : V → ℕ → V) (L : ℕ) : (starCopy P φ M X W a L).S.card ≤ {x ∈ allRoots P | x ∈ X}.card + W.card + ∑ i : Fin r, m i * (P i).S.card

The stars and copies have at most |R ∩ X| + |W| + ∑ m i |S i| new vertices.

theorem Erdos111.le_extCost_starCopy {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M N X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (hX : X ⊆ N \ M) (d : ForcingData G C M X ν) {r : ℕ} {P : Fin r → Pattern V} (hP : ∀ (i : Fin r), Pattern.IsOver G N (P i)) {W : Finset V} (hW : ∀ (i : Fin r), ∀ v ∈ (P i).R, v ∈ M ∨ v ∈ X ∨ v ∈ W) (hWN : ↑W ⊆ N \ M) (ρ : Fin r → NNReal) {k : ENNReal} {m : Fin r → ℕ} (hm : ∀ (i : Fin r), k * ↑(ρ i) ≤ ↑(m i)) {φ : (i : Fin r) × Fin (m i) → V → V} {D : Finset V} (hRD : allRoots P ⊆ D) (hφ : ∀ (j : (i : Fin r) × Fin (m i)), IsCopy G M N D (P j.fst) (φ j)) (hdisj : ∀ (j j' : (i : Fin r) × Fin (m i)), j ≠ j' → ∀ v ∈ (P j.fst).S, ∀ v' ∈ (P j'.fst).S, φ j v ≠ φ j' v') {ω : V → Bool} (hfin : ∀ y ∈ {x ∈ allRoots P | x ∈ X}, {n : ℕ | ω (d.a y n) ≠ d.s y ω}.Finite) {L : ℕ} (hL : ∑ y ∈ allRoots P with y ∈ X, {n : ℕ | ω (d.a y n) ≠ d.s y ω}.ncard + ∑ j : (i : Fin r) × Fin (m i), (P j.fst).E.card ≤ L) : k * ⨅ (η : V → Bool), ∑ i : Fin r, ↑(ρ i) * ↑(extCost (P i).S (P i).E (W.piecewise η (forced X d.s ω))) ≤ ↑(extCost (starCopy P φ M X W d.a L).S (starCopy P φ M X W d.a L).E ω)

The combinatorial lower bound: once L exceeds the disagreements along every a y plus the total number of edges of the copies, the stars and copies cost at least k times the optimal weighted cost of the patterns under the forced signs.

theorem Erdos111.key_inequality {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M N X : Set V} (hMN : ClosedOver G M N) {ν : MeasureTheory.Measure (V → Bool)} (hν : Rooted G C M ν) (hX : X ⊆ N \ M) (d : ForcingData G C M X ν) {r : ℕ} (P : Fin r → Pattern V) (hP : ∀ (i : Fin r), Pattern.IsOver G N (P i)) (W : Finset V) (hW : ∀ (i : Fin r), ∀ v ∈ (P i).R, v ∈ M ∨ v ∈ X ∨ v ∈ W) (hWN : ↑W ⊆ N \ M) (ρ : Fin r → NNReal) : ∫⁻ (ω : V → Bool), ⨅ (η : V → Bool), ∑ i : Fin r, ↑(ρ i) * ↑(extCost (P i).S (P i).E (W.piecewise η (forced X d.s ω))) ∂ν ≤ ∑ i : Fin r, ↑(ρ i) * (↑C * ↑(P i).S.card)

The key inequality (S) of the successor step, for nonnegative real weights.