Dissociation implies restriction independence (Diaconis–Janson Theorem 5.5, issue #91)

The reverse arc completing the five-way extremality theorem: a dissociated law is restriction independent. The finite content is a two-block factorization obtained from the upper-mass dissociation criterion by a two-variable Möbius inversion; it is then lifted from finite tail windows to the whole tail σ-algebra.

noncomputable def Graphon.upperSum₂ {k m : ℕ} (p : SimpleGraph (Fin k) → SimpleGraph (Fin m) → ℝ) (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)) : ℝ

The two-variable upper transform.

Equations

• Graphon.upperSum₂ p F H = Graphon.upperSum (fun (F' : SimpleGraph (Fin k)) => Graphon.upperSum (fun (H' : SimpleGraph (Fin m)) => p F' H') H) F

theorem Graphon.upperSum₂_injective {k m : ℕ} {p q : SimpleGraph (Fin k) → SimpleGraph (Fin m) → ℝ} (h : ∀ (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)), upperSum₂ p F H = upperSum₂ q F H) : p = q

The two-variable upper transform is injective.

def InfiniteGraph.blockInit (k m : ℕ) : Fin k ↪ Fin (k + m)

The initial-block embedding Fin k ↪ Fin (k+m) (the first k vertices), matching finSumFinEquiv on Sum.inl.

Equations

• InfiniteGraph.blockInit k m = Function.Embedding.inl.trans finSumFinEquiv.toEmbedding

def InfiniteGraph.blockTail (k m : ℕ) : Fin m ↪ Fin (k + m)

The tail-block embedding Fin m ↪ Fin (k+m) (the vertices k, …, k+m-1), matching finSumFinEquiv on Sum.inr.

Equations

• InfiniteGraph.blockTail k m = Function.Embedding.inr.trans finSumFinEquiv.toEmbedding

@[simp]

theorem InfiniteGraph.blockInit_apply (k m : ℕ) (a : Fin k) : ↑((blockInit k m) a) = ↑a

@[simp]

theorem InfiniteGraph.blockTail_apply (k m : ℕ) (b : Fin m) : ↑((blockTail k m) b) = k + ↑b

theorem InfiniteGraph.restrictFin_eq_comap_blockInit (k m : ℕ) (G : InfiniteGraph) : restrictFin k G = SimpleGraph.comap (⇑(blockInit k m)) (restrictFin (k + m) G)

The initial restriction is the initial-block comap of the (k+m)-restriction.

theorem InfiniteGraph.restrictFin_drop_eq_comap_blockTail (k m : ℕ) (G : InfiniteGraph) : restrictFin m (drop k G) = SimpleGraph.comap (⇑(blockTail k m)) (restrictFin (k + m) G)

The tail-window restriction is the tail-block comap of the (k+m)-restriction.

theorem InfiniteGraph.sum_map_le_iff {k m : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)) (K : SimpleGraph (Fin (k + m))) : SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F ⊕g H) ≤ K ↔ F ≤ SimpleGraph.comap (⇑(blockInit k m)) K ∧ H ≤ SimpleGraph.comap (⇑(blockTail k m)) K

The disjoint-union order characterization: a graph on Fin (k+m) contains the mapped disjoint union (F ⊕g H).map finSumFinEquiv iff its initial block contains F and its tail block contains H (cross-block edges unrestricted).

theorem Graphon.upperSum_const_mul {k : ℕ} (c : ℝ) (p : SimpleGraph (Fin k) → ℝ) (F : SimpleGraph (Fin k)) : upperSum (fun (G : SimpleGraph (Fin k)) => c * p G) F = c * upperSum p F

Constants factor out of the upper transform (left).

theorem Graphon.upperSum_mul_const {k : ℕ} (c : ℝ) (p : SimpleGraph (Fin k) → ℝ) (F : SimpleGraph (Fin k)) : upperSum (fun (G : SimpleGraph (Fin k)) => p G * c) F = upperSum p F * c

Constants factor out of the upper transform (right).

noncomputable def Graphon.blockJoint (L : ExchangeableGraphLaw) (k m : ℕ) (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)) : ℝ

The real-valued joint mass of the two exact block events under the (k+m)-vertex law.

Equations

• One or more equations did not get rendered due to their size.

theorem Graphon.upperSum₂_blockJoint (L : ExchangeableGraphLaw) (k m : ℕ) (F₀ : SimpleGraph (Fin k)) (H₀ : SimpleGraph (Fin m)) : upperSum₂ (blockJoint L k m) F₀ H₀ = L.upperMass (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F₀ ⊕g H₀))

Joint side of the two-block factorization: the double upper transform of the block joint mass is the upper mass of the mapped disjoint union (cross-block edges unrestricted).

theorem Graphon.upperSum₂_prod (L : ExchangeableGraphLaw) (k m : ℕ) (F₀ : SimpleGraph (Fin k)) (H₀ : SimpleGraph (Fin m)) : upperSum₂ (fun (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)) => ((L.law k) F).toReal * ((L.law m) H).toReal) F₀ H₀ = L.upperMass F₀ * L.upperMass H₀

Product side of the two-block factorization: the upper transform of the product of the two marginal masses is the product of their upper masses.

theorem Graphon.blockJoint_eq_prod {L : ExchangeableGraphLaw} (hL : L.IsDissociated) (k m : ℕ) (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin m)) : blockJoint L k m F H = ((L.law k) F).toReal * ((L.law m) H).toReal

The exact two-block factorization (the combinatorial heart of the reverse arc): for a dissociated law, the joint mass of the two exact block events factors as the product of the two marginal masses.

@[reducible]

noncomputable def InfiniteGraph.tailWindowAlgebra (k m : ℕ) : MeasurableSpace InfiniteGraph

The tail-window σ-algebra: events depending only on the graph induced on the vertices k, …, k+m-1.

Equations

• InfiniteGraph.tailWindowAlgebra k m = MeasurableSpace.comap (fun (G : InfiniteGraph) => InfiniteGraph.restrictFin m (InfiniteGraph.drop k G)) inferInstance

theorem InfiniteGraph.tailWindowAlgebra_eq_comap (k m : ℕ) : tailWindowAlgebra k m = MeasurableSpace.comap (drop k) (initialAlgebra m)

theorem InfiniteGraph.tailWindowAlgebra_le (k m : ℕ) : tailWindowAlgebra k m ≤ inferInstance

theorem InfiniteGraph.iSup_tailWindowAlgebra (k : ℕ) : ⨆ (m : ℕ), tailWindowAlgebra k m = tailAlgebra k

The tail-window σ-algebras exhaust the tail σ-algebra at level k.

theorem InfiniteGraph.tailWindowAlgebra_mono (k : ℕ) : Monotone (tailWindowAlgebra k)

theorem Graphon.InfiniteExchangeableGraphLaw.indep_initial_tailWindow (M : InfiniteExchangeableGraphLaw) (hM : M.IsDissociated) (k m : ℕ) : ProbabilityTheory.Indep (InfiniteGraph.initialAlgebra k) (InfiniteGraph.tailWindowAlgebra k m) ↑M.law

Finite-window restriction independence (from the exact block factorization): for a dissociated law, the initial k-vertex σ-algebra is independent of the tail-window σ-algebra.

theorem Graphon.InfiniteExchangeableGraphLaw.restrictionIndependent_of_isDissociated (M : InfiniteExchangeableGraphLaw) (hM : M.IsDissociated) : M.RestrictionIndependent

Dissociation implies restriction independence (the reverse arc): the finite-window independence lifts to the whole tail σ-algebra since the tail windows exhaust it.

theorem Graphon.InfiniteExchangeableGraphLaw.isDissociated_iff_restrictionIndependent (M : InfiniteExchangeableGraphLaw) : M.IsDissociated ↔ M.RestrictionIndependent

The dissociation ↔ restriction-independence equivalence.

theorem Graphon.InfiniteExchangeableGraphLaw.isDissociated_iff_vertexTailTrivial (M : InfiniteExchangeableGraphLaw) : M.IsDissociated ↔ M.VertexTailTrivial

Dissociation ↔ vertex-tail triviality (the tail formulation of extremality, as a direct pairwise equivalence).

theorem Graphon.InfiniteExchangeableGraphLaw.tfae_extremality (M : InfiniteExchangeableGraphLaw) : [∃ (x : StandardGraphonSpace), GraphonSpace.infiniteMixtureLawEquiv.symm M = MeasureTheory.diracProba x, ∃ (x : StandardGraphonSpace), M = GraphonSpace.infiniteSampleExchangeableLaw x, M.IsDissociated, M.RestrictionIndependent, M.VertexTailTrivial].TFAE

Diaconis–Janson Theorem 5.5 (the five-way extremality theorem).