Exchangeable graph laws as jointly exchangeable array laws

An exchangeable law on infinite graphs is the law of a symmetric Bool-valued array with false on the diagonal, jointly exchangeable under simultaneous relabelling of both axes. This file is the law-level adapter between the two: the array law arrayLaw μ of a law on graphs, the graph law graphLawOfArray ρ of a law on arrays, the bundled equivalence graphLawArrayLawEquiv between exchangeable laws on infinite graphs and the jointly exchangeable probability laws carried by the symmetric false-diagonal arrays, and the dissociation compatibility that lets the array theory speak about graph laws.

• Dissociation. The finite law attached to L is dissociated exactly when its array law is jointly dissociated (isDissociated_iff_jointlyDissociated). The graph notion is independence of two consecutive label windows; the array notion is independence of the arrays read along disjoint index sets; for a jointly exchangeable law consecutive windows suffice (indepFun_restrict_of_forall_Ico), and each window of a graph is the block restriction of its array.
• Convex mixtures. The array law and the graph law are pushforwards, so they are linear in the measure (arrayLaw_add, arrayLaw_smul, graphLawOfArray_add, graphLawOfArray_smul), and the array laws of graph laws are exactly the jointly exchangeable probability laws carried by the symmetric false-diagonal arrays. Extremality among those laws is joint dissociation (jointlyDissociated_iff_mem_extremePoints_on), so dissociation of a graph law is extremality of its array law (isDissociated_iff_arrayLaw_mem_extremePoints).

The carrier-level bridge, the adjacency array of a graph and the graph of an array, is ExchangeableGraphLaw/AdjArray.lean. The window of a graph on the labels [k, k + n) corresponds to the block [k, k + n)² of its adjacency array.

Main results

• TauCeti.DenseGraphLimits.arrayLaw, graphLawOfArray, infiniteGraphLawOfArray — the law-level adapter with its defining pushforwards (arrayLaw_def, graphLawOfArray_def, infiniteGraphLawOfArray_law) and the round trips (graphLawOfArray_arrayLaw, arrayLaw_graphLawOfArray, arrayLaw_infiniteGraphLawOfArray), and graphLawArrayLawEquiv, the bundled equivalence.
• TauCeti.DenseGraphLimits.isDissociated_iff_forall_indepFun_restrict — dissociation of the finite law is block independence of the array law at consecutive windows.
• TauCeti.DenseGraphLimits.isDissociated_iff_jointlyDissociated — dissociation compatibility.
• TauCeti.DenseGraphLimits.isDissociated_iff_arrayLaw_mem_extremePoints, isDissociated_iff_graphLawArrayLawEquiv_mem_extremePoints, isDissociated_graphLawArrayLawEquiv_symm — dissociation of a graph law is extremality of its array law, in either direction of the adapter.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33–61, Section 5.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.

The law-level adapter

noncomputable def TauCeti.DenseGraphLimits.arrayLaw (μ : MeasureTheory.Measure (SimpleGraph ℕ)) : MeasureTheory.Measure (ℕ × ℕ → Bool)

The array law of a law on graphs: its pushforward along the adjacency array.

Equations

• TauCeti.DenseGraphLimits.arrayLaw μ = MeasureTheory.Measure.map SimpleGraph.adjArray μ

theorem TauCeti.DenseGraphLimits.arrayLaw_def (μ : MeasureTheory.Measure (SimpleGraph ℕ)) : arrayLaw μ = MeasureTheory.Measure.map SimpleGraph.adjArray μ

The array law is the pushforward along the adjacency array.

instance TauCeti.DenseGraphLimits.instIsProbabilityMeasureForallProdNatBoolArrayLawOfSimpleGraph (μ : MeasureTheory.Measure (SimpleGraph ℕ)) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (arrayLaw μ)

@[simp]

theorem TauCeti.DenseGraphLimits.arrayLaw_add (μ ν : MeasureTheory.Measure (SimpleGraph ℕ)) : arrayLaw (μ + ν) = arrayLaw μ + arrayLaw ν

The array law of a sum of laws is the sum of the array laws.

@[simp]

theorem TauCeti.DenseGraphLimits.arrayLaw_smul (c : ENNReal) (μ : MeasureTheory.Measure (SimpleGraph ℕ)) : arrayLaw (c • μ) = c • arrayLaw μ

The array law of a scaled law is the scaled array law.

theorem TauCeti.DenseGraphLimits.arrayLaw_compl_symmetricArraysWithDiag_eq_zero (μ : MeasureTheory.Measure (SimpleGraph ℕ)) : (arrayLaw μ) (Probability.symmetricArraysWithDiag Bool false)ᶜ = 0

The array law of any law on graphs is carried by the symmetric false-diagonal arrays.

theorem TauCeti.DenseGraphLimits.jointlyExchangeable_arrayLaw {μ : MeasureTheory.Measure (SimpleGraph ℕ)} (hμ : ∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) μ = μ) : Probability.JointlyExchangeable (arrayLaw μ) fun (p : ℕ × ℕ) (x : ℕ × ℕ → Bool) => x p

The array law of a relabelling-invariant law on graphs is jointly exchangeable.

theorem TauCeti.DenseGraphLimits.arrayLaw_mem_jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag (L : InfiniteExchangeableGraphLaw) : arrayLaw L.law ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false

The array law of an exchangeable law on infinite graphs is a jointly exchangeable probability law carried by the symmetric false-diagonal arrays.

noncomputable def TauCeti.DenseGraphLimits.graphLawOfArray (ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)) : MeasureTheory.Measure (SimpleGraph ℕ)

The graph law of a law on arrays: its pushforward along the graph of an array.

Equations

• TauCeti.DenseGraphLimits.graphLawOfArray ρ = MeasureTheory.Measure.map TauCeti.DenseGraphLimits.graphOfArray ρ

theorem TauCeti.DenseGraphLimits.graphLawOfArray_def (ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)) : graphLawOfArray ρ = MeasureTheory.Measure.map graphOfArray ρ

The graph law is the pushforward along the graph of an array.

instance TauCeti.DenseGraphLimits.instIsProbabilityMeasureSimpleGraphNatGraphLawOfArrayOfForallProdBool (ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)) [MeasureTheory.IsProbabilityMeasure ρ] : MeasureTheory.IsProbabilityMeasure (graphLawOfArray ρ)

@[simp]

theorem TauCeti.DenseGraphLimits.graphLawOfArray_add (ρ ρ' : MeasureTheory.Measure (ℕ × ℕ → Bool)) : graphLawOfArray (ρ + ρ') = graphLawOfArray ρ + graphLawOfArray ρ'

The graph law of a sum of laws is the sum of the graph laws.

@[simp]

theorem TauCeti.DenseGraphLimits.graphLawOfArray_smul (c : ENNReal) (ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)) : graphLawOfArray (c • ρ) = c • graphLawOfArray ρ

The graph law of a scaled law is the scaled graph law.

@[simp]

theorem TauCeti.DenseGraphLimits.graphLawOfArray_arrayLaw (μ : MeasureTheory.Measure (SimpleGraph ℕ)) : graphLawOfArray (arrayLaw μ) = μ

The graph law of the array law of a law on graphs is the law.

@[simp]

theorem TauCeti.DenseGraphLimits.arrayLaw_graphLawOfArray {ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)} (hρ : ρ (Probability.symmetricArraysWithDiag Bool false)ᶜ = 0) : arrayLaw (graphLawOfArray ρ) = ρ

The array law of the graph law of a law carried by the symmetric false-diagonal arrays is the law.

theorem TauCeti.DenseGraphLimits.map_comap_graphLawOfArray {ρ : MeasureTheory.Measure (ℕ × ℕ → Bool)} (σ : Equiv.Perm ℕ) (hρ : MeasureTheory.Measure.map (Probability.pairReindex σ σ) ρ = ρ) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) (graphLawOfArray ρ) = graphLawOfArray ρ

The graph law of a diagonally invariant law on arrays is invariant under relabelling.

noncomputable def TauCeti.DenseGraphLimits.infiniteGraphLawOfArray (ρ : { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }) : InfiniteExchangeableGraphLaw

The exchangeable law on infinite graphs of a jointly exchangeable probability law carried by the symmetric false-diagonal arrays.

Equations

• TauCeti.DenseGraphLimits.infiniteGraphLawOfArray ρ = { law := TauCeti.DenseGraphLimits.graphLawOfArray ↑ρ, prob := ⋯, exchangeable := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteGraphLawOfArray_law (ρ : { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }) : (infiniteGraphLawOfArray ρ).law = graphLawOfArray ↑ρ

The law of the bundled graph law of an array law.

theorem TauCeti.DenseGraphLimits.arrayLaw_infiniteGraphLawOfArray (ρ : { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }) : arrayLaw (infiniteGraphLawOfArray ρ).law = ↑ρ

Converting a carried array law to a graph law and back recovers the array law.

noncomputable def TauCeti.DenseGraphLimits.graphLawArrayLawEquiv : InfiniteExchangeableGraphLaw ≃ { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }

Exchangeable graph laws are the jointly exchangeable array laws carried by the symmetric false-diagonal arrays. The bundled law-level adapter.

Equations

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

@[simp]

theorem TauCeti.DenseGraphLimits.graphLawArrayLawEquiv_apply_coe (L : InfiniteExchangeableGraphLaw) : ↑(graphLawArrayLawEquiv L) = arrayLaw L.law

The forward direction of the adapter is the array law.

@[simp]

theorem TauCeti.DenseGraphLimits.graphLawArrayLawEquiv_symm_apply (ρ : { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }) : graphLawArrayLawEquiv.symm ρ = infiniteGraphLawOfArray ρ

The inverse direction of the adapter is the bundled graph law of the array law.

Dissociation

theorem TauCeti.DenseGraphLimits.isDissociated_iff_forall_indepFun_restrict (L : InfiniteExchangeableGraphLaw) : (exchangeableGraphLawEquivInfinite.symm L).IsDissociated ↔ ∀ (k l : ℕ), ProbabilityTheory.IndepFun (fun (x : ℕ × ℕ → Bool) => (Finset.Ico 0 k ×ˢ Finset.Ico 0 k).restrict x) (fun (x : ℕ × ℕ → Bool) => (Finset.Ico k (k + l) ×ˢ Finset.Ico k (k + l)).restrict x) (arrayLaw L.law)

The dissociation identity of the finite law at (k, l) is block independence of the array law at the windows [0, k)² and [k, k + l)².

theorem TauCeti.DenseGraphLimits.isDissociated_iff_jointlyDissociated (L : InfiniteExchangeableGraphLaw) : (exchangeableGraphLawEquivInfinite.symm L).IsDissociated ↔ Probability.JointlyDissociated (arrayLaw L.law) fun (p : ℕ × ℕ) (x : ℕ × ℕ → Bool) => x p

Dissociation is joint dissociation of the array law.

theorem TauCeti.DenseGraphLimits.isDissociated_iff_arrayLaw_mem_extremePoints (L : InfiniteExchangeableGraphLaw) : (exchangeableGraphLawEquivInfinite.symm L).IsDissociated ↔ arrayLaw L.law ∈ Set.extremePoints ENNReal (Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false)

Dissociation is extremality for exchangeable laws on infinite graphs, read through their array laws.

theorem TauCeti.DenseGraphLimits.isDissociated_iff_graphLawArrayLawEquiv_mem_extremePoints (L : InfiniteExchangeableGraphLaw) : (exchangeableGraphLawEquivInfinite.symm L).IsDissociated ↔ ↑(graphLawArrayLawEquiv L) ∈ Set.extremePoints ENNReal (Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false)

Dissociation is extremality, stated on the adapter: an exchangeable law on infinite graphs is dissociated exactly when its image under graphLawArrayLawEquiv is an extreme point of the jointly exchangeable laws carried by the symmetric arrays.

theorem TauCeti.DenseGraphLimits.isDissociated_graphLawArrayLawEquiv_symm (ρ : { ρ : MeasureTheory.Measure (ℕ × ℕ → Bool) // ρ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false }) (h : ↑ρ ∈ Set.extremePoints ENNReal (Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false)) : (exchangeableGraphLawEquivInfinite.symm (graphLawArrayLawEquiv.symm ρ)).IsDissociated

The graph law recovered from an extreme carried array law is dissociated.