Mixtures of Markov chains

A process X : ℕ → Ω → α on a countable state space is a mixture of Markov chains when its finite-path μ-masses are integrals of Markov-chain path masses against μ: there is a measurable initial-law witness ν : Ω → ProbabilityMeasure α and a measurable transition-matrix witness κ : Ω → α → ProbabilityMeasure α with

prefixLaw μ X (n + 1) {w} = ∫⁻ ω, ν ω {w 0} * ∏ i, κ ω (w i.castSucc) {w i.succ} ∂μ

for every finite path w. MixedMarkovChainWith μ X ν κ names the pair of witnesses, and MixedMarkovChain μ X is the existential wrapper. The naming and the witness/existential split follow MixedIIDWith / MixedIID. This notion contains mixed i.i.d. processes: an i.i.d. mixture is the mixture of Markov chains whose rows do not depend on the current state (MixedIIDWith.mixedMarkovChainWith).

⚠ Like MixedIIDWith, this is a property of the unconditional finite path laws only. It says nothing about the joint law of (ν, κ, X), so it is not a conditional-independence statement, and the witnesses are not asserted to be unique. The conditional strengthening — conditionally on (ν, κ) the process is a Markov chain with that initial law and that transition matrix — is the analogue of ConditionallyIIDWith and is deliberately not what is defined here.

This is the class in the conclusion of the Diaconis–Freedman representation theorem: a recurrent Markov exchangeable process is a mixture of Markov chains. This file supplies the class together with the easy direction of that theorem, MixedMarkovChainWith.markovExchangeable: every mixture of Markov chains is Markov exchangeable. The mechanism is the one that makes the initial state together with the transition counts sufficient for a Markov-chain path mass — the transition-product factor depends on the path only through its transition counts (TauCeti.prod_eq_of_transitionCount_eq) — applied inside the mixing integral, where it holds pointwise in the mixing variable.

The class is strictly larger than the mixed i.i.d. one: the deterministic 3-cycle of TauCeti/Probability/Exchangeability/ThreeCycle.lean is a Markov chain, hence a mixture of Markov chains (threeCycle_mixedMarkovChain), but is not exchangeable and so not mixed i.i.d.

The class is also closed under gluing along a countable partition (mixedMarkovChainWith_of_forall_cond): if the process is a mixture of Markov chains under each conditional measure μ[|f ⁻¹' {b}] on a fibre of positive mass of a random variable f with countably many values, then it is one under μ, with the witnesses on the fibre of ω read off at ω. This follows from the law of total probability over the fibres (ProbabilityTheory.sum_meas_smul_cond_fiber_of_countable), since a fibre of mass zero contributes nothing to the finite path masses. The case f = X 0 is what takes the Diaconis–Freedman representation from a process starting at a fixed state to one with a random initial state: the conditional representations at the individual initial states glue to a single pair of witnesses.

Main definitions

• TauCeti.Probability.MixedMarkovChainWith: the mixture identity with named witnesses.
• TauCeti.Probability.MixedMarkovChain: its existential wrapper.

Main results

• TauCeti.Probability.MixedMarkovChainWith.prefixLaw_singleton_eq_lintegral_prod_pow: the initial state and transition counts of a path are sufficient for its μ-mass.
• TauCeti.Probability.MixedMarkovChainWith.markovExchangeable: a mixture of Markov chains is Markov exchangeable — the easy direction of Diaconis–Freedman.
• TauCeti.Probability.mixedMarkovChainWith_const_of_prefixLaw_singleton_eq: a single Markov chain is the degenerate mixture.
• TauCeti.Probability.MixedIIDWith.mixedMarkovChainWith: a mixed i.i.d. process is a mixture of Markov chains with state-independent rows.
• TauCeti.Probability.mixedMarkovChainWith_of_forall_cond and TauCeti.Probability.mixedMarkovChain_of_forall_cond: a process that is a mixture of Markov chains conditionally on each positive-mass value of a countably-valued random variable is a mixture of Markov chains.
• TauCeti.Probability.markovChainLaw_mixedMarkovChainWith: the homogeneous Markov chain of an initial law and a transition kernel is the degenerate mixture with those constant witnesses, and TauCeti.Probability.markovChainLaw_markovExchangeable is its Markov exchangeability. These make the two classes non-vacuous at an arbitrary transition kernel, rather than only at the hypothesis that some product form of the finite path laws holds.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.
• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 8, "Markov exchangeability".

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

def TauCeti.Probability.MixedMarkovChainWith {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (ν : Ω → MeasureTheory.ProbabilityMeasure α) (κ : Ω → α → MeasureTheory.ProbabilityMeasure α) : Prop

A mixture of Markov chains with specified mixing witnesses ν and κ: the μ-mass of a finite path is the integral against μ of its Markov-chain path mass built from ν ω and κ ω. The countability and measurable-singleton conjuncts restrict this singleton-mass formulation to discrete state spaces, matching MarkovExchangeable, where it is non-vacuous and determines the finite path laws. Bundled alongside, as in MarkovExchangeable, are the regularity conjuncts the mixture identity is stated against: the process is coordinatewise a.e. measurable, and both witnesses are measurable (ν, and each row ω ↦ κ ω a).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Probability.MixedMarkovChainWith.intro {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (hν : Measurable ν) (hκ : ∀ (a : α), Measurable fun (ω : Ω) => κ ω a) (h : ∀ (n : ℕ) (w : Fin (n + 1) → α), (prefixLaw μ X (n + 1)) {w} = ∫⁻ (ω : Ω), ↑(ν ω) {w 0} * ∏ i : Fin n, ↑(κ ω (w i.castSucc)) {w i.succ} ∂μ) : MixedMarkovChainWith μ X ν κ

Constructor from discrete-state instances, coordinatewise a.e. measurability, measurability of the two witnesses, and the mixture identity for finite paths.

theorem TauCeti.Probability.MixedMarkovChainWith.countable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) : Countable α

The state space of a mixture of Markov chains is countable.

theorem TauCeti.Probability.MixedMarkovChainWith.measurableSingletonClass {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) : MeasurableSingletonClass α

Singletons in the state space of a mixture of Markov chains are measurable.

theorem TauCeti.Probability.MixedMarkovChainWith.aemeasurable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) (i : ℕ) : AEMeasurable (X i) μ

Every coordinate of a mixture of Markov chains is a.e. measurable.

theorem TauCeti.Probability.MixedMarkovChainWith.measurable_initialLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) : Measurable ν

The initial-law witness of a mixture of Markov chains is measurable.

theorem TauCeti.Probability.MixedMarkovChainWith.measurable_transitionMatrix {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) (a : α) : Measurable fun (ω : Ω) => κ ω a

Each row of the transition-matrix witness of a mixture of Markov chains is measurable.

theorem TauCeti.Probability.MixedMarkovChainWith.prefixLaw_singleton_eq_lintegral {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) (n : ℕ) (w : Fin (n + 1) → α) : (prefixLaw μ X (n + 1)) {w} = ∫⁻ (ω : Ω), ↑(ν ω) {w 0} * ∏ i : Fin n, ↑(κ ω (w i.castSucc)) {w i.succ} ∂μ

The defining mixture identity: the μ-mass of a finite path is the integral of its Markov-chain path masses against μ.

@[simp]

theorem TauCeti.Probability.mixedMarkovChainWith_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} : MixedMarkovChainWith μ X ν κ ↔ (∀ (i : ℕ), AEMeasurable (X i) μ) ∧ Measurable ν ∧ (∀ (a : α), Measurable fun (ω : Ω) => κ ω a) ∧ ∀ (n : ℕ) (w : Fin (n + 1) → α), (prefixLaw μ X (n + 1)) {w} = ∫⁻ (ω : Ω), ↑(ν ω) {w 0} * ∏ i : Fin n, ↑(κ ω (w i.castSucc)) {w i.succ} ∂μ

Simp normal form for MixedMarkovChainWith.

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

A mixture of Markov chains: existence of initial-law and transition-matrix witnesses representing the finite path laws by integration against μ.

Equations

• TauCeti.Probability.MixedMarkovChain μ X = ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α) (κ : Ω → α → MeasureTheory.ProbabilityMeasure α), TauCeti.Probability.MixedMarkovChainWith μ X ν κ

theorem TauCeti.Probability.MixedMarkovChain.of_witnesses {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) : MixedMarkovChain μ X

Constructor from a named pair of witnesses.

theorem TauCeti.Probability.MixedMarkovChain.exists_witnesses {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedMarkovChain μ X) : ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α) (κ : Ω → α → MeasureTheory.ProbabilityMeasure α), MixedMarkovChainWith μ X ν κ

A mixture of Markov chains has initial-law and transition-matrix witnesses.

@[simp]

theorem TauCeti.Probability.mixedMarkovChain_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} : MixedMarkovChain μ X ↔ ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α) (κ : Ω → α → MeasureTheory.ProbabilityMeasure α), MixedMarkovChainWith μ X ν κ

Simp normal form for the existential wrapper MixedMarkovChain.

theorem TauCeti.Probability.MixedMarkovChain.countable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedMarkovChain μ X) : Countable α

The state space of a mixture of Markov chains is countable.

theorem TauCeti.Probability.MixedMarkovChain.measurableSingletonClass {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedMarkovChain μ X) : MeasurableSingletonClass α

Singletons in the state space of a mixture of Markov chains are measurable.

theorem TauCeti.Probability.MixedMarkovChain.aemeasurable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedMarkovChain μ X) (i : ℕ) : AEMeasurable (X i) μ

Every coordinate of a mixture of Markov chains is a.e. measurable.

theorem TauCeti.Probability.MixedMarkovChainWith.prefixLaw_singleton_eq_lintegral_prod_pow {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) {n : ℕ} (w : Fin (n + 1) → α) {S : Finset α} (hS : ∀ (i : Fin (n + 1)), w i ∈ S) : (prefixLaw μ X (n + 1)) {w} = ∫⁻ (ω : Ω), ↑(ν ω) {w 0} * ∏ ab ∈ S ×ˢ S, ↑(κ ω ab.1) {ab.2} ^ transitionCount w ab.1 ab.2 ∂μ

The initial state together with the transition counts of a path is sufficient for its μ-mass. Rewriting the mixture identity through TauCeti.prod_transitionCount replaces the transition-product factor by a product of powers indexed by the transition counts; the index set S only has to contain the letters of the path.

theorem TauCeti.Probability.MixedMarkovChainWith.markovExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {κ : Ω → α → MeasureTheory.ProbabilityMeasure α} (h : MixedMarkovChainWith μ X ν κ) : MarkovExchangeable μ X

A mixture of Markov chains is Markov exchangeable. This is the easy direction of the Diaconis–Freedman representation theorem. Two paths with a common start and common transition counts have equal Markov-chain probabilities for every value of the mixing variable, because a product of transition weights depends on the path only through its transition counts; integration against μ preserves the equality.

theorem TauCeti.Probability.MixedMarkovChain.markovExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedMarkovChain μ X) : MarkovExchangeable μ X

A mixture of Markov chains is Markov exchangeable, existential form.

theorem TauCeti.Probability.mixedMarkovChainWith_const_of_prefixLaw_singleton_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (p₀ : MeasureTheory.ProbabilityMeasure α) (p : α → MeasureTheory.ProbabilityMeasure α) (h : ∀ (n : ℕ) (w : Fin (n + 1) → α), (prefixLaw μ X (n + 1)) {w} = ↑p₀ {w 0} * ∏ i : Fin n, ↑(p (w i.castSucc)) {w i.succ}) : MixedMarkovChainWith μ X (fun (x : Ω) => p₀) fun (x : Ω) => p

A Markov chain is the degenerate mixture of Markov chains. The hypothesis is the defining product form of the finite-dimensional laws of a Markov chain with initial law p₀ and transition matrix p; the mixing witnesses are constant.

theorem TauCeti.Probability.MixedIIDWith.mixedMarkovChainWith {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) : MixedMarkovChainWith μ X ν fun (ω : Ω) (x : α) => ν ω

A mixed i.i.d. process is a mixture of Markov chains whose rows do not depend on the current state: drawing the next coordinate from the mixing representative, whatever the present one, reproduces the mixed i.i.d. finite-dimensional laws. Thus this places MixedIID below MixedMarkovChain in the symmetry lattice, refining Exchangeable.markovExchangeable at the level of the representations.

theorem TauCeti.Probability.MixedIID.mixedMarkovChain {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedIID μ X) : MixedMarkovChain μ X

A mixed i.i.d. process is a mixture of Markov chains, existential form.

theorem TauCeti.Probability.markovChainLaw_prefixLaw_singleton {α : Type u_2} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasurableSingletonClass α] (n : ℕ) (w : Fin (n + 1) → α) : (prefixLaw (markovChainLaw ν κ) (fun (i : ℕ) (x : ℕ → α) => x i) (n + 1)) {w} = ν {w 0} * ∏ i : Fin n, (κ (w i.castSucc)) {w i.succ}

The finite path masses of the homogeneous Markov chain of ν and κ, read through prefixLaw for its coordinate process. This is the product form markovExchangeable_of_prefixLaw_singleton_eq and mixedMarkovChainWith_const_of_prefixLaw_singleton_eq ask for, so it is what supplies those two theorems with genuine instances.

theorem TauCeti.Probability.markovChainLaw_markovExchangeable {α : Type u_2} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [Countable α] [MeasurableSingletonClass α] : MarkovExchangeable (markovChainLaw ν κ) fun (i : ℕ) (x : ℕ → α) => x i

A homogeneous Markov chain is Markov exchangeable. Its finite path masses factor as an initial weight times a product of transition weights, and such a product depends on the path only through its first state and its transition counts.

theorem TauCeti.Probability.markovChainLaw_mixedMarkovChainWith {α : Type u_2} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [Countable α] [MeasurableSingletonClass α] : MixedMarkovChainWith (markovChainLaw ν κ) (fun (i : ℕ) (x : ℕ → α) => x i) (fun (x : ℕ → α) => ⟨ν, ⋯⟩) fun (x : ℕ → α) (a : α) => ⟨κ a, ⋯⟩

A homogeneous Markov chain is the degenerate mixture of Markov chains at its own initial law and transition kernel: the two witnesses are the constant ones. This is the source of genuine MixedMarkovChain processes at an arbitrary transition kernel.

theorem TauCeti.Probability.markovChainLaw_mixedMarkovChain {α : Type u_2} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [Countable α] [MeasurableSingletonClass α] : MixedMarkovChain (markovChainLaw ν κ) fun (i : ℕ) (x : ℕ → α) => x i

A homogeneous Markov chain is a mixture of Markov chains, existential form.

theorem TauCeti.Probability.mixedMarkovChainWith_of_forall_cond {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {f : Ω → β} [Countable α] [MeasurableSingletonClass α] [MeasureTheory.IsFiniteMeasure μ] (hf : Measurable f) {ν : β → Ω → MeasureTheory.ProbabilityMeasure α} {κ : β → Ω → α → MeasureTheory.ProbabilityMeasure α} (hν : ∀ (b : β), Measurable (ν b)) (hκ : ∀ (b : β) (a : α), Measurable fun (ω : Ω) => κ b ω a) (h : ∀ (b : β), μ (f ⁻¹' {b}) ≠ 0 → MixedMarkovChainWith μ[|f ⁻¹' {b}] X (ν b) (κ b)) : MixedMarkovChainWith μ X (fun (ω : Ω) => ν (f ω) ω) fun (ω : Ω) => κ (f ω) ω

Gluing mixtures of Markov chains along a countable partition, witness form. If, on every fibre f ⁻¹' {b} of positive mass of a random variable f with countably many values, the process is a mixture of Markov chains under the conditional measure with witnesses ν b and κ b, then it is a mixture of Markov chains under μ itself, with the witnesses read off on the fibre of ω. The witnesses on the null fibres are only required to be measurable.

theorem TauCeti.Probability.mixedMarkovChain_of_forall_cond {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {f : Ω → β} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hf : Measurable f) (h : ∀ (b : β), μ (f ⁻¹' {b}) ≠ 0 → MixedMarkovChain μ[|f ⁻¹' {b}] X) : MixedMarkovChain μ X

Gluing mixtures of Markov chains along a countable partition, existential form. A process that is a mixture of Markov chains conditionally on each positive-mass value of a random variable with countably many values is a mixture of Markov chains. The measure is assumed nonzero, so that at least one fibre carries positive mass.