Conditional array laws given the corner tail

Condition a jointly exchangeable array law on its corner-tail σ-algebra. Almost every resulting conditional law is again jointly exchangeable, and it is jointly dissociated. These conditional laws are therefore the ergodic components in the decomposition used by the Aldous--Hoover representation. Constructing their vertex and cell noise is a separate step.

A separately exchangeable law keeps its stronger symmetry under the same conditioning, because a corner-tail event is fixed by relabelling the two axes independently, and not only by the diagonal relabellings. Its conditional laws are therefore separately exchangeable and jointly dissociated, which is the pair of properties the global-variable-free separate coding asks for.

We use Mathlib's condExpKernel on array path space. Although the conditioning σ-algebra need not be standard Borel, the space of arrays is standard Borel when the value space is. Thus no regularity assumption is imposed on a sample space carrying an original array process.

The corner-tail events are fixed by every finitely supported permutation. Disintegration uniqueness gives invariance of the conditional laws under each such permutation; countability puts these statements on one almost-sure set. Finite-dimensional determinacy then gives full joint exchangeability, including permutations with infinite support.

For dissociation, fix disjoint finite index sets I and J. Permutations fixing I and pushing J past n leave conditional probabilities given the tail unchanged and move the square block over J into the n-th corner-tail family. The conditional form of Lévy's downward factorization, MeasureTheory.condExp_inter_ae_eq_mul_iInf, then makes the square blocks over I and J conditionally independent given the tail. Mathlib's description of conditional independence through condExpKernel turns this into independence under almost every conditional law. Countably many pairs I, J share one null set, and independence of finite square blocks gives joint dissociation (jointlyDissociated_iff_indepFun_restrict).

Main results

• TauCeti.Probability.JointlyExchangeable.ae_jointlyExchangeable_condExpKernel_arrayTail — almost every conditional law given the corner tail is jointly exchangeable;
• TauCeti.Probability.SeparatelyExchangeable.ae_separatelyExchangeable_condExpKernel_arrayTail — almost every conditional law of a separately exchangeable law is separately exchangeable;
• TauCeti.Probability.JointlyExchangeable.ae_jointlyDissociated_condExpKernel_arrayTail — almost every conditional law given the corner tail is jointly dissociated.

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.JointlyExchangeable.ae_jointlyExchangeable_condExpKernel_arrayTail {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : ∀ᵐ (x : ℕ × ℕ → α) ∂ρ, JointlyExchangeable ((ProbabilityTheory.condExpKernel ρ (arrayTail fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p)) x) fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p

Almost every conditional law of a jointly exchangeable array, given its corner tail, is jointly exchangeable. The almost-sure set works simultaneously for all coordinate permutations.

theorem TauCeti.Probability.SeparatelyExchangeable.ae_separatelyExchangeable_condExpKernel_arrayTail {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : SeparatelyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : ∀ᵐ (x : ℕ × ℕ → α) ∂ρ, SeparatelyExchangeable ((ProbabilityTheory.condExpKernel ρ (arrayTail fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p)) x) fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p

Almost every conditional law of a separately exchangeable array, given its corner tail, is separately exchangeable. A corner-tail event is fixed by relabelling the two axes independently, not only diagonally, so the stronger symmetry survives the conditioning. The almost-sure set works simultaneously for all pairs of coordinate permutations.

theorem TauCeti.Probability.JointlyExchangeable.ae_jointlyDissociated_condExpKernel_arrayTail {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) : ∀ᵐ (x : ℕ × ℕ → α) ∂ρ, JointlyDissociated ((ProbabilityTheory.condExpKernel ρ (arrayTail fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p)) x) fun (p : ℕ × ℕ) (y : ℕ × ℕ → α) => y p

Almost every conditional law of a jointly exchangeable array, given its corner tail, is jointly dissociated. Together with JointlyExchangeable.ae_jointlyExchangeable_condExpKernel_arrayTail, almost every conditional law is a jointly exchangeable, jointly dissociated array law.