Forced signs

Over the previous set M, every vertex y of the set X of new vertices with infinite trace carries derived-sign data from Lemma D. The forcing map replaces the sign of each y ∈ X by the opposite of its derived sign and keeps every other sign. Under the law ν.map (forced X s) the coordinates of X take exactly the forced values, the marginals on M are those of ν, and every y ∈ X has trace energy at most C.

structure Erdos111.ForcingData {V : Type u_1} (G : SimpleGraph V) (C : NNReal) (M X : Set V) (ν : MeasureTheory.Measure (V → Bool)) : Type u_1

Derived-sign data over M for the vertices of X, as given by Lemma D.

• s : V → (V → Bool) → Bool

  The derived sign of each vertex.

• a : V → ℕ → V

  The enumerated neighbours in M that determine the derived sign.

• injective (y : V) : y ∈ X → Function.Injective (self.a y)
• adj_mem (y : V) : y ∈ X → ∀ (n : ℕ), G.Adj y (self.a y n) ∧ self.a y n ∈ M
• measurable (y : V) : y ∈ X → Measurable (self.s y)
• ae_finite (y : V) : y ∈ X → ∀ᵐ (ω : V → Bool) ∂ν, {n : ℕ | ω (self.a y n) ≠ self.s y ω}.Finite
• sum_le (y : V) : y ∈ X → ∀ (B : Finset V), ↑B ⊆ {u : V | G.Adj y u ∧ u ∈ M} → ∑ u ∈ B, ν {ω : V → Bool | ω u ≠ self.s y ω} ≤ ↑C

theorem Erdos111.exists_forcingData {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (hν : Rooted G C M ν) (hX : ∀ y ∈ X, y ∉ M ∧ {u : V | G.Adj y u ∧ u ∈ M}.Infinite) : Nonempty (ForcingData G C M X ν)

Lemma D supplies forcing data for every set of vertices outside M with infinite traces.

noncomputable def Erdos111.forced {V : Type u_1} (X : Set V) (s : V → (V → Bool) → Bool) (ω : V → Bool) : V → Bool

The forcing map: each y ∈ X takes the opposite of its derived sign.

Equations

• Erdos111.forced X s ω v = if v ∈ X then !s v ω else ω v

theorem Erdos111.measurable_forced {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (d : ForcingData G C M X ν) : Measurable (forced X d.s)

The forcing map is measurable.

theorem Erdos111.sameOn_map_forced {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (d : ForcingData G C M X ν) (hXM : Disjoint X M) : SameOn M ν (MeasureTheory.Measure.map (forced X d.s) ν)

The forced law has the marginals of ν on M.

theorem Erdos111.traceBound_map_forced {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {M X : Set V} {ν : MeasureTheory.Measure (V → Bool)} (d : ForcingData G C M X ν) (hXM : Disjoint X M) {y : V} (hy : y ∈ X) : TraceBound C (MeasureTheory.Measure.map (forced X d.s) ν) y {u : V | G.Adj y u ∧ u ∈ M}

Under the forced law every y ∈ X has trace energy at most C over its neighbours in M.