Documentation

TauCeti.Probability.Exchangeability.Recurrence.AbsorbedWalk

A nonrecurrent Markov exchangeable process #

The deterministic path false, true, true, … is a Markov chain and hence Markov exchangeable, but it visits false only once. Thus recurrence is a genuine additional hypothesis in the Diaconis–Freedman representation theorem.

References #

source
def TauCeti.Probability.absorbedWalk :
ℕ → Unit → Bool

The deterministic path false, true, true, …, on the one-point sample space. It is the Markov chain that leaves false at time 1 and is then absorbed at true.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.absorbedWalk_apply (n : ℕ) (u : Unit) :
    absorbedWalk n u = decide (n ≠ 0)
    source
    theorem TauCeti.Probability.absorbedWalk_prefixLaw_singleton (n : ℕ) (w : Fin (n + 1) → Bool) :
    (prefixLaw (MeasureTheory.Measure.dirac ()) absorbedWalk (n + 1)) {w} = (if w 0 = false then 1 else 0) * ∏ i : Fin n, if w i.succ = true then 1 else 0

    The absorbed walk has the finite-dimensional laws of a Markov chain. A path of length n + 1 is possible only if it starts at false and is true from time 1 on.

    source
    theorem TauCeti.Probability.absorbedWalk_markovExchangeable :
    MarkovExchangeable (MeasureTheory.Measure.dirac ()) absorbedWalk

    The absorbed walk is Markov exchangeable, being a Markov chain.

    source
    theorem TauCeti.Probability.not_recurrent_absorbedWalk :
    ¬Recurrent (MeasureTheory.Measure.dirac ()) absorbedWalk

    The absorbed walk is not recurrent: it visits false only at time 0. Together with absorbedWalk_markovExchangeable this shows that recurrence is a genuine extra hypothesis on a Markov exchangeable process, in contrast with Exchangeable.recurrent.