Toward the five-way extremality theorem (Diaconis–Janson Theorem 5.5, issue #91)

The vertex-tail formulation of extremality: the empirical limit is vertex-tail measurable (Graphon/VertexTail.lean), so a law with a trivial vertex-tail σ-algebra has a Dirac representing measure, hence is dissociated.

• Graphon.InfiniteExchangeableGraphLaw.VertexTailTrivial — the vertex-tail σ-algebra is M.law-trivial;
• Graphon.InfiniteExchangeableGraphLaw.law_map_drop — the law is invariant under the tail shift (consistency of the finite marginals);
• GraphonSpace.isDissociated_of_vertexTailTrivial — vertex-tail triviality implies dissociation: the representing measure has all-0/1 masses (its coordinates factor through the tail-measurable limitGraphon), hence is Dirac.

The initial and vertex-tail σ-algebras and their laws

@[reducible]

noncomputable def InfiniteGraph.initialAlgebra (k : ℕ) : MeasurableSpace InfiniteGraph

The initial σ-algebra: events depending only on the first k vertices.

Equations

• InfiniteGraph.initialAlgebra k = MeasurableSpace.comap (InfiniteGraph.restrictFin k) inferInstance

theorem InfiniteGraph.initialAlgebra_le (k : ℕ) : initialAlgebra k ≤ inferInstance

theorem InfiniteGraph.initialAlgebra_mono : Monotone initialAlgebra

The initial σ-algebras are monotone in the number of vertices.

theorem InfiniteGraph.iSup_initialAlgebra_eq : ⨆ (k : ℕ), initialAlgebra k = inferInstance

The initial σ-algebras generate the Borel σ-algebra: the initial cylinders are a generating family.

theorem Graphon.InfiniteExchangeableGraphLaw.law_map_drop (M : InfiniteExchangeableGraphLaw) (k : ℕ) : MeasureTheory.Measure.map (InfiniteGraph.drop k) ↑M.law = ↑M.law

The law is invariant under the tail shift: deleting the first k vertices does not change the law (consistency of the finite marginals under the addNat injections).

def Graphon.InfiniteExchangeableGraphLaw.VertexTailTrivial (M : InfiniteExchangeableGraphLaw) : Prop

Vertex-tail triviality: every event in the vertex-tail σ-algebra ⋂ₖ σ(G|{k,k+1,…}) has M.law-measure 0 or 1.

Equations

• M.VertexTailTrivial = ∀ (s : Set InfiniteGraph), MeasurableSet s → ↑M.law s = 0 ∨ ↑M.law s = 1

def Graphon.InfiniteExchangeableGraphLaw.RestrictionIndependent (M : InfiniteExchangeableGraphLaw) : Prop

Restriction independence: for every k, the graph on the first k vertices is independent of the graph on the remaining vertices.

Equations

• M.RestrictionIndependent = ∀ (k : ℕ), ProbabilityTheory.Indep (InfiniteGraph.initialAlgebra k) (InfiniteGraph.tailAlgebra k) ↑M.law

theorem Graphon.InfiniteExchangeableGraphLaw.vertexTailTrivial_of_restrictionIndependent {M : InfiniteExchangeableGraphLaw} (hM : M.RestrictionIndependent) : M.VertexTailTrivial

Restriction independence implies vertex-tail triviality: a vertex-tail event is independent of every initial σ-algebra, hence — the initial σ-algebras generating the Borel σ-algebra — independent of itself, so has measure 0 or 1.

Vertex-tail triviality implies dissociation

theorem GraphonSpace.representing_dirac_of_vertexTailTrivial {M : Graphon.InfiniteExchangeableGraphLaw} (hM : M.VertexTailTrivial) : ∃ (x : StandardGraphonSpace), infiniteMixtureLawEquiv.symm M = MeasureTheory.diracProba x

Vertex-tail triviality implies a Dirac representing measure: the representing measure's Borel masses factor through the tail-measurable limitGraphon, so they are all 0 or 1, forcing a Dirac.

theorem GraphonSpace.isDissociated_of_vertexTailTrivial {M : Graphon.InfiniteExchangeableGraphLaw} (hM : M.VertexTailTrivial) : M.IsDissociated

Vertex-tail triviality implies dissociation (a Diaconis–Janson Theorem 5.5 arc): a law whose vertex-tail σ-algebra is trivial is dissociated.