Documentation

TauCeti.Probability.Process.SuccessorArray

Successor arrays of paths and processes #

The combinatorial successor-array encoding and its inverse are defined in TauCeti.Combinatorics.Enumerative.SuccessorArray. This file relates that encoding to transition counts and proves that both directions of the change of variables are measurable.

Why this is the Diaconis–Freedman decomposition #

Markov exchangeability (TauCeti.Probability.MarkovExchangeable) says that the law of a finite path depends only on its initial state and transition counts. The successor array is the change of variables that reads those counts as occurrence counts in initial segments of its rows. Its measurability transfers representations of the joint law of (x 0, successorArray x) back to the law of the path.

Main definitions #

Main results #

References #

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

source
theorem TauCeti.Probability.visitCount_eq_occCount_prefixProj {α : Type u_1} (x : ℕ → α) (a : α) (n : ℕ) :
visitCount x a n = Function.occCount (prefixProj α n x) a

A visit count is the occurrence count of the corresponding finite prefix.

source
theorem TauCeti.Probability.transitionCount_prefixProj {α : Type u_1} (x : ℕ → α) (n : ℕ) (a b : α) :
transitionCount (prefixProj α (n + 1) x) a b = visitCount (successorArray x a) b (visitCount x a n)

The transition counts of a path are visit counts in its successor rows. The number of a-to-b transitions before time n is the number of occurrences of b among the successors of the visits to a before n. This is the form used by the later row-exchangeability argument.

source
theorem TauCeti.Probability.measurable_visitCount_comp {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {P : β → ℕ → α} (a : α) (n : ℕ) (ha : MeasurableSet {a}) (hP : ∀ i < n, Measurable fun (b : β) => P b i) :
Measurable fun (b : β) => visitCount (P b) a n

Visit counts of a measurably varying sequence are measurable when the relevant coordinates are measurable.

source
theorem TauCeti.Probability.measurable_visitCount {α : Type u_1} [MeasurableSpace α] (a : α) (n : ℕ) (ha : MeasurableSet {a}) :
Measurable fun (x : ℕ → α) => visitCount x a n

Visit counts are measurable functions of a path.

source
theorem TauCeti.Probability.measurable_visitTime {α : Type u_1} [MeasurableSpace α] (a : α) (k : ℕ) (ha : MeasurableSet {a}) :
Measurable fun (x : ℕ → α) => visitTime x a k

Visit times are measurable functions of the path. Each fibre is described by visitTime_eq_iff as a countable Boolean combination of coordinate events.

source
theorem TauCeti.Probability.measurable_successorArray_apply {α : Type u_1} [MeasurableSpace α] (a : α) (k : ℕ) (ha : MeasurableSet {a}) :
Measurable fun (x : ℕ → α) => successorArray x a k

Each entry of the successor array is a measurable function of the path.

source
theorem TauCeti.Probability.measurable_visitedSuccessorArray_apply {α : Type u_1} [MeasurableSpace α] (a : α) (k : ℕ) (ha : MeasurableSet {a}) :
Measurable fun (x : ℕ → α) => visitedSuccessorArray x a k

Each entry of the visited successor array is a measurable function of the path: whether the path visits the row is a countable union of coordinate events.

source
theorem TauCeti.Probability.measurable_successorArray {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
Measurable fun (x : ℕ → α) => successorArray x

The successor array of a path is a measurable function of the path.

source
theorem TauCeti.Probability.measurable_visitedSuccessorArray {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
Measurable fun (x : ℕ → α) => visitedSuccessorArray x

The visited successor array of a path is a measurable function of the path.

source
noncomputable def TauCeti.Probability.successorProcess {α : Type u_1} {Ω : Type u_2} (X : ℕ → Ω → α) :
α × ℕ → Ω → α

The successor array of a process, as an array indexed by state and visit number: the (a, k)-entry is the value the process takes right after its k-th visit to a.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.successorProcess_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ → Ω → α) (p : α × ℕ) (ω : Ω) :
    successorProcess X p ω = successorArray (fun (n : ℕ) => X n ω) p.1 p.2
    source
    theorem TauCeti.Probability.aemeasurable_successorProcess {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (p : α × ℕ) :
    AEMeasurable (successorProcess X p) μ

    Every entry of the successor array of an almost everywhere measurable process is almost everywhere measurable.

    source
    noncomputable def TauCeti.Probability.visitedSuccessorProcess {α : Type u_1} {Ω : Type u_2} (X : ℕ → Ω → α) :
    α × ℕ → Ω → α

    The visited successor array of a process, as an array indexed by state and visit number. Genuine visit indices record the value following the visit. Other indices in a visited row retain the totalized junk behavior of TauCeti.successorArray, while a wholly unvisited row is constant at its index a.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Probability.visitedSuccessorProcess_apply {α : Type u_1} {Ω : Type u_2} (X : ℕ → Ω → α) (p : α × ℕ) (ω : Ω) :
      visitedSuccessorProcess X p ω = visitedSuccessorArray (fun (n : ℕ) => X n ω) p.1 p.2
      source
      theorem TauCeti.Probability.visitedSuccessorProcess_visitCell {α : Type u_1} {Ω : Type u_2} (X : ℕ → Ω → α) (n : ℕ) (ω : Ω) :
      visitedSuccessorProcess X (visitCell (fun (j : ℕ) => X j ω) n) ω = X (n + 1) ω

      At every cell consumed by a sample path, its visited successor process records the next value.

      source
      theorem TauCeti.Probability.aemeasurable_visitedSuccessorProcess {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (p : α × ℕ) :
      AEMeasurable (visitedSuccessorProcess X p) μ

      Every entry of the visited successor array of an almost everywhere measurable process is almost everywhere measurable.

      source
      theorem TauCeti.Probability.measurable_apply_zero_prodMk_successorArray {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :
      Measurable fun (x : ℕ → α) => (x 0, successorArray x)

      The map pairing a path's initial state with its successor array is measurable.

      source
      theorem TauCeti.Probability.measurable_pathOfSuccessors {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] :
      Measurable fun (q : α × (α → ℕ → α)) => pathOfSuccessors q.1 q.2

      Rebuilding a path from an initial state and a successor array is measurable.

      source
      theorem TauCeti.Probability.map_pathOfSuccessors_map_apply_zero_prodMk_successorArray {α : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] (ρ : MeasureTheory.Measure (ℕ → α)) :
      MeasureTheory.Measure.map (fun (q : α × (α → ℕ → α)) => pathOfSuccessors q.1 q.2) (MeasureTheory.Measure.map (fun (x : ℕ → α) => (x 0, successorArray x)) ρ) = ρ

      Every law on path space is the image of the joint law of the initial state and the successor array. This is the change of variables behind the Diaconis–Freedman representation theorem: a description of the law of (x 0, successorArray x) determines the law of the path.

      source
      theorem TauCeti.Probability.pathLaw_eq_map_pathOfSuccessors {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) :
      pathLaw μ X = MeasureTheory.Measure.map (fun (q : α × (α → ℕ → α)) => pathOfSuccessors q.1 q.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X 0 ω, successorArray fun (n : ℕ) => X n ω)) μ)

      The path law of a process is the image of the joint law of its initial state and its successor array.