Block independence of an array law along relabellings and consecutive windows

For a law on ℕ × ℕ → α, independence of the Finset restrictions of the array to two square blocks I ×ˢ I, J ×ˢ J transports along any diagonal relabelling preserving the law, to the blocks over the relabelled sets. For a jointly exchangeable law the blocks may therefore be taken consecutive: independence of the windows [0, |I|)² and [|I|, |I| + |J|)² gives independence of the blocks over any two disjoint finite sets I, J, since a finitely supported permutation carries the two sets onto the two windows. This is the form in which independence of consecutive label windows, the shape of dissociation for a law on another carrier read into arrays, is compared with independence of all disjoint blocks.

Main results

• TauCeti.Probability.indepFun_restrict_map_of_map_pairReindex_eq — block independence transports along a law-preserving diagonal relabelling.
• TauCeti.Probability.indepFun_restrict_of_forall_Ico — for a jointly exchangeable law, consecutive windows suffice.

theorem TauCeti.Probability.indepFun_restrict_map_of_map_pairReindex_eq {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (σ : Equiv.Perm ℕ) (hρ : MeasureTheory.Measure.map (pairReindex σ σ) ρ = ρ) {I J : Finset ℕ} (h : ProbabilityTheory.IndepFun (fun (x : ℕ × ℕ → α) => (I ×ˢ I).restrict x) (fun (x : ℕ × ℕ → α) => (J ×ˢ J).restrict x) ρ) : ProbabilityTheory.IndepFun (fun (x : ℕ × ℕ → α) => (Finset.map (Equiv.toEmbedding σ) I ×ˢ Finset.map (Equiv.toEmbedding σ) I).restrict x) (fun (x : ℕ × ℕ → α) => (Finset.map (Equiv.toEmbedding σ) J ×ˢ Finset.map (Equiv.toEmbedding σ) J).restrict x) ρ

Block independence transports along a diagonal relabelling preserving the law: the blocks I ×ˢ I, J ×ˢ J independent under ρ give the blocks over σ '' I, σ '' J independent.

theorem TauCeti.Probability.indepFun_restrict_of_forall_Ico {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyExchangeable ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) (I J : Finset ℕ) (hIJ : Disjoint I J) (h : ProbabilityTheory.IndepFun (fun (x : ℕ × ℕ → α) => (Finset.Ico 0 I.card ×ˢ Finset.Ico 0 I.card).restrict x) (fun (x : ℕ × ℕ → α) => (Finset.Ico I.card (I.card + J.card) ×ˢ Finset.Ico I.card (I.card + J.card)).restrict x) ρ) : ProbabilityTheory.IndepFun (fun (x : ℕ × ℕ → α) => (I ×ˢ I).restrict x) (fun (x : ℕ × ℕ → α) => (J ×ˢ J).restrict x) ρ

Consecutive windows suffice. For a jointly exchangeable law, block independence at the consecutive windows [0, |I|)², [|I|, |I| + |J|)² gives block independence at the disjoint finite sets I, J.