Finite-dimensional and path laws of a process

For a process X : ℕ → Ω → α on a measure space (Ω, μ), this file defines its laws as measures on finite tuples and on path space ℕ → α, together with the elementary path-space maps used to compare them:

• blockLaw μ X k — the law of the finite selection (X (k 0), …, X (k (m - 1))), for an arbitrary index type;
• prefixLaw μ X n — the law of the first n coordinates;
• pathLaw μ X — the law of the whole path ω ↦ (i ↦ X i ω);
• prefixProj α n, shift α, permReindex π — the prefix projection, the one-sided left shift, and reindexing by a permutation of time;
• prefixSplitEquiv r — the measurable equivalence splitting a path into its length-r prefix and its tail from index r.

The definitions are hypothesis-light; measurability hypotheses enter only in the lemmas that compose Measure.maps (map_prefixProj_pathLaw, map_blockLaw, map_reindex_pathLaw, …). Nothing here mentions a symmetry of the process: the exchangeability predicates built on these laws live in TauCeti.Probability.Exchangeability.Basic.

The laws and path-space maps are adapted from the cameronfreer/exchangeability sources pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, with Tau Ceti API names and hypotheses; prefixSplitEquiv is not taken from those sources.

noncomputable def TauCeti.Probability.blockLaw {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) {m : ℕ} (k : Fin m → ι) : MeasureTheory.Measure (Fin m → α)

The finite-dimensional law of a family along a coordinate selection k.

The index type is arbitrary: nothing about a finite selection needs the indices to be natural numbers, so families over an arbitrary index type can select from it. Sequence-level users get the ι = ℕ case by unification.

Equations

• TauCeti.Probability.blockLaw μ X k = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ

noncomputable def TauCeti.Probability.prefixLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (n : ℕ) : MeasureTheory.Measure (Fin n → α)

The law of the first n coordinates of a process.

Equations

• TauCeti.Probability.prefixLaw μ X n = TauCeti.Probability.blockLaw μ X fun (i : Fin n) => ↑i

noncomputable def TauCeti.Probability.pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : MeasureTheory.Measure (ℕ → α)

The law of the whole process as a measure on path space.

Equations

• TauCeti.Probability.pathLaw μ X = MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X i ω) μ

def TauCeti.Probability.prefixProj (α : Type u_5) (n : ℕ) (x : ℕ → α) : Fin n → α

Projection from path space to the first n coordinates.

Equations

• TauCeti.Probability.prefixProj α n x i = x ↑i

def TauCeti.Probability.shift (α : Type u_5) (x : ℕ → α) : ℕ → α

The left shift on one-sided path space.

Equations

• TauCeti.Probability.shift α x n = x (n + 1)

def TauCeti.Probability.permReindex {α : Type u_2} (π : Equiv.Perm ℕ) (x : ℕ → α) : ℕ → α

Reindex a one-sided path by a permutation of time.

Equations

• TauCeti.Probability.permReindex π x n = x (π n)

@[simp]

theorem TauCeti.Probability.blockLaw_def {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) {m : ℕ} (k : Fin m → ι) : blockLaw μ X k = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ

theorem TauCeti.Probability.blockLaw_apply_of_measurable {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) {m : ℕ} (k : Fin m → ι) (hXk : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) {S : Set (Fin m → α)} (hS : MeasurableSet S) : (blockLaw μ X k) S = μ ((fun (ω : Ω) (i : Fin m) => X (k i) ω) ⁻¹' S)

The block law of X along k, evaluated on any measurable set S, is the measure of its coordinate-wise preimage. This is the characteristic evaluation of blockLaw as a pushforward; blockLaw_apply_rectangle is the rectangle specialization.

theorem TauCeti.Probability.blockLaw_apply_rectangle {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) {m : ℕ} (k : Fin m → ι) (hXk : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : (blockLaw μ X k) (Set.univ.pi B) = μ {ω : Ω | ∀ (i : Fin m), X (k i) ω ∈ B i}

The block law of X along k, evaluated on a measurable rectangle Set.univ.pi B, is the measure of the coordinate-wise preimage {ω | ∀ i, X (k i) ω ∈ B i} — the rectangle specialization of blockLaw_apply_of_measurable.

@[simp]

theorem TauCeti.Probability.prefixLaw_def {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (n : ℕ) : prefixLaw μ X n = blockLaw μ X fun (i : Fin n) => ↑i

instance TauCeti.Probability.isFiniteMeasure_blockLaw {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : ι → Ω → α) {m : ℕ} (k : Fin m → ι) : MeasureTheory.IsFiniteMeasure (blockLaw μ X k)

A block law of a family under a finite measure is finite.

instance TauCeti.Probability.isFiniteMeasure_prefixLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (n : ℕ) : MeasureTheory.IsFiniteMeasure (prefixLaw μ X n)

A prefix law of a process under a finite measure is finite.

theorem TauCeti.Probability.prefixLaw_singleton_eq_measure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) {n : ℕ} (w : Fin n → α) : (prefixLaw μ X n) {w} = μ {ω : Ω | ∀ (i : Fin n), X (↑i) ω = w i}

The mass of a finite path, as the measure of the event that the process spells it out: prefixLaw μ X n {w} = μ {ω | ∀ i, X i.val ω = w i}. The singleton specialization of blockLaw_apply_of_measurable along the prefix selection.

@[simp]

theorem TauCeti.Probability.pathLaw_def {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : pathLaw μ X = MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X i ω) μ

theorem TauCeti.Probability.pathLaw_coord {α : Type u_2} [MeasurableSpace α] (ρ : MeasureTheory.Measure (ℕ → α)) : (pathLaw ρ fun (i : ℕ) (x : ℕ → α) => x i) = ρ

The path law of the coordinate process on path space is the law itself.

@[simp]

theorem TauCeti.Probability.prefixProj_apply {α : Type u_2} (n : ℕ) (x : ℕ → α) (i : Fin n) : prefixProj α n x i = x ↑i

@[simp]

theorem TauCeti.Probability.shift_apply {α : Type u_2} (x : ℕ → α) (n : ℕ) : shift α x n = x (n + 1)

@[simp]

theorem TauCeti.Probability.permReindex_apply {α : Type u_2} (π : Equiv.Perm ℕ) (x : ℕ → α) (n : ℕ) : permReindex π x n = x (π n)

@[simp]

theorem TauCeti.Probability.permReindex_permReindex {α : Type u_2} (π σ : Equiv.Perm ℕ) (x : ℕ → α) : permReindex π (permReindex σ x) = permReindex (σ * π) x

Composing permReindex π after permReindex σ reindexes by σ * π.

theorem TauCeti.Probability.measurable_prefixProj {α : Type u_2} [MeasurableSpace α] (n : ℕ) : Measurable (prefixProj α n)

The prefix projection is measurable.

theorem TauCeti.Probability.measurable_shift {α : Type u_2} [MeasurableSpace α] : Measurable (shift α)

The one-sided path-space shift is measurable.

def TauCeti.Probability.prefixSplitEquiv {α : Type u_2} [MeasurableSpace α] (r : ℕ) : (ℕ → α) ≃ᵐ (Fin r → α) × (ℕ → α)

Split a sequence into its length-r prefix Fin r → α and the tail ℕ → α from index r, as a measurable equivalence. The forward map sends f to (fun i => f i.val, fun j => f (r + j)); its inverse glues a prefix/tail pair back into a sequence, taking coordinates below r from the prefix and the rest (reindexed by · - r) from the tail.

Equations

• TauCeti.Probability.prefixSplitEquiv r = (MeasurableEquiv.arrowCongr' (finSumNatEquiv r).symm (MeasurableEquiv.refl α)).trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin r ⊕ ℕ) => α)

@[simp]

theorem TauCeti.Probability.prefixSplitEquiv_apply {α : Type u_2} [MeasurableSpace α] (r : ℕ) (f : ℕ → α) : (prefixSplitEquiv r) f = (fun (i : Fin r) => f ↑i, fun (j : ℕ) => f (r + j))

Applying prefixSplitEquiv: it reads off the length-r prefix and the tail from index r.

@[simp]

theorem TauCeti.Probability.prefixSplitEquiv_symm_apply {α : Type u_2} [MeasurableSpace α] (r : ℕ) (p : (Fin r → α) × (ℕ → α)) (n : ℕ) : (prefixSplitEquiv r).symm p n = if h : n < r then p.1 ⟨n, h⟩ else p.2 (n - r)

The inverse of prefixSplitEquiv glues a prefix/tail pair into a sequence: coordinates below r come from the prefix p.1, the rest (reindexed by · - r) from the tail p.2.

theorem TauCeti.Probability.map_prefixProj_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : AEMeasurable (fun (ω : Ω) (i : ℕ) => X i ω) μ) (n : ℕ) : MeasureTheory.Measure.map (prefixProj α n) (pathLaw μ X) = prefixLaw μ X n

The prefix law is the pushforward of the path law by prefixProj.

theorem TauCeti.Probability.prefixLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : prefixLaw (pathLaw μ X) (fun (n : ℕ) (x : ℕ → α) => x n) n = prefixLaw μ X n

The prefix laws of a path law are the prefix laws of the process.

theorem TauCeti.Probability.map_blockLaw {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ι → Ω → α} {m : ℕ} (k : Fin m → ι) {f : α → β} [MeasurableSpace β] (hf : Measurable f) (hXk : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) : MeasureTheory.Measure.map (fun (x : Fin m → α) (i : Fin m) => f (x i)) (blockLaw μ X k) = blockLaw μ (fun (n : ι) (ω : Ω) => f (X n ω)) k

A coordinatewise measurable map sends block laws to block laws.

theorem TauCeti.Probability.map_prefixLaw {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} {f : α → β} [MeasurableSpace β] (hf : Measurable f) (n : ℕ) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : MeasureTheory.Measure.map (fun (x : Fin n → α) (i : Fin n) => f (x i)) (prefixLaw μ X n) = prefixLaw μ (fun (n : ℕ) (ω : Ω) => f (X n ω)) n

A coordinatewise measurable map sends prefix laws to prefix laws.

theorem TauCeti.Probability.map_pathLaw {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} {f : α → β} [MeasurableSpace β] (hf : Measurable f) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : MeasureTheory.Measure.map (fun (x : ℕ → α) (i : ℕ) => f (x i)) (pathLaw μ X) = pathLaw μ fun (n : ℕ) (ω : Ω) => f (X n ω)

A coordinatewise measurable map sends path laws to path laws.

theorem TauCeti.Probability.map_blockLaw_reindex {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ι → Ω → α} {n p : ℕ} (k : Fin n → ι) (g : Fin p → Fin n) (hXk : ∀ (j : Fin n), AEMeasurable (X (k j)) μ) : MeasureTheory.Measure.map (fun (x : Fin n → α) (i : Fin p) => x (g i)) (blockLaw μ X k) = blockLaw μ X (k ∘ g)

Push a block law forward along a coordinate reindexing: selecting the coordinates of blockLaw μ X k through g : Fin p → Fin n yields the block law along k ∘ g.

theorem TauCeti.Probability.measurable_reindex {α : Type u_2} [MeasurableSpace α] (φ : ℕ → ℕ) : Measurable fun (x : ℕ → α) (k : ℕ) => x (φ k)

Reindexing the coordinates of path space along φ is measurable.

theorem TauCeti.Probability.map_reindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (φ : ℕ → ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (pathLaw μ X) = pathLaw μ fun (k : ℕ) (ω : Ω) => X (φ k) ω

Reindexing a path law gives the path law of the reindexed process.

theorem TauCeti.Probability.map_reindex_prefixProj_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (φ : ℕ → ℕ) (n : ℕ) : MeasureTheory.Measure.map (prefixProj α n) (MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (pathLaw μ X)) = blockLaw μ X fun (i : Fin n) => φ ↑i

Projecting the φ-reindexed path law onto its first n coordinates gives the law of the block (X (φ 0), …, X (φ (n-1))).

theorem TauCeti.Probability.map_prefixLaw_castLE {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} {m n : ℕ} (hmn : m ≤ n) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : MeasureTheory.Measure.map (fun (x : Fin n → α) (i : Fin m) => x (Fin.castLE hmn i)) (prefixLaw μ X n) = prefixLaw μ X m

Projecting the prefix law on Fin n onto its first m ≤ n coordinates (via Fin.castLE) gives the prefix law on Fin m.