Documentation

TauCeti.Probability.Exchangeability.Arrays.Tail

Tail σ-algebras of arrays #

This file defines the corner tail of an array: the events readable from entries X (i, j) with both indices arbitrarily large. It is the two-dimensional analogue of the tail σ-algebra of a process, cutting both index axes at the same time, and it is the σ-algebra the zero-one law for a dissociated array in Arrays.ZeroOne is stated for. Cutting both axes is what dissociation asks for: two square blocks are independent only when their index sets are disjoint, so a one-axis cut would not do.

The corner tail need not be the tail of the diagonal process arrayDiag X; it contains it (tailProcess_arrayDiag_le_arrayTail) and may additionally read off-diagonal entries above the cutoff.

These definitions support the exchangeable-arrays milestone of TauCetiRoadmap/Exchangeability/README.md, Layer 8.

Main definitions #

Main results #

source
@[implicit_reducible]
def TauCeti.Probability.arrayTailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) (n : ℕ) :
MeasurableSpace Ω

The tail family of an array at time n: the events readable from the entries X (i, j) with n ≤ i and n ≤ j. It is the array analogue of the future σ-algebra tailFamily of a process, cutting both index axes at once.

Equations
Instances For
    source
    @[implicit_reducible]
    def TauCeti.Probability.arrayTail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) :
    MeasurableSpace Ω

    The tail σ-algebra of an array: the events readable from the entries with both indices arbitrarily large. It is the array analogue of tailProcess.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Probability.arrayTailFamily_eq_blockSigma {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) (n : ℕ) :
      arrayTailFamily X n = blockSigma X (Set.Ici n ×ˢ Set.Ici n)

      Normal form for the array tail family.

      source
      @[simp]
      theorem TauCeti.Probability.arrayTail_eq_iInf_arrayTailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) :
      arrayTail X = ⨅ (n : ℕ), arrayTailFamily X n

      Normal form for the tail σ-algebra of an array.

      source
      theorem TauCeti.Probability.measurable_arrayTailFamily_of_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} {n i j : ℕ} (hi : n ≤ i) (hj : n ≤ j) :
      Measurable (X (i, j))

      An entry with both indices at least n is measurable for the array tail family at n.

      source
      theorem TauCeti.Probability.arrayTailFamily_le_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} {n : ℕ} {m : MeasurableSpace Ω} :
      arrayTailFamily X n ≤ m ↔ ∀ (i j : ℕ), n ≤ i → n ≤ j → Measurable (X (i, j))

      Universal property of the array tail family at n.

      source
      theorem TauCeti.Probability.arrayTailFamily_antitone {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) :
      Antitone (arrayTailFamily X)

      The array tail family decreases.

      source
      theorem TauCeti.Probability.arrayTailFamily_eq_iSup_Icc {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) (n : ℕ) :
      arrayTailFamily X n = ⨆ (k : ℕ), blockSigma X (Set.Icc n (n + k) ×ˢ Set.Icc n (n + k))

      The finite corners above n exhaust the array tail family at n.

      source
      theorem TauCeti.Probability.arrayTail_le_arrayTailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) (n : ℕ) :
      arrayTail X ≤ arrayTailFamily X n

      The tail σ-algebra of an array sits inside every member of its tail family.

      source
      theorem TauCeti.Probability.le_arrayTail_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} {m : MeasurableSpace Ω} :
      m ≤ arrayTail X ↔ ∀ (n : ℕ), m ≤ arrayTailFamily X n

      Universal property of the array tail σ-algebra.

      source
      @[simp]
      theorem TauCeti.Probability.measurableSet_arrayTail_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} {s : Set Ω} :
      MeasurableSet s ↔ ∀ (n : ℕ), MeasurableSet s

      An event belongs to the array tail exactly when it belongs to every member of the tail family.

      source
      theorem TauCeti.Probability.arrayTailFamily_le_ambient {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} [MeasurableSpace Ω] (n : ℕ) (hX : ∀ (p : ℕ × ℕ), n ≤ p.1 → n ≤ p.2 → Measurable (X p)) :
      arrayTailFamily X n ≤ inferInstance

      A member of the tail family is a sub-σ-algebra of the ambient one when the entries it sees are measurable.

      source
      theorem TauCeti.Probability.arrayTail_le_ambient {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ × ℕ → Ω → α} [MeasurableSpace Ω] (n : ℕ) (hX : ∀ (p : ℕ × ℕ), n ≤ p.1 → n ≤ p.2 → Measurable (X p)) :
      arrayTail X ≤ inferInstance

      The tail σ-algebra is a sub-σ-algebra of the ambient one when the entries beyond some cutoff are measurable.

      source
      theorem TauCeti.Probability.blockSigma_arrayDiag_le_blockSigma_prod_self {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) (S : Set ℕ) :
      blockSigma (arrayDiag X) S ≤ blockSigma X (S ×ˢ S)

      The diagonal entries indexed by S are read by the square block over S. The entry arrayDiag X i is X (i, i), and (i, i) lies in S ×ˢ S for every i ∈ S.

      source
      theorem TauCeti.Probability.tailProcess_arrayDiag_le_arrayTail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ × ℕ → Ω → α) :
      tailProcess (arrayDiag X) ≤ arrayTail X

      The tail of the diagonal is an array tail event. The diagonal entries from time n on have both indices at least n, so they generate a sub-σ-algebra of the tail family at n. The inclusion need not be an equality: the array tail may additionally read off-diagonal entries above the cutoff.