Documentation

TauCeti.Probability.Exchangeability.Recurrence.Excursion

The excursion process of a recurrent Markov exchangeable process #

A recurrent process that starts at a state a₀ returns to it infinitely often, so its path splits into an infinite sequence of excursions away from a₀. This file assembles that sequence into the excursion process excursionProcess X a₀, a process valued in the finite words List α, and proves the theorem the Diaconis–Freedman representation rests on: for a Markov exchangeable process the excursion process is exchangeable (TauCeti.Probability.MarkovExchangeable.exchangeable_excursionProcess). De Finetti's theorem then applies to it, making the excursions conditionally i.i.d. — that step is drawn in Recurrence.Representation, which is where this subtree meets the representation theory, so the excursion mechanics here stay independent of it.

How the two symmetries meet #

Markov exchangeability constrains finite-path events: the mass of a finite path depends only on its initial state and its transition counts. Exchangeability of the excursion process asks instead about events of the excursions. The bridge is that under recurrence these are the same events. Prescribing the first bs.length excursions of a path starting at a₀ says exactly that, over the span loopSteps bs of the loop they spell out, the path is the loop word loopPathAt a₀ bs (TauCeti.eqOn_loopPathAt_iff_excursionPrefix_eq). Reordering the excursions leaves the initial state and the transition counts alone, so TauCeti.Probability.MarkovExchangeable.measure_setOf_loopPathAt_eq_of_perm gives the two loops equal mass, and the finite-dimensional laws of the excursion process are therefore permutation invariant.

Recurrence is what makes the bridge two-way, and it is a genuine hypothesis: the deterministic walk of TauCeti/Probability/Exchangeability/Recurrence/AbsorbedWalk.lean is Markov exchangeable and leaves its initial state for good.

Lists carry the natural length-indexed measurable structure of TauCeti/MeasureTheory/MeasurableSpace/List.lean. Over the countable discrete state space here this structure is discrete, hence standard Borel, so de Finetti's theorem needs no hypothesis beyond the countability Markov exchangeability already carries.

Main definitions #

Main results #

References #

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

The excursion process #

source
noncomputable def TauCeti.Probability.excursionProcess {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (a₀ : α) :
ℕ → Ω → List α

The excursion process of X away from a₀: its k-th value is the finite word the sample path traverses strictly between its k-th and (k + 1)-st visits to a₀.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.excursionProcess_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (a₀ : α) (k : ℕ) (ω : Ω) :
    excursionProcess X a₀ k ω = excursion (fun (n : ℕ) => X n ω) a₀ k

    Measurability #

    source
    theorem TauCeti.Probability.measurable_excursion {α : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] (a₀ : α) (k : ℕ) :
    Measurable fun (x : ℕ → α) => excursion x a₀ k

    An excursion is a measurable function of the path. The two endpoint visit times are measurable and range over a countable set, and on each of their fibres the excursion reads a fixed finite list of coordinates.

    source
    theorem TauCeti.Probability.aemeasurable_excursionProcess {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (a₀ : α) (k : ℕ) :
    AEMeasurable (excursionProcess X a₀ k) μ

    Every excursion of a process with a.e. measurable coordinates is a.e. measurable.

    Excursion events are finite-path events #

    source
    theorem TauCeti.Probability.measure_setOf_excursionPrefix_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a₀ : α} {bs : List (List α)} (hvisit : ∀ᵐ (ω : Ω) ∂μ, ∃ (n : ℕ), X n ω = a₀ ∧ visitCount (fun (n : ℕ) => X n ω) a₀ n = bs.length) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) (havoid : ∀ e ∈ bs, a₀ ∉ e) :
    μ {ω : Ω | excursionPrefix (fun (n : ℕ) => X n ω) a₀ bs.length = bs} = μ {ω : Ω | ∀ i ≤ loopSteps bs, X i ω = loopPathAt a₀ bs i}

    Prescribing the first excursions is a finite-path event. For a process almost surely starting at a₀ and almost surely making a bs.length-th visit to a₀, having bs as its first bs.length excursions is, up to a null set, spelling out the loop word of bs. Only the visit closing the last prescribed excursion is used, so this asks less than returning to a₀ infinitely often, let alone recurrence of the whole process; TauCeti.exists_visitCount_of_infinite supplies the hypothesis from infinitely many returns.

    source
    theorem TauCeti.Probability.MarkovExchangeable.measure_setOf_excursionPrefix_eq_of_perm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a₀ : α} (h : MarkovExchangeable μ X) (hrec : Recurrent μ X) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) {bs bs' : List (List α)} (hperm : bs.Perm bs') :
    μ {ω : Ω | excursionPrefix (fun (n : ℕ) => X n ω) a₀ bs.length = bs} = μ {ω : Ω | excursionPrefix (fun (n : ℕ) => X n ω) a₀ bs'.length = bs'}

    Reordering a list of excursions does not change the probability that a recurrent Markov exchangeable process traverses it. No hypothesis on the list is needed: excursions never visit the base state, so if some entry of bs does, both events are empty.

    Exchangeability of the excursion process #

    source
    theorem TauCeti.Probability.MarkovExchangeable.exchangeable_excursionProcess {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a₀ : α} (h : MarkovExchangeable μ X) (hrec : Recurrent μ X) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) :
    Exchangeable μ (excursionProcess X a₀)

    The excursion process of a recurrent Markov exchangeable process is exchangeable.

    This is the half of the Diaconis–Freedman representation theorem that consumes the recurrence hypothesis. Its finite-dimensional laws are permutation invariant because each of them is the mass of a finite path, and reordering the excursions of a path preserves both its initial state and its transition counts — the sufficient statistic Markov exchangeability sees.