Vertex noise for the strips of an exchangeable array

Fix injective enumerations e and f of hidden rows and hidden columns of a separately exchangeable array, and injective enumerations g and g' of visible rows and visible columns, disjoint from the hidden ones. The hidden block is (x (e a, f b))_{a,b}; the row strip of the visible row g i is (x (g i, f b))_b, and the column strip of the visible column g' j is (x (e a, g' j))_a.

Given the hidden block, the row strips are i.i.d., the column strips are i.i.d., and the two families are conditionally independent. Consequently the hidden block together with all visible row and column strips is generated from the hidden block by two measurable maps fed with one uniform variable per visible row and one per visible column, all independent:

(H, (x (g i, f ·))ᵢ, (x (e ·, g' j))ⱼ) =ᵈ (H, (r H Uᵢ)ᵢ, (c H Vⱼ)ⱼ).

These are the row and column noises of the Aldous–Hoover representation of a separately exchangeable array. The row strip and column strip of a visible cell, together with the hidden block, form its cellContext, from which the cell itself is generated by a common kernel.

For a jointly exchangeable array the rows and columns share one set of vertices, and the hidden data is the hidden square (x (e a, e b))_{a,b}. The data of a vertex k consist of both orientations of its entries against the hidden vertices, (x (k, e b), x (e b, k))_b, together with its diagonal entry x (k, k). Unlike a hidden row of a separately exchangeable array, the data of a hidden vertex e a overlap the hidden square, so they need not have the law of a visible vertex and cannot serve as an identically distributed observed sample. So a second infinite set of vertices, enumerated by d, is kept as a reservoir: its vertex data have the law of the visible ones and recover their directing law. A relabelling of the reservoir and visible vertices fixing the hidden ones leaves the hidden square unchanged, so the visible strips and diagonal entries are coded from the hidden square and the reservoir data R by one uniform variable per visible vertex:

((H, R), ((x (g i, e ·), x (e ·, g i)), x (g i, g i))ᵢ)
  =ᵈ ((H, R), (v (H, R) Uᵢ)ᵢ).

Main results

• TauCeti.Probability.SeparatelyExchangeable.exists_vertex_strip_coding — the visible row and column strips are coded from the hidden block by independent i.i.d. uniform row and column noise.
• TauCeti.Probability.JointlyExchangeable.exists_vertex_strip_diagonal_coding — the visible vertex strips and diagonal entries of a jointly exchangeable array are coded from the hidden square and a reservoir of vertex data by independent i.i.d. uniform vertex noise.

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.

theorem TauCeti.Probability.SeparatelyExchangeable.exists_vertex_strip_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e f g g' : ℕ → ℕ} (he : Function.Injective e) (hf : Function.Injective f) (hg : Function.Injective g) (hg' : Function.Injective g') (heg : Disjoint (Set.range e) (Set.range g)) (hfg' : Disjoint (Set.range f) (Set.range g')) : ∃ (r : (ℕ × ℕ → α) → ↑unitInterval → ℕ → α) (c : (ℕ × ℕ → α) → ↑unitInterval → ℕ → α), Measurable (Function.uncurry r) ∧ Measurable (Function.uncurry c) ∧ MeasureTheory.Measure.map (fun (p : (ℕ × ℕ → α) × (ℕ → ↑unitInterval) × (ℕ → ↑unitInterval)) => (p.1, fun (i : ℕ) => r p.1 (p.2.1 i), fun (j : ℕ) => c p.1 (p.2.2 j))) ((MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) (q : ℕ × ℕ) => x (e q.1, f q.2)) ρ).prod ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))) = MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (fun (q : ℕ × ℕ) => x (e q.1, f q.2), fun (i b : ℕ) => x (g i, f b), fun (j a : ℕ) => x (e a, g' j))) ρ

The crossing strips are coded by i.i.d. vertex noise given the hidden block. Let e, f enumerate hidden rows and columns and g, g' visible rows and columns, all injectively, with visible and hidden indices disjoint on each axis. There are jointly measurable r and c such that the hidden block, the visible row strips along f, and the visible column strips along e are jointly distributed as the hidden block, r applied to one fresh uniform variable per visible row, and c applied to one fresh uniform variable per visible column, all these uniforms being independent of each other and of the hidden block.

theorem TauCeti.Probability.JointlyExchangeable.exists_vertex_strip_diagonal_coding {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {e d g : ℕ → ℕ} (he : Function.Injective e) (hd : Function.Injective d) (hg : Function.Injective g) (hed : Disjoint (Set.range e) (Set.range d)) (heg : Disjoint (Set.range e) (Set.range g)) (hdg : Disjoint (Set.range d) (Set.range g)) : ∃ (v : (ℕ × ℕ → α) × (ℕ → (ℕ → α × α) × α) → ↑unitInterval → (ℕ → α × α) × α), Measurable (Function.uncurry v) ∧ MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => ((fun (q : ℕ × ℕ) => x (e q.1, e q.2), fun (k : ℕ) => (fun (b : ℕ) => (x (d k, e b), x (e b, d k)), x (d k, d k))), fun (i : ℕ) => (fun (b : ℕ) => (x (g i, e b), x (e b, g i)), x (g i, g i)))) ρ = MeasureTheory.Measure.map (fun (p : ((ℕ × ℕ → α) × (ℕ → (ℕ → α × α) × α)) × (ℕ → ↑unitInterval)) => (p.1, fun (i : ℕ) => v p.1 (p.2 i))) ((MeasureTheory.Measure.map (fun (x : ℕ × ℕ → α) => (fun (q : ℕ × ℕ) => x (e q.1, e q.2), fun (k : ℕ) => (fun (b : ℕ) => (x (d k, e b), x (e b, d k)), x (d k, d k)))) ρ).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

The vertex strips and diagonal are coded by i.i.d. vertex noise. Let e enumerate hidden vertices, d a reservoir of further vertices and g visible vertices, all injectively and with pairwise disjoint ranges. The data of a vertex k consist of the two-oriented strip (x (k, e b), x (e b, k))_b and the diagonal entry x (k, k). There is a jointly measurable v such that the hidden square, the reservoir vertex data and the visible vertex data are jointly distributed as the hidden square, the reservoir data, and v applied to them and to one fresh uniform variable per visible vertex. The uniforms are independent of each other and of the hidden data. Producing the diagonal from the same noise as its vertex strip supplies the contexts required by the off-diagonal-pair coding.