The successor step (Lemma S)

Let N be closed over M and let ν satisfy J over M. There is a law ν' with the marginals of ν on M, satisfying J over N, under which every vertex of N \ M with infinitely many neighbours in M has trace energy at most C over them.

Proof. Force the signs of the set X of such vertices, giving the law Λ = ν.map (forced X s). For each finite family of patterns over N, the key inequality and the mixture lemma give a law with the marginals of Λ on M ∪ X meeting J for those patterns. A limit along an ultrafilter finer than the filter of finite families keeps the marginals on M ∪ X and meets J for every pattern over N.

theorem Erdos111.exists_law_of_finset {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 ν) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (forced X d.s) ν)] (F : Finset (Pattern V)) : ∃ (μ : MeasureTheory.Measure (V → Bool)), MeasureTheory.IsProbabilityMeasure μ ∧ SameOn (M ∪ X) (MeasureTheory.Measure.map (forced X d.s) ν) μ ∧ ∀ P ∈ F, Pattern.IsOver G N P → ∫⁻ (τ : V → Bool), ↑(extCost P.S P.E τ) ∂μ ≤ ↑C * ↑P.S.card

For one finite family of patterns over N, the mixture lemma gives a law with the marginals of the forced law on M ∪ X meeting J for the patterns of the family.

theorem Erdos111.exists_successor {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M N : Set V} (hMN : ClosedOver G M N) {ν : MeasureTheory.Measure (V → Bool)} [MeasureTheory.IsProbabilityMeasure ν] (hν : Rooted G C M ν) : ∃ (ν' : MeasureTheory.Measure (V → Bool)), MeasureTheory.IsProbabilityMeasure ν' ∧ SameOn M ν ν' ∧ Rooted G C N ν' ∧ ∀ y ∈ N \ M, {u : V | G.Adj y u ∧ u ∈ M}.Infinite → TraceBound C ν' y {u : V | G.Adj y u ∧ u ∈ M}

Lemma S.