Exchangeable arrays

A doubly indexed array X : ℕ × ℕ → Ω → α carries two symmetry notions, and they are genuinely different:

• SeparatelyExchangeable μ X — the law of the array is unchanged when the two axes are permuted independently, by (i, j) ↦ (σ i, τ j);
• JointlyExchangeable μ X — the law is unchanged when the same permutation is applied to both axes, by (i, j) ↦ (σ i, σ j).

Separate exchangeability is the stronger notion (SeparatelyExchangeable.jointlyExchangeable). Joint exchangeability is the one to ask of a symmetric array X (i, j) = X (j, i), such as the adjacency array of an exchangeable random graph. Symmetry is a pathwise condition and by itself gives no invariance of the law; the point is rather that a joint reindexing (i, j) ↦ (σ i, σ j) carries a symmetric array to a symmetric array, whereas permuting the rows alone does not, so joint exchangeability is the invariance a symmetric array can consistently be asked to have.

The main theorem here is the first step of the standard route to the Aldous–Hoover representation: the rows of a separately exchangeable array form an exchangeable sequence of random paths (SeparatelyExchangeable.fullyExchangeable_arrayRow), so de Finetti's theorem applies to them and makes them conditionally i.i.d. That consequence is drawn in Arrays.DeFinetti, which is where this subtree meets the representation theory; the value space of the sequence is path space ℕ → α, standard Borel whenever α is, so it needs no hypothesis beyond de Finetti's own.

Main definitions

• TauCeti.Probability.pairReindex — the two-axis analogue of permReindex, reindexing an array-shaped path by a permutation of each axis.
• TauCeti.Probability.SeparatelyExchangeable, TauCeti.Probability.JointlyExchangeable — the two array symmetries.
• TauCeti.Probability.arrayRow, TauCeti.Probability.arrayCol, TauCeti.Probability.arrayDiag — the rows and columns of an array, as random elements of path space, and its diagonal, as a process.

Main results

• TauCeti.Probability.SeparatelyExchangeable.jointlyExchangeable — the implication between the two symmetries.
• TauCeti.Probability.separatelyExchangeable_iff_map_pairReindex — the bridge to the array law: separate exchangeability is invariance of the law on ℕ × ℕ → α under every pair reindexing, with TauCeti.Probability.SeparatelyExchangeable.measurePreserving_pairReindex its measure-preserving form.
• TauCeti.Probability.map_uncurry_pathLaw_arrayRow — the array law is the uncurried path law of the row process.
• TauCeti.Probability.separatelyExchangeable_iff_axes — separate exchangeability splits into invariance under row permutations and invariance under column permutations.
• TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_arrayRow and TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_arrayCol — the rows, and the columns, of a separately exchangeable array form fully exchangeable sequences of paths.
• TauCeti.Probability.JointlyExchangeable.fullyExchangeable_arrayDiag — the diagonal of a jointly exchangeable array is a fully exchangeable sequence.
• TauCeti.Probability.ExchangeableFamily.separatelyExchangeable and TauCeti.Probability.separatelyExchangeable_of_iIndepFun_identDistrib — the sources: an exchangeable family indexed by ℕ × ℕ, in particular an i.i.d. array, is separately exchangeable.
• TauCeti.Probability.jointlyExchangeable_diagIndicatorArray and TauCeti.Probability.not_separatelyExchangeable_diagIndicatorArray — the implication between the two symmetries is strict, witnessed by the deterministic diagonal-indicator array, whose rows are not exchangeable.

Implementation notes

The two predicates are stated at the level of the whole array law, matching FullyExchangeable rather than the finite-dimensional Exchangeable, and quantify over arbitrary permutations of ℕ. This is the formulation that makes the row and column statements pushforwards of one array law (map_map_array), and it is the one Kallenberg uses for infinite arrays. Every symmetry consequence below is an instance of SeparatelyExchangeable.map_comp or JointlyExchangeable.map_comp with a different measurable read-off F of the array's sample path.

The a.e.-measurability hypothesis ∀ p, AEMeasurable (X p) μ is what turns a law identity for the array into a law identity for a read-off; the definitions themselves are hypothesis-free.

The next law-level consequence of the row and column decompositions is in Arrays.MixingLaw: the law of either directing measure is invariant when every path coordinate is permuted. This is deliberately weaker than saying that the directing measure is almost surely an exchangeable law, which is false in general.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.
• D. Aldous, Representations for partially exchangeable arrays of random variables, Journal of Multivariate Analysis 11 (1981), 581–598.

Reindexing the two axes

def TauCeti.Probability.pairReindex {α : Type u_1} (σ τ : Equiv.Perm ℕ) (x : ℕ × ℕ → α) : ℕ × ℕ → α

Reindex an array-shaped path by a permutation of each axis: the (i, j)-entry of pairReindex σ τ x is x (σ i, τ j). This is the two-axis analogue of permReindex.

Equations

• TauCeti.Probability.pairReindex σ τ x p = x (σ p.1, τ p.2)

@[simp]

theorem TauCeti.Probability.pairReindex_apply {α : Type u_1} (σ τ : Equiv.Perm ℕ) (x : ℕ × ℕ → α) (p : ℕ × ℕ) : pairReindex σ τ x p = x (σ p.1, τ p.2)

theorem TauCeti.Probability.pairReindex_def {α : Type u_1} (σ τ : Equiv.Perm ℕ) : pairReindex σ τ = fun (x : ℕ × ℕ → α) (p : ℕ × ℕ) => x (σ p.1, τ p.2)

The function form of pairReindex.

@[simp]

theorem TauCeti.Probability.pairReindex_comp {α : Type u_1} (σ₁ τ₁ σ₂ τ₂ : Equiv.Perm ℕ) : pairReindex σ₁ τ₁ ∘ pairReindex σ₂ τ₂ = pairReindex (σ₂ * σ₁) (τ₂ * τ₁)

Reindexing both axes twice composes the corresponding permutations on each axis.

@[simp]

theorem TauCeti.Probability.pairReindex_one_one {α : Type u_1} : pairReindex 1 1 = id

Reindexing both axes by the identity permutation leaves an array unchanged.

Rows, columns and the diagonal

def TauCeti.Probability.arrayRow {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (i : ℕ) : Ω → ℕ → α

The i-th row of an array, as a random element of path space.

Equations

• TauCeti.Probability.arrayRow X i ω j = X (i, j) ω

def TauCeti.Probability.arrayCol {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (j : ℕ) : Ω → ℕ → α

The j-th column of an array, as a random element of path space.

Equations

• TauCeti.Probability.arrayCol X j ω i = X (i, j) ω

def TauCeti.Probability.arrayDiag {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (i : ℕ) : Ω → α

The diagonal of an array, as a process.

Equations

• TauCeti.Probability.arrayDiag X i = X (i, i)

@[simp]

theorem TauCeti.Probability.arrayRow_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (i : ℕ) (ω : Ω) (j : ℕ) : arrayRow X i ω j = X (i, j) ω

@[simp]

theorem TauCeti.Probability.arrayCol_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (j : ℕ) (ω : Ω) (i : ℕ) : arrayCol X j ω i = X (i, j) ω

@[simp]

theorem TauCeti.Probability.arrayDiag_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (i : ℕ) : arrayDiag X i = X (i, i)

def TauCeti.Probability.symmetricArraysWithDiag (α : Type u_3) (d : α) : Set (ℕ × ℕ → α)

The symmetric arrays with constant diagonal value d: x (i, j) = x (j, i) and x (i, i) = d. For α = Bool and d = false these are the adjacency arrays of the simple graphs on ℕ.

Equations

• TauCeti.Probability.symmetricArraysWithDiag α d = {x : ℕ × ℕ → α | (∀ (i j : ℕ), x (i, j) = x (j, i)) ∧ ∀ (i : ℕ), x (i, i) = d}

@[simp]

theorem TauCeti.Probability.mem_symmetricArraysWithDiag_iff {α : Type u_1} {d : α} {x : ℕ × ℕ → α} : x ∈ symmetricArraysWithDiag α d ↔ (∀ (i j : ℕ), x (i, j) = x (j, i)) ∧ ∀ (i : ℕ), x (i, i) = d

Membership in the symmetric arrays with diagonal d.

@[simp]

theorem TauCeti.Probability.preimage_pairReindex_symmetricArraysWithDiag {α : Type u_1} (σ : Equiv.Perm ℕ) (d : α) : pairReindex σ σ ⁻¹' symmetricArraysWithDiag α d = symmetricArraysWithDiag α d

The symmetric arrays with diagonal d are stable under diagonal relabelling.

@[simp]

theorem TauCeti.Probability.measurableSet_symmetricArraysWithDiag {α : Type u_1} [MeasurableSpace α] [MeasurableEq α] (d : α) : MeasurableSet (symmetricArraysWithDiag α d)

The symmetric arrays with diagonal d form a measurable set.

theorem TauCeti.Probability.measurable_pairReindex {α : Type u_1} [MeasurableSpace α] (σ τ : Equiv.Perm ℕ) : Measurable (pairReindex σ τ)

theorem TauCeti.Probability.aemeasurable_arrayRow {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (i : ℕ) : AEMeasurable (arrayRow X i) μ

theorem TauCeti.Probability.aemeasurable_arrayCol {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (j : ℕ) : AEMeasurable (arrayCol X j) μ

theorem TauCeti.Probability.aemeasurable_entry_of_aemeasurable_arrayRow {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : ∀ (i : ℕ), AEMeasurable (arrayRow X i) μ) (p : ℕ × ℕ) : AEMeasurable (X p) μ

Entry measurability from row measurability, the converse of aemeasurable_arrayRow. The entries are the coordinates of the rows, so this needs no probabilistic structure; a caller holding a mixed or conditional witness passes its aemeasurable.

theorem TauCeti.Probability.aemeasurable_entry_of_aemeasurable_arrayCol {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : ∀ (j : ℕ), AEMeasurable (arrayCol X j) μ) (p : ℕ × ℕ) : AEMeasurable (X p) μ

Entry measurability from column measurability, the converse of aemeasurable_arrayCol.

The two array symmetries

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

Separate exchangeability. The law of the array X is unchanged when its two axes are permuted independently.

Equations

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

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

Joint exchangeability. The law of the array X is unchanged when one and the same permutation is applied to both of its axes.

This, rather than separate exchangeability, is the hypothesis one puts on a symmetric array X (i, j) = X (j, i): reindexing both axes by the same permutation preserves pathwise symmetry, while permuting the rows alone destroys it. Symmetry alone is not an exchangeability assumption — it constrains the sample path, not the law.

Equations

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

@[simp]

theorem TauCeti.Probability.separatelyExchangeable_iff {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} : SeparatelyExchangeable μ X ↔ ∀ (σ τ : Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (σ p.1, τ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

The invariance law defining separate exchangeability, as a restatement: the array law is unchanged along every pair of axis permutations. This is the simp normal form of the predicate, and serves as both its introduction and its elimination rule.

@[simp]

theorem TauCeti.Probability.jointlyExchangeable_iff {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} : JointlyExchangeable μ X ↔ ∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (σ p.1, σ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

The invariance law defining joint exchangeability, as a restatement: the array law is unchanged along every diagonal pair of axis permutations. This is the simp normal form of the predicate, and serves as both its introduction and its elimination rule.

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

Separate exchangeability implies joint exchangeability: permuting both axes by the same permutation is the special case τ = σ.

Reading off the array law

theorem TauCeti.Probability.map_map_array {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {β : Type u_3} [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) {F : (ℕ × ℕ → α) → β} (hF : Measurable F) : MeasureTheory.Measure.map F (MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) = MeasureTheory.Measure.map (fun (ω : Ω) => F fun (p : ℕ × ℕ) => X p ω) μ

Reading a measurable function F off the sample path of an array turns the law of the array into a pushforward. Every symmetry consequence below is this lemma with a different F: currying for the rows, currying after a swap for the columns, restriction to the diagonal, evaluation at a single entry.

theorem TauCeti.Probability.SeparatelyExchangeable.map_comp {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {β : Type u_3} [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (σ τ : Equiv.Perm ℕ) {F : (ℕ × ℕ → α) → β} (hF : Measurable F) : MeasureTheory.Measure.map (fun (ω : Ω) => F fun (p : ℕ × ℕ) => X (σ p.1, τ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) => F fun (p : ℕ × ℕ) => X p ω) μ

Separate exchangeability, transported to any measurable read-off F of the array's sample path.

theorem TauCeti.Probability.JointlyExchangeable.map_comp {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {β : Type u_3} [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (σ : Equiv.Perm ℕ) {F : (ℕ × ℕ → α) → β} (hF : Measurable F) : MeasureTheory.Measure.map (fun (ω : Ω) => F fun (p : ℕ × ℕ) => X (σ p.1, σ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) => F fun (p : ℕ × ℕ) => X p ω) μ

Joint exchangeability, transported to any measurable read-off F of the array's sample path.

theorem TauCeti.Probability.separatelyExchangeable_iff_map_pairReindex {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : SeparatelyExchangeable μ X ↔ ∀ (σ τ : Equiv.Perm ℕ), MeasureTheory.Measure.map (pairReindex σ τ) (MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

Separate exchangeability is a property of the array law. It says exactly that the law of the array on ℕ × ℕ → α is invariant under every pair reindexing, which is the form in which a statement about a law rather than a process supplies it.

theorem TauCeti.Probability.JointlyExchangeable.map_pairReindex {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (pairReindex σ σ) ρ = ρ

A jointly exchangeable law on array path space is invariant under every diagonal relabelling.

theorem TauCeti.Probability.SeparatelyExchangeable.measurePreserving_pairReindex {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (σ τ : Equiv.Perm ℕ) : MeasureTheory.MeasurePreserving (pairReindex σ τ) ρ ρ

A separately exchangeable array law is preserved by every pair reindexing of array path space. This is the measure-preserving form of separatelyExchangeable_iff_map_pairReindex for the coordinate array.

theorem TauCeti.Probability.jointlyExchangeable_map_iff {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : (JointlyExchangeable (MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) ↔ JointlyExchangeable μ X

Joint exchangeability is a property of the array law: an array is jointly exchangeable exactly when the coordinate array under its law on ℕ × ℕ → α is.

theorem TauCeti.Probability.map_uncurry_pathLaw_arrayRow {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : MeasureTheory.Measure.map Function.uncurry (pathLaw μ (arrayRow X)) = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

An array law is the uncurried path law of its row process. A statement about the law of the row process therefore transports to one about the law of the array.

Splitting separate exchangeability into its two axes

theorem TauCeti.Probability.separatelyExchangeable_iff_axes {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : SeparatelyExchangeable μ X ↔ (∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (σ p.1, p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ) ∧ ∀ (τ : Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (p.1, τ p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

Separate exchangeability splits into its two axes: it is the conjunction of invariance under a permutation of the rows and invariance under a permutation of the columns. The forward direction is the two specializations τ = 1 and σ = 1; the converse composes the two pushforwards, which is where measurability of the coordinates is used.

Rows and columns of a separately exchangeable array

theorem TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_arrayRow {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : FullyExchangeable μ (arrayRow X)

The rows of a separately exchangeable array form a fully exchangeable sequence of random paths: permuting the rows is the case τ = 1 of separate exchangeability, read off by currying.

theorem TauCeti.Probability.SeparatelyExchangeable.exchangeable_arrayRow {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : Exchangeable μ (arrayRow X)

The rows of a separately exchangeable array form an exchangeable sequence of random paths.

theorem TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_arrayCol {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : FullyExchangeable μ (arrayCol X)

The columns of a separately exchangeable array form a fully exchangeable sequence of random paths.

theorem TauCeti.Probability.SeparatelyExchangeable.exchangeable_arrayCol {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : Exchangeable μ (arrayCol X)

The columns of a separately exchangeable array form an exchangeable sequence of random paths.

theorem TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_row {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (i : ℕ) : FullyExchangeable μ fun (j : ℕ) => X (i, j)

Each single row of a separately exchangeable array is a fully exchangeable sequence. This is the column half of the symmetry, read off at one row index.

theorem TauCeti.Probability.SeparatelyExchangeable.fullyExchangeable_col {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (j : ℕ) : FullyExchangeable μ fun (i : ℕ) => X (i, j)

Each single column of a separately exchangeable array is a fully exchangeable sequence.

theorem TauCeti.Probability.SeparatelyExchangeable.map_entry_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (p : ℕ × ℕ) : MeasureTheory.Measure.map (X p) μ = MeasureTheory.Measure.map (X (0, 0)) μ

The entries of a separately exchangeable array are identically distributed.

The diagonal of a jointly exchangeable array

theorem TauCeti.Probability.JointlyExchangeable.fullyExchangeable_arrayDiag {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : FullyExchangeable μ (arrayDiag X)

The diagonal of a jointly exchangeable array is a fully exchangeable sequence. Separate exchangeability is not needed: joint exchangeability alone already constrains the diagonal, which is what makes it a useful hypothesis on a jointly exchangeable symmetric array.

theorem TauCeti.Probability.JointlyExchangeable.exchangeable_arrayDiag {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : Exchangeable μ (arrayDiag X)

The diagonal of a jointly exchangeable array is an exchangeable sequence.

The two symmetries are distinct

def TauCeti.Probability.diagIndicatorArray (S : Type u_3) : ℕ × ℕ → S → Bool

The deterministic diagonal-indicator array over a sample space S: its (i, j) entry is true exactly when i = j. Under every measure it is jointly exchangeable, but under a probability measure it is not separately exchangeable.

Equations

• TauCeti.Probability.diagIndicatorArray S p x✝ = decide (p.1 = p.2)

@[simp]

theorem TauCeti.Probability.diagIndicatorArray_apply (S : Type u_3) (p : ℕ × ℕ) (s : S) : diagIndicatorArray S p s = decide (p.1 = p.2)

The entries of the diagonal-indicator array: constant in the sample point, and true exactly on the diagonal.

theorem TauCeti.Probability.jointlyExchangeable_diagIndicatorArray {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : JointlyExchangeable μ (diagIndicatorArray Ω)

The diagonal-indicator array is jointly exchangeable: permuting both axes by one injective map leaves the array itself, not merely its law, unchanged.

theorem TauCeti.Probability.not_fullyExchangeable_arrayRow_diagIndicatorArray {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ¬FullyExchangeable μ (arrayRow (diagIndicatorArray Ω))

The rows of the diagonal-indicator array are not exchangeable: they are the distinct deterministic paths j ↦ decide (i = j), so permuting them moves the point mass.

theorem TauCeti.Probability.not_separatelyExchangeable_diagIndicatorArray {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ¬SeparatelyExchangeable μ (diagIndicatorArray Ω)

Joint exchangeability is strictly weaker than separate exchangeability. The diagonal-indicator array is jointly exchangeable, but not separately so: separate exchangeability would make its rows exchangeable, and they are not.

Sources of separately exchangeable arrays

theorem TauCeti.Probability.ExchangeableFamily.separatelyExchangeable {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} (h : ExchangeableFamily μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) : SeparatelyExchangeable μ X

An exchangeable family indexed by ℕ × ℕ is a separately exchangeable array. The converse fails: ExchangeableFamily also constrains selections that no pair of axis permutations realizes, such as the one sending (0, 0), (0, 1) to (0, 0), (1, 1).

theorem TauCeti.Probability.separatelyExchangeable_of_iIndepFun_identDistrib {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (p : ℕ × ℕ), ProbabilityTheory.IdentDistrib (X p) (X (0, 0)) μ μ) : SeparatelyExchangeable μ X

An i.i.d. array is separately exchangeable. The non-vacuous base case of the definition: independence gives a product block law, and identical distribution makes that product blind to any reindexing of the two axes.

theorem TauCeti.Probability.jointlyExchangeable_of_iIndepFun_identDistrib {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (p : ℕ × ℕ), ProbabilityTheory.IdentDistrib (X p) (X (0, 0)) μ μ) : JointlyExchangeable μ X

An i.i.d. array is jointly exchangeable.