Limits of sign laws along an ultrafilter

Probability laws on V → Bool are compact in the following sense: along any ultrafilter, the finite-dimensional marginals of a family of laws converge, and Kolmogorov extension turns the limits into one law. Every property that is a closed condition on finitely many coordinates, holding eventually along the ultrafilter, then holds for the limit. In particular Rooted, SameOn and TraceBound pass to the limit.

theorem Erdos111.exists_tendsto_measure_of_finite {α : Type u_2} {X : Type u_3} [Finite X] [MeasurableSpace X] [MeasurableSingletonClass X] (F : Ultrafilter α) (π : α → MeasureTheory.Measure X) : ∃ (ρ : MeasureTheory.Measure X), ∀ (S : Set X), Filter.Tendsto (fun (a : α) => (π a) S) (↑F) (nhds (ρ S))

Along an ultrafilter, laws on a finite type converge setwise to a limit measure.

theorem Erdos111.exists_limit {V : Type u_1} {α : Type u_2} (F : Ultrafilter α) (ν : α → MeasureTheory.Measure (V → Bool)) [∀ (a : α), MeasureTheory.IsProbabilityMeasure (ν a)] : ∃ (μ : MeasureTheory.Measure (V → Bool)), MeasureTheory.IsProbabilityMeasure μ ∧ ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))

Along an ultrafilter, sign laws have a limit law: the integral of every finite-valued function of finitely many coordinates converges to its integral under the limit.

theorem Erdos111.lintegral_le_of_tendsto {V : Type u_1} {α : Type u_2} {F : Ultrafilter α} {ν : α → MeasureTheory.Measure (V → Bool)} {μ : MeasureTheory.Measure (V → Bool)} (hμ : ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))) {J : Finset V} {f : (V → Bool) → ENNReal} (hf : DependsOn f ↑J) (hfin : ∀ (ω : V → Bool), f ω ≠ ⊤) {c : ENNReal} (h : ∀ᶠ (a : α) in ↑F, ∫⁻ (ω : V → Bool), f ω ∂ν a ≤ c) : ∫⁻ (ω : V → Bool), f ω ∂μ ≤ c

A bound on the integral of a finite-valued function of finitely many coordinates that holds eventually along the ultrafilter holds for the limit law.

theorem Erdos111.rooted_of_tendsto {V : Type u_1} {α : Type u_2} {F : Ultrafilter α} {ν : α → MeasureTheory.Measure (V → Bool)} {μ : MeasureTheory.Measure (V → Bool)} (hμ : ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))) {G : SimpleGraph V} {C : NNReal} {N : Set V} (h : ∀ (P : Pattern V), Pattern.IsOver G N P → ∀ᶠ (a : α) in ↑F, ∫⁻ (τ : V → Bool), ↑(extCost P.S P.E τ) ∂ν a ≤ ↑C * ↑P.S.card) : Rooted G C N μ

J over N passes to the limit law.

theorem Erdos111.tendsto_measure_of_dependsOn {V : Type u_1} {α : Type u_2} {F : Ultrafilter α} {ν : α → MeasureTheory.Measure (V → Bool)} {μ : MeasureTheory.Measure (V → Bool)} (hμ : ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))) {J : Finset V} {s : Set (V → Bool)} (hs : MeasurableSet s) (hsJ : DependsOn (fun (x : V → Bool) => x ∈ s) ↑J) : Filter.Tendsto (fun (a : α) => (ν a) s) (↑F) (nhds (μ s))

The mass of a measurable set determined by finitely many coordinates converges to its mass under the limit law.

theorem Erdos111.sameOn_of_tendsto {V : Type u_1} {α : Type u_2} {F : Ultrafilter α} {ν : α → MeasureTheory.Measure (V → Bool)} {μ : MeasureTheory.Measure (V → Bool)} (hμ : ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))) {A : Set V} {ρ : MeasureTheory.Measure (V → Bool)} (h : ∀ᶠ (a : α) in ↑F, SameOn A ρ (ν a)) : SameOn A ρ μ

Agreement of finite marginals on A with a fixed law passes to the limit law.

theorem Erdos111.traceBound_of_tendsto {V : Type u_1} {α : Type u_2} {F : Ultrafilter α} {ν : α → MeasureTheory.Measure (V → Bool)} {μ : MeasureTheory.Measure (V → Bool)} (hμ : ∀ (J : Finset V) (f : (V → Bool) → ENNReal), DependsOn f ↑J → (∀ (ω : V → Bool), f ω ≠ ⊤) → Filter.Tendsto (fun (a : α) => ∫⁻ (ω : V → Bool), f ω ∂ν a) (↑F) (nhds (∫⁻ (ω : V → Bool), f ω ∂μ))) {C : NNReal} {v : V} {T : Set V} (h : ∀ᶠ (a : α) in ↑F, TraceBound C (ν a) v T) : TraceBound C μ v T

A trace bound that holds eventually along the ultrafilter holds for the limit law.