Derived signs of infinite traces (Lemma D)

Let ν satisfy J over M, and let y ∉ M have infinitely many neighbours in M. Enumerate infinitely many of them as a 0, a 1, …. Stars from y to finite sets of neighbours are patterns over M, so the expected minority count of the signs on any finite set of neighbours is at most C. Hence almost surely one sign occurs only finitely often along a; the other is the derived sign s, a measurable function of the coordinates a n. For every finite set B of neighbours, the stars on B together with a 0, …, a (L - 1) cost at least the disagreements with s on B once the derived sign has recurred often enough along a, so monotone convergence in L bounds ∑ u ∈ B, ν (σ u ≠ s) by C.

theorem Erdos111.exists_extCost_star_eq {V : Type u_1} {y : V} {D : Finset V} (hyD : y ∉ D) (τ : V → Bool) : ∃ (c : Bool), extCost {y} (Finset.image (fun (b : V) => s(y, b)) D) τ = {b ∈ D | τ b = c}.card

A star from y to the vertices of D, with y ∉ D, has extension cost equal to the number of vertices of D carrying some sign c, the sign chosen for y.

theorem Erdos111.isOver_star {V : Type u_1} {G : SimpleGraph V} {M : Set V} {y : V} (hy : y ∉ M) {D : Finset V} (hD : ↑D ⊆ {u : V | G.Adj y u ∧ u ∈ M}) : Pattern.IsOver G M { R := D, S := {y}, E := Finset.image (fun (b : V) => s(y, b)) D }

A star from y ∉ M to finitely many of its neighbours in M is a pattern over M.

theorem Erdos111.exists_le_card_filter_range {p : ℕ → Prop} [DecidablePred p] (h : {n : ℕ | p n}.Infinite) (K : ℕ) : ∃ (L : ℕ), K ≤ (Finset.filter p (Finset.range L)).card

An infinite set of naturals meets some initial segment in at least K elements.

theorem Erdos111.card_filter_range_mono (p : ℕ → Prop) [DecidablePred p] {L L' : ℕ} (h : L ≤ L') : (Finset.filter p (Finset.range L)).card ≤ (Finset.filter p (Finset.range L')).card

The count of a property along an initial segment is monotone in its length.

theorem Erdos111.measurable_card_filter {V : Type u_1} {ι : Type u_2} (B : Finset ι) (p : ι → (V → Bool) → Prop) [(i : ι) → (ω : V → Bool) → Decidable (p i ω)] (hp : ∀ (i : ι), MeasurableSet {ω : V → Bool | p i ω}) : Measurable fun (ω : V → Bool) => ↑{i ∈ B | p i ω}.card

The number of indices with a measurable property is a measurable function.

theorem Erdos111.lintegral_card_filter {V : Type u_1} {ι : Type u_2} (ν : MeasureTheory.Measure (V → Bool)) (B : Finset ι) (p : ι → (V → Bool) → Prop) [(i : ι) → (ω : V → Bool) → Decidable (p i ω)] (hp : ∀ (i : ι), MeasurableSet {ω : V → Bool | p i ω}) : ∫⁻ (ω : V → Bool), ↑{i ∈ B | p i ω}.card ∂ν = ∑ i ∈ B, ν {ω : V → Bool | p i ω}

The expected number of indices with a measurable property is the sum of their probabilities.

theorem Erdos111.exists_derivedSign {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M : Set V} {ν : MeasureTheory.Measure (V → Bool)} (hν : Rooted G C M ν) {y : V} (hy : y ∉ M) (hT : {u : V | G.Adj y u ∧ u ∈ M}.Infinite) : ∃ (s : (V → Bool) → Bool) (a : ℕ → V), Function.Injective a ∧ (∀ (n : ℕ), G.Adj y (a n) ∧ a n ∈ M) ∧ DependsOn s (Set.range a) ∧ Measurable s ∧ (∀ᵐ (ω : V → Bool) ∂ν, {n : ℕ | ω (a n) ≠ s ω}.Finite) ∧ ∀ (B : Finset V), ↑B ⊆ {u : V | G.Adj y u ∧ u ∈ M} → ∑ u ∈ B, ν {ω : V → Bool | ω u ≠ s ω} ≤ ↑C

Lemma D: a vertex with infinitely many neighbours in M has a derived sign s, determined by the signs along an enumeration a of some of those neighbours, from which almost surely only finitely many signs along a differ, and whose expected disagreement with the signs of the neighbours sums to at most C.