Documentation

TauCeti.Probability.Exchangeability.Arrays.AldousHoover.Dissociated

Global-free Aldous--Hoover codings are dissociated #

Coding through a function that ignores its global variable gives the ergodic form of the Aldous--Hoover representation, and the arrays it produces are dissociated as well as exchangeable: two blocks over disjoint row sets and disjoint column sets read disjoint sets of noise coordinates once the global one is out of the way, and the noise coordinates are independent. This is the easy direction of the ergodic form of the theorem. The shared global coordinate obstructs this disjoint-noise proof, and a nontrivial array built from global noise alone is not dissociated, by JointlyDissociated.measure_preimage_eq_zero_or_one_of_const.

Conversely, the global variable of any coding of a dissociated law can be dropped: freezing it at almost any value leaves the law unchanged. Freezing the global argument of a coding f at t leaves the frozen coding (a, b, c) ↦ f (t, a, b, c), which reads no global noise. Since the global noise coordinate is uniform and independent of the coordinates the frozen codings read, the law of f is the mixture of the laws of its frozen codings over a uniform t (map_jointArray_eq_bind_frozen, map_separateArray_eq_bind_frozen). Read from right to left this identity also assembles one coding out of a measurable family of global-free ones. Each frozen coding is jointly exchangeable, and a jointly dissociated law is not a nontrivial mixture of jointly exchangeable laws (JointlyDissociated.ae_eq_of_comp_eq), so almost every frozen coding has the original law. Hence the ergodic form of the representation follows from the general one, for both array symmetries; and since the frozen codings of a separate coding are separately exchangeable, hence jointly exchangeable, the separate statement too needs only joint dissociation of the law.

Main results #

References #

No material is adapted from cameronfreer/exchangeability, which treats sequences rather than exchangeable arrays.

source
theorem TauCeti.Probability.AldousHoover.separatelyDissociated_separateArray_of_snd {α : Type u_1} [MeasurableSpace α] (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hg : Measurable g) :
SeparatelyDissociated (noiseMeasure Axis (ℕ × ℕ)) (separateArray fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => g q.2)

A separate Aldous--Hoover coding that ignores its global variable is dissociated. This is the easy direction of the ergodic form of the representation; the coded array is also separately exchangeable, by separatelyExchangeable_separateArray applied to fun q => g q.2.

source
theorem TauCeti.Probability.AldousHoover.jointlyDissociated_jointArray_of_snd {α : Type u_1} [MeasurableSpace α] (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → α) (hg : Measurable g) :
JointlyDissociated (noiseMeasure Unit (Sym2 ℕ)) (jointArray fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => g q.2)

A joint Aldous--Hoover coding that ignores its global variable is jointly dissociated. It need not be separately dissociated: the entries X (i, j) and X (j, i) read the same cell variable u (.cell s(i, j)), and for a coding through a symmetric g they are equal, which SeparatelyDissociated.measure_preimage_eq_zero_or_one_of_symm rules out unless they are trivial. The coded array is also jointly exchangeable, by jointlyExchangeable_jointArray applied to fun q => g q.2.

Freezing the global variable #

The joint coding #

source
theorem TauCeti.Probability.AldousHoover.map_jointArray_eq_bind_frozen {α : Type u_1} [MeasurableSpace α] {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) :
MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray f p u) (noiseMeasure Unit (Sym2 ℕ)) = MeasureTheory.volume.bind fun (t : ↑unitInterval) => MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q.2)) p u) (noiseMeasure Unit (Sym2 ℕ))

The law of a joint Aldous--Hoover coding is the uniform mixture of the laws of its frozen codings. Freezing the global argument of f at t leaves the coding (a, b, c) ↦ f (t, a, b, c), which reads no global noise; averaging the law of the array it codes over a uniform t returns the law of the original coding.

source
theorem TauCeti.Probability.AldousHoover.ae_map_jointArray_eq_of_jointlyDissociated {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) (hcode : MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray f p u) (noiseMeasure Unit (Sym2 ℕ)) = ρ) :
∀ᵐ (t : ↑unitInterval), MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q.2)) p u) (noiseMeasure Unit (Sym2 ℕ)) = ρ

For a dissociated law, almost every frozen global value gives an Aldous--Hoover coding. If a measurable joint coding f has a jointly dissociated law ρ, then for almost every value t of the global variable, the coding (a, b, c) ↦ f (t, a, b, c), which ignores the global variable, already has law ρ.

source
theorem TauCeti.Probability.AldousHoover.exists_map_jointArray_snd_eq_of_jointlyDissociated {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) (hcode : MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray f p u) (noiseMeasure Unit (Sym2 ℕ)) = ρ) :
∃ (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → α), Measurable g ∧ MeasureTheory.Measure.map (fun (u : NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => jointArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => g q.2) p u) (noiseMeasure Unit (Sym2 ℕ)) = ρ

A dissociated law with an Aldous--Hoover coding has one that ignores its global variable. This is the ergodic form of the representation, obtained from a coding of the general form.

The separate coding #

source
theorem TauCeti.Probability.AldousHoover.map_separateArray_eq_bind_frozen {α : Type u_1} [MeasurableSpace α] {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) :
MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray f p u) (noiseMeasure Axis (ℕ × ℕ)) = MeasureTheory.volume.bind fun (t : ↑unitInterval) => MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q.2)) p u) (noiseMeasure Axis (ℕ × ℕ))

The law of a separate Aldous--Hoover coding is the uniform mixture of the laws of its frozen codings, the separate form of map_jointArray_eq_bind_frozen.

source
theorem TauCeti.Probability.AldousHoover.ae_map_separateArray_eq_of_jointlyDissociated {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) (hcode : MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray f p u) (noiseMeasure Axis (ℕ × ℕ)) = ρ) :
∀ᵐ (t : ↑unitInterval), MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q.2)) p u) (noiseMeasure Axis (ℕ × ℕ)) = ρ

For a dissociated law, almost every frozen global value gives a separate Aldous--Hoover coding. The frozen codings are separately exchangeable, hence jointly exchangeable, so joint dissociation of the law is all the argument needs; a separately dissociated law supplies it through SeparatelyDissociated.jointlyDissociated.

source
theorem TauCeti.Probability.AldousHoover.exists_map_separateArray_snd_eq_of_jointlyDissociated {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ × ℕ → α)} (hρ : JointlyDissociated ρ fun (p : ℕ × ℕ) (x : ℕ × ℕ → α) => x p) {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → α} (hf : Measurable f) (hcode : MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray f p u) (noiseMeasure Axis (ℕ × ℕ)) = ρ) :
∃ (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → α), Measurable g ∧ MeasureTheory.Measure.map (fun (u : NoiseIndex Axis (ℕ × ℕ) → ↑unitInterval) (p : ℕ × ℕ) => separateArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => g q.2) p u) (noiseMeasure Axis (ℕ × ℕ)) = ρ

A dissociated law with a separate Aldous--Hoover coding has one that ignores its global variable. This is the ergodic form of the separate representation, obtained from a coding of the general form; the coding it produces is separately dissociated again, by separatelyDissociated_separateArray_of_snd.