Dissociated arrays

The Aldous--Hoover representation of an exchangeable array has an ergodic form, in which the array is a fixed measurable function of one variable per row, one per column, and one per cell, with no global variable; the general form is a mixture of these over the global variable. The class of laws the ergodic form describes is singled out by dissociation: sub-arrays over disjoint sets of rows and disjoint sets of columns are independent.

Two disjointness conditions are needed, one per axis, and this file therefore carries the two notions the two array symmetries ask for:

• SeparatelyDissociated μ X — the blocks X (i, j), i ∈ A, j ∈ B, and X (i, j), i ∈ A', j ∈ B', are independent whenever A ∩ A' = ∅ and B ∩ B' = ∅. This is the notion paired with SeparatelyExchangeable;
• JointlyDissociated μ X — the square blocks over A × A and A' × A' are independent whenever A ∩ A' = ∅. This is the notion paired with JointlyExchangeable, and it is genuinely weaker (SeparatelyDissociated.jointlyDissociated): a symmetric array is not separately dissociated unless its off-diagonal entries are trivial, since X (i, j) and X (j, i) are then equal while separate dissociation asks them to be independent; it may perfectly well be jointly dissociated.

Index sets are presented, as in Arrays/Block/Basic.lean, by index maps e f : ℕ → ℕ. The two sub-arrays are the rectangular blocks arrayBlock X e f and arrayBlock X e' f' and the disjointness conditions read Disjoint (Set.range e) (Set.range e') and Disjoint (Set.range f) (Set.range f'). Ranges of maps ℕ → ℕ are exactly the nonempty sets of indices, and a block over an empty set of indices carries no information, so nothing is lost.

The same disjoint-block device that turns joint exchangeability into separate exchangeability also transfers dissociation. If e and f are injections with disjoint ranges, every rectangular block of arrayBlock X e f reads a square block of X on the union of its selected row and column indices. Thus joint dissociation of X makes this block separately dissociated (JointlyDissociated.separatelyDissociated_arrayBlock), including the pair-valued version that retains both orientations. This is the bridge from the ergodic jointly exchangeable branch to the separate Aldous--Hoover branch. For a separately exchangeable array law the block has the law of the array itself, so there joint and separate dissociation coincide (SeparatelyExchangeable.separatelyDissociated_iff_jointlyDissociated).

Dissociation is a restriction on the array and not a consequence of any exchangeability: an array all of whose entries are one common random variable is separately exchangeable, but dissociating it forces that variable to be almost surely trivial (JointlyDissociated.measure_preimage_eq_zero_or_one_of_const). Thus nontrivial randomness shared unchanged by every entry is incompatible with dissociation; the ergodic Aldous--Hoover coding drops the global noise coordinate entirely.

These results advance the exchangeable-arrays milestone of TauCetiRoadmap/Exchangeability/README.md, Layer 8. The dissociated codings themselves are in Arrays/AldousHoover/Dissociated.lean.

Main definitions

• TauCeti.Probability.SeparatelyDissociated;
• TauCeti.Probability.JointlyDissociated.

Main results

• TauCeti.Probability.SeparatelyDissociated.jointlyDissociated — the implication between the two notions;
• TauCeti.Probability.separatelyDissociated_of_iIndepFun — an array of independent entries is separately dissociated;
• TauCeti.Probability.SeparatelyDissociated.arrayBlock and TauCeti.Probability.JointlyDissociated.arrayBlock_diag — dissociation passes to blocks along injective index maps;
• TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlock and TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlockPair — a block along two injections with disjoint ranges converts joint dissociation to separate dissociation;
• TauCeti.Probability.SeparatelyExchangeable.separatelyDissociated_iff_jointlyDissociated — for a separately exchangeable array law the two notions coincide;
• TauCeti.Probability.SeparatelyDissociated.map_values and TauCeti.Probability.JointlyDissociated.map_values — dissociation is preserved by a measurable coordinatewise pushforward;
• TauCeti.Probability.JointlyDissociated.indep_blockSigma_prod_self — square blocks over arbitrary disjoint index sets generate independent σ-algebras;
• TauCeti.Probability.jointlyDissociated_iff_indep_blockSigma_finset — conversely, independence of the square blocks over disjoint finite index sets already gives joint dissociation;
• TauCeti.Probability.SeparatelyDissociated.indepFun_apply and TauCeti.Probability.JointlyDissociated.indepFun_arrayDiag — entries in different rows and different columns are independent, so in particular the diagonal entries of a jointly dissociated array are pairwise independent;
• TauCeti.Probability.JointlyDissociated.measure_preimage_eq_zero_or_one_of_const — a dissociated array with all entries equal has an almost surely trivial entry;
• TauCeti.Probability.SeparatelyDissociated.measure_preimage_eq_zero_or_one_of_symm — a symmetric array is separately dissociated only if it is trivial off the diagonal, which is the sharp form of the separation between the two notions.

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.

No material is adapted from cameronfreer/exchangeability, which treats exchangeable sequences rather than exchangeable arrays.

def TauCeti.Probability.SeparatelyDissociated {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ × ℕ → Ω → α) : Prop

Separate dissociation. Two rectangular blocks of the array are independent whenever their row index sets are disjoint and their column index sets are disjoint. The blocks are arrayBlock X e f and arrayBlock X e' f', read as random elements of array space.

Equations

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

def TauCeti.Probability.JointlyDissociated {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ × ℕ → Ω → α) : Prop

Joint dissociation. Two square blocks of the array, over disjoint sets of indices, are independent. This is the notion a symmetric array can have: separate dissociation would ask X (i, j) and X (j, i) to be independent, and a symmetric array has them equal, which forces them to be trivial (SeparatelyDissociated.measure_preimage_eq_zero_or_one_of_symm).

Equations

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

@[simp]

theorem TauCeti.Probability.separatelyDissociated_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} : SeparatelyDissociated μ X ↔ ∀ (e f e' f' : ℕ → ℕ), Disjoint (Set.range e) (Set.range e') → Disjoint (Set.range f) (Set.range f') → ProbabilityTheory.IndepFun (fun (ω : Ω) (p : ℕ × ℕ) => X (e p.1, f p.2) ω) (fun (ω : Ω) (p : ℕ × ℕ) => X (e' p.1, f' p.2) ω) μ

The independence law defining separate dissociation, as a restatement: it is the simp normal form of the predicate, and serves as both its introduction and its elimination rule.

@[simp]

theorem TauCeti.Probability.jointlyDissociated_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} : JointlyDissociated μ X ↔ ∀ (e e' : ℕ → ℕ), Disjoint (Set.range e) (Set.range e') → ProbabilityTheory.IndepFun (fun (ω : Ω) (p : ℕ × ℕ) => X (e p.1, e p.2) ω) (fun (ω : Ω) (p : ℕ × ℕ) => X (e' p.1, e' p.2) ω) μ

The independence law defining joint dissociation, as a restatement: it is the simp normal form of the predicate, and serves as both its introduction and its elimination rule.

theorem TauCeti.Probability.SeparatelyDissociated.jointlyDissociated {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyDissociated μ X) : JointlyDissociated μ X

Separate dissociation implies joint dissociation: a square block is the rectangular block with the two index maps equal.

theorem TauCeti.Probability.JointlyDissociated.indep_blockSigma_prod_self {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h : JointlyDissociated μ X) {S T : Set ℕ} (hd : Disjoint S T) : ProbabilityTheory.Indep (blockSigma X (S ×ˢ S)) (blockSigma X (T ×ˢ T)) μ

Square blocks over arbitrary disjoint index sets are independent. This is the σ-algebra form of joint dissociation. Empty blocks generate the bottom σ-algebra; the normalization assumption is needed for the bottom σ-algebra to be independent of every σ-algebra.

theorem TauCeti.Probability.jointlyDissociated_of_indep_blockSigma_finset {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : ∀ (p : ℕ × ℕ), Measurable (X p)) (h : ∀ (I J : Finset ℕ), Disjoint I J → ProbabilityTheory.Indep (blockSigma X (↑I ×ˢ ↑I)) (blockSigma X (↑J ×ˢ ↑J)) μ) : JointlyDissociated μ X

Joint dissociation from finite blocks. A coordinatewise measurable array is jointly dissociated as soon as its square blocks over disjoint finite index sets are independent: the square block over the range of an index map is exhausted by the increasing square blocks over its finite initial images.

theorem TauCeti.Probability.jointlyDissociated_iff_indep_blockSigma_finset {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : ∀ (p : ℕ × ℕ), Measurable (X p)) : JointlyDissociated μ X ↔ ∀ (I J : Finset ℕ), Disjoint I J → ProbabilityTheory.Indep (blockSigma X (↑I ×ˢ ↑I)) (blockSigma X (↑J ×ˢ ↑J)) μ

Joint dissociation is independence of finite square blocks for a coordinatewise measurable array under a zero-or-probability measure: it suffices to test the square blocks over disjoint finite index sets.

theorem TauCeti.Probability.jointlyDissociated_iff_indepFun_restrict {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : ∀ (p : ℕ × ℕ), Measurable (X p)) : JointlyDissociated μ X ↔ ∀ (I J : Finset ℕ), Disjoint I J → ProbabilityTheory.IndepFun (fun (ω : Ω) => (I ×ˢ I).restrict fun (p : ℕ × ℕ) => X p ω) (fun (ω : Ω) => (J ×ˢ J).restrict fun (p : ℕ × ℕ) => X p ω) μ

Joint dissociation is independence of the restrictions of the array to every pair of disjoint finite square blocks.

theorem TauCeti.Probability.SeparatelyDissociated.indepFun_apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyDissociated μ X) {i j i' j' : ℕ} (hi : i ≠ i') (hj : j ≠ j') : ProbabilityTheory.IndepFun (X (i, j)) (X (i', j')) μ

Entries of a separately dissociated array in different rows and different columns are independent.

theorem TauCeti.Probability.JointlyDissociated.indepFun_arrayDiag {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) {i i' : ℕ} (hi : i ≠ i') : ProbabilityTheory.IndepFun (arrayDiag X i) (arrayDiag X i') μ

The diagonal entries of a jointly dissociated array are pairwise independent.

theorem TauCeti.Probability.JointlyDissociated.measure_preimage_eq_zero_or_one_of_const {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → α} (hY : Measurable Y) (h : JointlyDissociated μ fun (x : ℕ × ℕ) => Y) {s : Set α} (hs : MeasurableSet s) : μ (Y ⁻¹' s) = 0 ∨ μ (Y ⁻¹' s) = 1

Dissociation makes a constant array trivial. If every entry of a jointly dissociated array is one and the same random variable Y, then Y generates an almost surely trivial σ-algebra.

In particular, the array X (i, j) = U built from global noise alone is separately exchangeable, but dissociating it would make U degenerate.

theorem TauCeti.Probability.SeparatelyDissociated.measure_preimage_eq_zero_or_one_of_symm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} [MeasureTheory.IsProbabilityMeasure μ] (h : SeparatelyDissociated μ X) {i j : ℕ} (hij : i ≠ j) (hsymm : X (j, i) = X (i, j)) (hX : Measurable (X (i, j))) {s : Set α} (hs : MeasurableSet s) : μ (X (i, j) ⁻¹' s) = 0 ∨ μ (X (i, j) ⁻¹' s) = 1

Equal transposed entries of a separately dissociated array are trivial off the diagonal. Separate dissociation asks X (i, j) and X (j, i) to be independent, so if those two entries are equal, they are self-independent. This applies in particular to symmetric arrays.

theorem TauCeti.Probability.SeparatelyDissociated.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyDissociated μ X) {g : α → β} (hg : Measurable g) : SeparatelyDissociated μ fun (p : ℕ × ℕ) (ω : Ω) => g (X p ω)

Dissociation is preserved by a measurable coordinatewise pushforward of the entries.

theorem TauCeti.Probability.JointlyDissociated.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) {g : α → β} (hg : Measurable g) : JointlyDissociated μ fun (p : ℕ × ℕ) (ω : Ω) => g (X p ω)

Joint dissociation is preserved by a measurable coordinatewise pushforward of the entries.

theorem TauCeti.Probability.SeparatelyDissociated.arrayBlock {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyDissociated μ X) {e f : ℕ → ℕ} (he : Function.Injective e) (hf : Function.Injective f) : SeparatelyDissociated μ (Probability.arrayBlock X e f)

Dissociation passes to rectangular blocks along injective index maps: a block of a block is a block, and an injection carries disjoint index sets to disjoint index sets.

theorem TauCeti.Probability.JointlyDissociated.arrayBlock_diag {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) {e : ℕ → ℕ} (he : Function.Injective e) : JointlyDissociated μ (arrayBlock X e e)

Joint dissociation passes to the diagonal blocks along an injective index map.

theorem TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlockPair {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) {e f : ℕ → ℕ} (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) : SeparatelyDissociated μ (arrayBlockPair X e f)

A two-orientation block of a jointly dissociated array is separately dissociated. The row and column injections must have disjoint ranges. Each rectangular block of the pair-valued array then reads a square block of the original array on the union of its row and column indices; the two unions are disjoint when both pairs of rectangular index sets are disjoint.

theorem TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlock {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) {e f : ℕ → ℕ} (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) : SeparatelyDissociated μ (arrayBlock X e f)

A rectangular block of a jointly dissociated array is separately dissociated when its row and column injections have disjoint ranges. This is the one-orientation consequence of JointlyDissociated.separatelyDissociated_arrayBlockPair.

The canonical block, along the even and the odd indices

theorem TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlock_evenOdd {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) : SeparatelyDissociated μ (arrayBlock X (fun (i : ℕ) => 2 * i) fun (j : ℕ) => 2 * j + 1)

The canonical separately dissociated block of a jointly dissociated array: read the rows along the even indices and the columns along the odd ones.

theorem TauCeti.Probability.JointlyDissociated.separatelyDissociated_arrayBlockPair_evenOdd {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyDissociated μ X) : SeparatelyDissociated μ (arrayBlockPair X (fun (i : ℕ) => 2 * i) fun (j : ℕ) => 2 * j + 1)

The canonical separately dissociated block of pairs of a jointly dissociated array.

theorem TauCeti.Probability.SeparatelyExchangeable.separatelyDissociated_iff_jointlyDissociated {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : (SeparatelyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p

Under separate exchangeability, joint and separate dissociation coincide. A separately exchangeable finite measure on arrays is separately dissociated if and only if it is jointly dissociated.

theorem TauCeti.Probability.separatelyDissociated_of_iIndepFun {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (p : ℕ × ℕ), Measurable (X p)) : SeparatelyDissociated μ X

An array of independent entries is separately dissociated. The two blocks read disjoint sets of entries, because their row index sets already are disjoint.