Extreme jointly exchangeable array laws

A jointly exchangeable probability law on array path space ℕ × ℕ → α is an extreme point of the convex set of jointly exchangeable probability laws if and only if its coordinate array is jointly dissociated. With the corner-tail theorem and the ergodicity theorem this completes the representation-free triangle for jointly exchangeable arrays: joint dissociation, triviality of the corner tail, ergodicity of the diagonal finitary relabelling action, and extremality are one condition, stated on the law alone for any measurable value space.

The jointly exchangeable probability laws are the invariant probability laws for the diagonal finitary action established in Arrays.Ergodic. The extreme-point characterisation is the general one for a countable group action, ErgodicSMul.iff_mem_extremePoints, composed with jointlyDissociated_iff_ergodicSMul.

Main results

• TauCeti.Probability.jointlyExchangeableProbabilityMeasures — the convex set, and its identification with the invariant measures of total mass one of the diagonal action;
• TauCeti.Probability.jointlyDissociated_iff_mem_extremePoints — joint dissociation is extremality among jointly exchangeable probability laws, with jointlyDissociated_of_mem_extremePoints reading dissociation off an extreme point;
• TauCeti.Probability.jointlyExchangeableProbabilityMeasuresOn — the jointly exchangeable probability laws carried by a set of arrays, a face of the whole set, so that jointlyDissociated_iff_mem_extremePoints_on restricts the characterisation to them, and jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag the case of the symmetric arrays with a fixed diagonal, the adjacency arrays of graphs when α = Bool;
• TauCeti.Probability.JointlyDissociated.ae_eq_of_comp_eq — the integral form: a jointly dissociated law written as a mixture of jointly exchangeable laws has almost every component equal to itself.

References

• D. Aldous, "Representations for partially exchangeable arrays of random variables", Journal of Multivariate Analysis 11 (1981), 581--598.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.
• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33–61, Section 5: exchangeable random graphs as symmetric zero-diagonal arrays, and dissociated laws as the extreme ones.

def TauCeti.Probability.jointlyExchangeableProbabilityMeasures (α : Type u_2) [MeasurableSpace α] : Set (MeasureTheory.Measure (ℕ × ℕ → α))

The convex set of jointly exchangeable probability laws on array path space.

Equations

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

@[simp]

theorem TauCeti.Probability.mem_jointlyExchangeableProbabilityMeasures_iff {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure (ℕ × ℕ → α)} : ν ∈ jointlyExchangeableProbabilityMeasures α ↔ (JointlyExchangeable ν fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ∧ MeasureTheory.IsProbabilityMeasure ν

Membership in the jointly exchangeable probability laws.

theorem TauCeti.Probability.jointlyExchangeableProbabilityMeasures_eq {α : Type u_1} [MeasurableSpace α] : jointlyExchangeableProbabilityMeasures α = MeasureTheory.invariantMeasuresOfMeasureUnivEq FinitaryPerm (ℕ × ℕ → α) 1

The jointly exchangeable probability laws are the probability laws invariant under the diagonal finitary action.

theorem TauCeti.Probability.convex_jointlyExchangeableProbabilityMeasures {α : Type u_1} [MeasurableSpace α] : Convex ENNReal (jointlyExchangeableProbabilityMeasures α)

The jointly exchangeable probability laws form a convex set.

theorem TauCeti.Probability.jointlyDissociated_iff_mem_extremePoints {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hexch : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : (JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasures α)

Joint dissociation is extremality: a jointly exchangeable probability law is an extreme point of the jointly exchangeable probability laws if and only if its coordinate array is jointly dissociated.

def TauCeti.Probability.jointlyExchangeableProbabilityMeasuresOn (α : Type u_2) [MeasurableSpace α] (s : Set (ℕ × ℕ → α)) : Set (MeasureTheory.Measure (ℕ × ℕ → α))

The jointly exchangeable probability laws carried by a set s of arrays: those giving mass zero to sᶜ.

Equations

• TauCeti.Probability.jointlyExchangeableProbabilityMeasuresOn α s = {ν : MeasureTheory.Measure (ℕ × ℕ → α) | ν ∈ TauCeti.Probability.jointlyExchangeableProbabilityMeasures α ∧ ν sᶜ = 0}

@[simp]

theorem TauCeti.Probability.mem_jointlyExchangeableProbabilityMeasuresOn_iff {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} {ν : MeasureTheory.Measure (ℕ × ℕ → α)} : ν ∈ jointlyExchangeableProbabilityMeasuresOn α s ↔ ν ∈ jointlyExchangeableProbabilityMeasures α ∧ ν sᶜ = 0

Membership in the jointly exchangeable laws carried by s.

theorem TauCeti.Probability.isExtreme_jointlyExchangeableProbabilityMeasuresOn {α : Type u_1} [MeasurableSpace α] (s : Set (ℕ × ℕ → α)) : IsExtreme ENNReal (jointlyExchangeableProbabilityMeasures α) (jointlyExchangeableProbabilityMeasuresOn α s)

The jointly exchangeable laws carried by s are a face of all jointly exchangeable probability laws.

theorem TauCeti.Probability.convex_jointlyExchangeableProbabilityMeasuresOn {α : Type u_1} [MeasurableSpace α] (s : Set (ℕ × ℕ → α)) : Convex ENNReal (jointlyExchangeableProbabilityMeasuresOn α s)

The jointly exchangeable laws carried by s form a convex set.

theorem TauCeti.Probability.extremePoints_jointlyExchangeableProbabilityMeasuresOn {α : Type u_1} [MeasurableSpace α] (s : Set (ℕ × ℕ → α)) : Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasuresOn α s) = jointlyExchangeableProbabilityMeasuresOn α s ∩ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasures α)

The extreme points of the jointly exchangeable laws carried by s are the extreme jointly exchangeable laws so carried.

theorem TauCeti.Probability.jointlyDissociated_iff_mem_extremePoints_on {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hexch : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (hs : ρ sᶜ = 0) : (JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasuresOn α s)

Joint dissociation is extremality among the laws carried by s: a jointly exchangeable probability law carried by s is an extreme point of the jointly exchangeable laws carried by s if and only if its coordinate array is jointly dissociated.

theorem TauCeti.Probability.jointlyExchangeable_of_mem_extremePoints {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (h : ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasures α)) : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

An extreme point of the jointly exchangeable probability laws is jointly exchangeable.

theorem TauCeti.Probability.isProbabilityMeasure_of_mem_extremePoints {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (h : ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasures α)) : MeasureTheory.IsProbabilityMeasure ρ

An extreme point of the jointly exchangeable probability laws is a probability law.

theorem TauCeti.Probability.jointlyDissociated_of_mem_extremePoints {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (h : ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasures α)) : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

The coordinate array of an extreme point of the jointly exchangeable probability laws is jointly dissociated.

theorem TauCeti.Probability.jointlyDissociated_of_mem_extremePoints_on {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ × ℕ → α)} {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (h : ρ ∈ Set.extremePoints ENNReal (jointlyExchangeableProbabilityMeasuresOn α s)) : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

The coordinate array of an extreme point of the jointly exchangeable laws carried by s is jointly dissociated.

def TauCeti.Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag (α : Type u_2) [MeasurableSpace α] (d : α) : Set (MeasureTheory.Measure (ℕ × ℕ → α))

The jointly exchangeable probability laws carried by the symmetric arrays with diagonal d. For α = Bool and d = false the carrier is the adjacency arrays of the simple graphs on ℕ, and these are the laws of exchangeable random graphs read as arrays.

Equations

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

theorem TauCeti.Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag_eq {α : Type u_1} [MeasurableSpace α] (d : α) : jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag α d = jointlyExchangeableProbabilityMeasuresOn α (symmetricArraysWithDiag α d)

The jointly exchangeable laws carried by the symmetric arrays are the carried laws at that carrier.

@[simp]

theorem TauCeti.Probability.mem_jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag_iff {α : Type u_1} [MeasurableSpace α] {d : α} {ν : MeasureTheory.Measure (ℕ × ℕ → α)} : ν ∈ jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag α d ↔ ν ∈ jointlyExchangeableProbabilityMeasures α ∧ ν (symmetricArraysWithDiag α d)ᶜ = 0

Membership in the jointly exchangeable laws carried by the symmetric arrays.

theorem TauCeti.Probability.JointlyDissociated.ae_eq_of_comp_eq {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {Z : Type u_2} [MeasurableSpace Z] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] {π : MeasureTheory.Measure Z} {κ : ProbabilityTheory.Kernel Z (ℕ × ℕ → α)} [ProbabilityTheory.IsMarkovKernel κ] (hρ : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (hκ : ∀ᵐ (z : Z) ∂π, JointlyExchangeable (κ z) fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (hmix : π.bind ⇑κ = ρ) : ∀ᵐ (z : Z) ∂π, κ z = ρ

A jointly dissociated array law is not a nontrivial mixture of jointly exchangeable laws. If ρ is the mixture κ ∘ₘ π of a Markov kernel whose laws are almost all jointly exchangeable, then almost every κ z is ρ itself. This is the integral form of jointlyDissociated_iff_mem_extremePoints.