Edge costs, linear graphs, rooted patterns

Signs are Boolean: a sign assignment is τ : V → Bool, and an edge is monochromatic under τ when its two ends receive the same sign.

• edgeCost E is the least number of monochromatic edges of the finite edge set E over all sign assignments, the number of deletions that make E bipartite.
• Linear G C says that every finite edge set of G whose ends lie in s has edgeCost at most C |s|.
• A Pattern has roots R, new vertices S and edges E. Its extension cost extCost P.S P.E τ is the least number of monochromatic edges after the signs of S are chosen freely and the others are those of τ.
• Rooted G C N ν is the property J of the proof: every pattern over N has expected extension cost at most C |S| under the law ν of the signs.
• SameOn A μ ν says that μ and ν have the same finite-dimensional marginals on the coordinates in A.
• TraceBound C ν v T bounds the trace energy ∑ u ∈ T, ν (σ u = σ v) by C.

def Erdos111.mono {V : Type u_1} (τ : V → Bool) : Sym2 V → Prop

mono τ e holds when both ends of e receive the same sign under τ.

Equations

• Erdos111.mono τ = Sym2.lift ⟨fun (a b : V) => τ a = τ b, ⋯⟩

noncomputable def Erdos111.monoCount {V : Type u_1} (E : Finset (Sym2 V)) (τ : V → Bool) : ℕ

The number of edges of E that are monochromatic under τ.

Equations

• Erdos111.monoCount E τ = (Finset.filter (Erdos111.mono τ) E).card

noncomputable def Erdos111.edgeCost {V : Type u_1} (E : Finset (Sym2 V)) : ℕ

The least number of monochromatic edges of E over all sign assignments.

Equations

• Erdos111.edgeCost E = ⨅ (τ : V → Bool), Erdos111.monoCount E τ

noncomputable def Erdos111.extCost {V : Type u_1} (S : Finset V) (E : Finset (Sym2 V)) (τ : V → Bool) : ℕ

The least number of monochromatic edges of E when the signs on S are chosen freely and every other vertex keeps its sign under τ.

Equations

• Erdos111.extCost S E τ = ⨅ (η : V → Bool), Erdos111.monoCount E (S.piecewise η τ)

def Erdos111.Linear {V : Type u_1} (G : SimpleGraph V) (C : NNReal) : Prop

G is C-linear: every finite set of edges of G with ends in s can be made bipartite by deleting at most C |s| of them.

Equations

• Erdos111.Linear G C = ∀ (s : Finset V) (E : Finset (Sym2 V)), ↑E ⊆ G.edgeSet → (∀ e ∈ E, ∀ v ∈ e, v ∈ s) → ↑(Erdos111.edgeCost E) ≤ C * ↑s.card

structure Erdos111.Pattern (V : Type u_2) : Type u_2

A rooted pattern: roots R, new vertices S and edges E.

• R : Finset V

  The roots, whose signs are given.

• S : Finset V

  The new vertices, whose signs are chosen.

• E : Finset (Sym2 V)

  The edges, each meeting S and lying inside R ∪ S.

structure Erdos111.Pattern.IsOver {V : Type u_1} (G : SimpleGraph V) (N : Set V) (P : Pattern V) : Prop

P is a pattern of G over N: its roots lie in N, its new vertices lie outside N, and its edges are edges of G that meet S and lie inside R ∪ S.

• roots_subset : ↑P.R ⊆ N
• new_not_mem (v : V) : v ∈ P.S → v ∉ N
• edges_subset : ↑P.E ⊆ G.edgeSet
• edges_meet (e : Sym2 V) : e ∈ P.E → ∃ v ∈ e, v ∈ P.S
• edges_inside (e : Sym2 V) : e ∈ P.E → ∀ v ∈ e, v ∈ P.R ∨ v ∈ P.S

def Erdos111.Rooted {V : Type u_1} (G : SimpleGraph V) (C : NNReal) (N : Set V) (ν : MeasureTheory.Measure (V → Bool)) : Prop

The property J: every pattern of G over N has expected extension cost at most C |S| under ν.

Equations

• Erdos111.Rooted G C N ν = ∀ (P : Erdos111.Pattern V), Erdos111.Pattern.IsOver G N P → ∫⁻ (τ : V → Bool), ↑(Erdos111.extCost P.S P.E τ) ∂ν ≤ ↑C * ↑P.S.card

def Erdos111.SameOn {V : Type u_1} (A : Set V) (μ ν : MeasureTheory.Measure (V → Bool)) : Prop

μ and ν have the same finite-dimensional marginals on the coordinates in A.

Equations

• Erdos111.SameOn A μ ν = ∀ (J : Finset V), ↑J ⊆ A → MeasureTheory.Measure.map J.restrict μ = MeasureTheory.Measure.map J.restrict ν

def Erdos111.TraceBound {V : Type u_1} (C : NNReal) (ν : MeasureTheory.Measure (V → Bool)) (v : V) (T : Set V) : Prop

The trace energy of v over T is at most C: every finite B ⊆ T has ∑ u ∈ B, ν (σ u = σ v) ≤ C.

Equations

• Erdos111.TraceBound C ν v T = ∀ (B : Finset V), ↑B ⊆ T → ∑ u ∈ B, ν {ω : V → Bool | ω u = ω v} ≤ ↑C

Basic properties

theorem Erdos111.DependsOn.eq_comp_restrict {V : Type u_1} {β : Type u_2} {f : (V → Bool) → β} {J : Finset V} (hf : DependsOn f ↑J) (ω : V → Bool) : f ω = f fun (v : V) => if h : v ∈ J then J.restrict ω ⟨v, h⟩ else true

A function of finitely many coordinates factors through the restriction to them.

theorem Erdos111.measurable_of_dependsOn {V : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : (V → Bool) → β} {J : Finset V} (hf : DependsOn f ↑J) : Measurable f

A function of finitely many coordinates is measurable.

theorem Erdos111.monoCount_congr {V : Type u_1} {E : Finset (Sym2 V)} {τ τ' : V → Bool} (h : ∀ e ∈ E, ∀ v ∈ e, τ v = τ' v) : monoCount E τ = monoCount E τ'

The monochromatic count depends only on the signs at the ends of the edges.

theorem Erdos111.extCost_dependsOn {V : Type u_1} {S : Finset V} {E : Finset (Sym2 V)} {R : Finset V} (hE : ∀ e ∈ E, ∀ v ∈ e, v ∈ R ∨ v ∈ S) : DependsOn (extCost S E) ↑R

The extension cost depends only on the signs off S at the ends of the edges.

theorem Erdos111.exists_monoCount_eq_edgeCost {V : Type u_1} (E : Finset (Sym2 V)) : ∃ (σ : V → Bool), monoCount E σ = edgeCost E

Some sign assignment attains the edge cost.

theorem Erdos111.edgeCost_le_monoCount {V : Type u_1} (E : Finset (Sym2 V)) (σ : V → Bool) : edgeCost E ≤ monoCount E σ

Every sign assignment costs at least the edge cost.

theorem Erdos111.extCost_le_card {V : Type u_1} (S : Finset V) (E : Finset (Sym2 V)) (τ : V → Bool) : extCost S E τ ≤ E.card

The extension cost is at most the number of edges.

theorem Erdos111.exists_extCost_eq {V : Type u_1} (S : Finset V) (E : Finset (Sym2 V)) (τ : V → Bool) : ∃ (η : V → Bool), monoCount E (S.piecewise η τ) = extCost S E τ

Some choice of the signs on S attains the extension cost.

theorem Erdos111.extCost_le_monoCount {V : Type u_1} (S : Finset V) (E : Finset (Sym2 V)) (τ η : V → Bool) : extCost S E τ ≤ monoCount E (S.piecewise η τ)

Every choice of the signs on S costs at least the extension cost.

theorem Erdos111.rooted_empty {V : Type u_1} {G : SimpleGraph V} {C : NNReal} (hG : Linear G C) (ν : MeasureTheory.Measure (V → Bool)) [MeasureTheory.IsProbabilityMeasure ν] : Rooted G C ∅ ν

A linear graph satisfies J over the empty set, for every probability law: a pattern with no roots costs at most C |S| whatever the signs.

theorem Erdos111.SameOn.lintegral_eq {V : Type u_1} {A : Set V} {μ ν : MeasureTheory.Measure (V → Bool)} (h : SameOn A μ ν) {f : (V → Bool) → ENNReal} {J : Finset V} (hf : DependsOn f ↑J) (hJ : ↑J ⊆ A) : ∫⁻ (ω : V → Bool), f ω ∂μ = ∫⁻ (ω : V → Bool), f ω ∂ν

Laws with the same finite marginals on A integrate a function of finitely many coordinates of A alike.

theorem Erdos111.Rooted.of_sameOn {V : Type u_1} {G : SimpleGraph V} {C : NNReal} {N : Set V} {μ ν : MeasureTheory.Measure (V → Bool)} (hμ : Rooted G C N μ) (h : SameOn N μ ν) : Rooted G C N ν

J over N depends only on the finite marginals on N.

theorem Erdos111.TraceBound.of_sameOn {V : Type u_1} {C : NNReal} {A T : Set V} {v : V} {μ ν : MeasureTheory.Measure (V → Bool)} (hμ : TraceBound C μ v T) (h : SameOn A μ ν) (hv : v ∈ A) (hT : T ⊆ A) : TraceBound C ν v T

A trace bound depends only on the finite marginals on the trace and the vertex.

theorem Erdos111.SameOn.trans {V : Type u_1} {A : Set V} {μ ν ρ : MeasureTheory.Measure (V → Bool)} (h₁ : SameOn A μ ν) (h₂ : SameOn A ν ρ) : SameOn A μ ρ

Agreement of finite marginals is transitive.

theorem Erdos111.SameOn.mono {V : Type u_1} {A B : Set V} {μ ν : MeasureTheory.Measure (V → Bool)} (h : SameOn A μ ν) (hBA : B ⊆ A) : SameOn B μ ν

Agreement of finite marginals on A gives agreement on every subset of A.