Documentation

TauCeti.Probability.Exchangeability.Arrays.Block.Basic

Rectangular blocks of an exchangeable array #

Joint exchangeability alone guarantees only invariance under the diagonal reindexing (i, j) ↦ (σ i, σ j), so the rows of a jointly exchangeable array need not be exchangeable and the separately exchangeable theory does not apply to it in general. This file supplies the standard device that repairs this: read the array on a rectangular block arrayBlock X e f, whose (i, j)-entry is X (e i, f j), along two injections e, f : ℕ → ℕ with disjoint ranges. On such a block the single permutation the array is invariant under has two independent halves — one permutation may be prescribed on the range of e and another, unrelated one on the range of f, because a permutation of ℕ is free to act differently on two disjoint sets — and the block is therefore separately exchangeable (JointlyExchangeable.separatelyExchangeable_arrayBlock). Every theorem about separately exchangeable arrays is then available for it; in particular de Finetti's theorem makes the rows of the block conditionally i.i.d.

The block only sees the entries X (e i, f j), so it omits the reverse-orientation entries X (f j, e i). Reading the two together as an array of pairs retains both orientations of the selected rectangular cross-block, and the pair array is separately exchangeable (JointlyExchangeable.separatelyExchangeable_arrayBlockPair). For a symmetric array the two coordinates of each such pair agree.

Main definitions #

Main results #

References #

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

Blocks of an array #

source
def TauCeti.Probability.arrayBlock {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (e f : ℕ → ℕ) :
ℕ × ℕ → Ω → α

The rectangular block of the array X along the index maps e and f: its (i, j)-entry is the (e i, f j)-entry of X.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.arrayBlock_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (e f : ℕ → ℕ) (p : ℕ × ℕ) :
    arrayBlock X e f p = X (e p.1, f p.2)
    source
    def TauCeti.Probability.arrayBlockPair {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (e f : ℕ → ℕ) :
    ℕ × ℕ → Ω → α × α

    The rectangular block of X along e and f, read together with its transpose: its (i, j)-entry is the pair of the (e i, f j)-entry and the (f j, e i)-entry of X.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Probability.arrayBlockPair_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ × ℕ → Ω → α) (e f : ℕ → ℕ) (p : ℕ × ℕ) (ω : Ω) :
      arrayBlockPair X e f p ω = (X (e p.1, f p.2) ω, X (f p.2, e p.1) ω)
      source
      theorem TauCeti.Probability.aemeasurable_arrayBlock {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (p : ℕ × ℕ) :
      AEMeasurable (arrayBlock X e f p) μ

      Entrywise measurability passes to a block: the p-entry of arrayBlock X e f is the (e p.1, f p.2)-entry of X. A consumer cannot read this off the hypothesis on its own, since arrayBlock does not unfold outside this file.

      source
      theorem TauCeti.Probability.aemeasurable_arrayBlockPair {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (p : ℕ × ℕ) :
      AEMeasurable (arrayBlockPair X e f p) μ

      Entrywise measurability passes to a block read together with its transpose: the p-entry of arrayBlockPair X e f pairs two entries of X.

      source
      theorem TauCeti.Probability.measurable_blockReadOff {α : Type u_1} [MeasurableSpace α] (e f : ℕ → ℕ) :
      Measurable fun (x : ℕ × ℕ → α) (p : ℕ × ℕ) => x (e p.1, f p.2)

      Reading a block off an array's sample path is measurable.

      source
      theorem TauCeti.Probability.measurable_blockPairReadOff {α : Type u_1} [MeasurableSpace α] (e f : ℕ → ℕ) :
      Measurable fun (x : ℕ × ℕ → α) (p : ℕ × ℕ) => (x (e p.1, f p.2), x (f p.2, e p.1))

      Reading a block together with its transpose off an array's sample path is measurable.

      Blocks inherit the symmetry of the array #

      source
      theorem TauCeti.Probability.SeparatelyExchangeable.arrayBlock {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) :
      SeparatelyExchangeable μ (Probability.arrayBlock X e f)

      Separate exchangeability passes to every block along injections. No relation between the two ranges is needed.

      source
      theorem TauCeti.Probability.SeparatelyExchangeable.map_arrayBlock_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} [MeasureTheory.IsFiniteMeasure μ] (h : SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) :
      MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (e p.1, f p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

      A block of a separately exchangeable array along injections has the law of the array. No relation between the two ranges is needed.

      source
      theorem TauCeti.Probability.JointlyExchangeable.arrayBlock_diag {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e : ℕ → ℕ} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) :
      JointlyExchangeable μ (arrayBlock X e e)

      Joint exchangeability passes to diagonal blocks along an injection.

      source
      theorem TauCeti.Probability.JointlyExchangeable.map_arrayBlock_diag_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e : ℕ → ℕ} [MeasureTheory.IsFiniteMeasure μ] (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) :
      MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X (e p.1, e p.2) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => X p ω) μ

      A diagonal block of a jointly exchangeable array along an injection has the law of the array. Reading both axes along one injection e is, on every finite window, a single relabelling of the indices.

      source
      theorem TauCeti.Probability.JointlyExchangeable.separatelyExchangeable_arrayBlock {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) :
      SeparatelyExchangeable μ (arrayBlock X e f)

      A block of a jointly exchangeable array along injections with disjoint ranges is separately exchangeable.

      This makes separately exchangeable results, including de Finetti's theorem for the rows, available to the selected block.

      source
      theorem TauCeti.Probability.JointlyExchangeable.separatelyExchangeable_arrayBlockPair {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) :
      SeparatelyExchangeable μ (arrayBlockPair X e f)

      A block of a jointly exchangeable array, read in both orientations, is separately exchangeable. Its (i, j)-entry is (X (e i, f j), X (f j, e i)).

      The canonical block, along the even and the odd indices #

      source
      theorem TauCeti.Probability.JointlyExchangeable.separatelyExchangeable_arrayBlock_evenOdd {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) :
      SeparatelyExchangeable μ (arrayBlock X (fun (i : ℕ) => 2 * i) fun (j : ℕ) => 2 * j + 1)

      The canonical separately exchangeable block of a jointly exchangeable array: read the rows along the even indices and the columns along the odd ones. Any pair of injections with disjoint ranges would do; this one exists without further data, so it is the block a consumer with no preferred index sets should use.

      source
      theorem TauCeti.Probability.JointlyExchangeable.separatelyExchangeable_arrayBlockPair_evenOdd {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) :
      SeparatelyExchangeable μ (arrayBlockPair X (fun (i : ℕ) => 2 * i) fun (j : ℕ) => 2 * j + 1)

      The canonical block of pairs of a jointly exchangeable array.

      source
      theorem TauCeti.Probability.not_separatelyExchangeable_arrayBlock_diagIndicatorArray {Ω : Type u_2} [MeasurableSpace Ω] {e : ℕ → ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (he : Function.Injective e) :
      ¬SeparatelyExchangeable μ (arrayBlock (diagIndicatorArray Ω) e e)

      The disjointness hypothesis of JointlyExchangeable.separatelyExchangeable_arrayBlock cannot be omitted. Reading both axes along one and the same injection — the extreme case of overlapping ranges — the diagonal-indicator array gives a counterexample: the block is again the diagonal-indicator array, whose rows are not exchangeable.

      The block law is canonical #

      source
      theorem TauCeti.Probability.JointlyExchangeable.map_arrayBlock_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} [MeasureTheory.IsFiniteMeasure μ] {e' f' : ℕ → ℕ} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) (he' : Function.Injective e') (hf' : Function.Injective f') (hd' : Disjoint (Set.range e') (Set.range f')) :
      MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => arrayBlock X e f p ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => arrayBlock X e' f' p ω) μ

      The law of a block does not depend on the chosen pair of index maps. Any two pairs of injections with disjoint ranges give the same law; in particular, the canonical even-odd block computes it.

      source
      theorem TauCeti.Probability.JointlyExchangeable.map_arrayBlockPair_eq {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} [MeasureTheory.IsFiniteMeasure μ] {e' f' : ℕ → ℕ} (h : JointlyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) (he' : Function.Injective e') (hf' : Function.Injective f') (hd' : Disjoint (Set.range e') (Set.range f')) :
      MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => arrayBlockPair X e f p ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (p : ℕ × ℕ) => arrayBlockPair X e' f' p ω) μ

      The law of a pair-valued block does not depend on the chosen pair of index maps. Any two pairs of injections with disjoint ranges give the same law.