Directing measures of strips from a hidden array block

Choose infinite sets of hidden rows and columns of a separately exchangeable array, enumerated by injections e and f. All row strips along f are conditionally i.i.d. with a directing law that is a measurable function of the hidden block (X (e i, f j)). The analogous statement for column strips uses the same hidden block.

These are the row and column directing laws used in the hidden/visible decomposition of a separately exchangeable array. In particular, after restricting to visible rows or columns with ConditionallyIIDWith.comp_injective, the witness still depends only on the hidden block. The statements concern conditioning on these directing laws; they do not assert that the row and column strips are independent of one another given the entire hidden block.

Only the recovering axis must be injectively enumerated: row-strip recovery needs injective e, and column-strip recovery needs injective f. Measurability is needed only on the hidden block; the remaining entries may be merely a.e. measurable.

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_rowStrip_directing_of_injective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hblock : ∀ (i j : ℕ), Measurable (X (e i, f j))) : ∃ (R : (ℕ × ℕ → α) → MeasureTheory.ProbabilityMeasure (ℕ → α)), Measurable R ∧ ConditionallyIIDWith μ (fun (i : ℕ) (ω : Ω) (j : ℕ) => X (i, f j) ω) fun (ω : Ω) => R fun (p : ℕ × ℕ) => X (e p.1, f p.2) ω

The row strips along f admit a directing law measurable in the block selected by e and f. Only e must be injective: infinitely many selected rows determine the directing law of all the row strips.

theorem TauCeti.Probability.SeparatelyExchangeable.exists_colStrip_directing_of_injective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (hf : Function.Injective f) (hblock : ∀ (i j : ℕ), Measurable (X (e i, f j))) : ∃ (C : (ℕ × ℕ → α) → MeasureTheory.ProbabilityMeasure (ℕ → α)), Measurable C ∧ ConditionallyIIDWith μ (fun (j : ℕ) (ω : Ω) (i : ℕ) => X (e i, j) ω) fun (ω : Ω) => C fun (p : ℕ × ℕ) => X (e p.1, f p.2) ω

The column strips along e admit a directing law measurable in the block selected by e and f. Only f must be injective. Together with the row-strip theorem, this gives both directing laws as measurable functions of one common hidden block.