structure MarkovChain (State : Type u_1) : Type u_1

• ι : State
• P : State → PMF State

structure MarkovChain.Path {State : Type u_1} (M : MarkovChain State) : Type u_1

• states : List State
• length_pos : self.states.length ≠ 0
• nonempty : self.states ≠ []
• initial : self.states[0] = M.ι
• property (i : ℕ) (h : i + 1 < self.states.length) : (M.P self.states[i]) self.states[i + 1] ≠ 0

def MarkovChain.instDecidableEqPath.decEq {State✝ : Type u_2} {M✝ : MarkovChain State✝} [DecidableEq State✝] (x✝ x✝¹ : M✝.Path) : Decidable (x✝ = x✝¹)

Equations

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

instance MarkovChain.instDecidableEqPath {State✝ : Type u_2} {M✝ : MarkovChain State✝} [DecidableEq State✝] : DecidableEq M✝.Path

Equations

• MarkovChain.instDecidableEqPath = MarkovChain.instDecidableEqPath.decEq

instance MarkovChain.instInhabitedPath {State : Type u_1} {M : MarkovChain State} : Inhabited M.Path

Equations

• MarkovChain.instInhabitedPath = { default := { states := [M.ι], length_pos := ⋯, initial := ⋯, property := ⋯ } }

@[reducible, inline]

abbrev MarkovChain.Path.length {State : Type u_1} {M : MarkovChain State} (π : M.Path) : ℕ

Equations

• π.length = π.states.length

def MarkovChain.«term‖_‖» : Lean.ParserDescr

Equations

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

@[simp]

theorem MarkovChain.Path.states_length_eq_length {State : Type u_1} {M : MarkovChain State} {π : M.Path} : π.states.length = π.length

@[simp]

theorem MarkovChain.Path.mk_length {State : Type u_1} {M : MarkovChain State} {states : List State} {length_pos : states.length ≠ 0} {nonempty : states ≠ []} {initial : states[0] = M.ι} {property : ∀ (i : ℕ) (h : i + 1 < states.length), (M.P states[i]) states[i + 1] ≠ 0} : { states := states, length_pos := length_pos, initial := initial, property := property }.length = states.length

structure MarkovChain.Path' {State : Type u_1} (M : MarkovChain State) : Type u_1

• states : Stream' State
• initial : self.states 0 = M.ι
• property (i : ℕ) : (M.P (self.states i)) (self.states (i + 1)) ≠ 0

instance MarkovChain.instGetElemPathNatLtLength {State : Type u_1} {M : MarkovChain State} : GetElem M.Path ℕ State fun (π : M.Path) (n : ℕ) => n < π.length

Equations

• MarkovChain.instGetElemPathNatLtLength = { getElem := fun (π : M.Path) (i : ℕ) (h : i < π.length) => π.states[i] }

instance MarkovChain.instGetElemPath'NatEqBoolTrue {State : Type u_1} {M : MarkovChain State} : GetElem M.Path' ℕ State fun (x : M.Path') (x_1 : ℕ) => true = true

Equations

• MarkovChain.instGetElemPath'NatEqBoolTrue = { getElem := fun (π : M.Path') (i : ℕ) (x : true = true) => π.states i }

def MarkovChain.Path.eq_iff {State : Type u_1} {M : MarkovChain State} {a b : M.Path} : a = b ↔ a.states = b.states

Equations

• ⋯ = ⋯

def MarkovChain.Path.ext {State : Type u_1} {M : MarkovChain State} {a b : M.Path} (h₀ : a.length = b.length) (h : ∀ (i : ℕ) (ha : i < a.length) (hb : i < b.length), a.states[i] = b.states[i]) : a = b

Equations

• ⋯ = ⋯

theorem MarkovChain.Path.ext_iff {State : Type u_1} {M : MarkovChain State} {a b : M.Path} : a = b ↔ a.length = b.length ∧ ∀ (i : ℕ) (ha : i < a.length) (hb : i < b.length), a.states[i] = b.states[i]

def MarkovChain.Path'.ext {State : Type u_1} {M : MarkovChain State} {a b : M.Path'} (h : a.states = b.states) : a = b

Equations

• ⋯ = ⋯

theorem MarkovChain.Path'.ext_iff {State : Type u_1} {M : MarkovChain State} {a b : M.Path'} : a = b ↔ a.states = b.states

@[simp]

theorem MarkovChain.Path.mk_getElem {State : Type u_1} {M : MarkovChain State} {states : List State} {length_pos : states.length ≠ 0} {nonempty : states ≠ []} {initial : states[0] = M.ι} {property : ∀ (i : ℕ) (h : i + 1 < states.length), (M.P states[i]) states[i + 1] ≠ 0} (i : ℕ) (hi : i < states.length) : { states := states, length_pos := length_pos, initial := initial, property := property }[i] = states[i]

theorem MarkovChain.Path.length_eq_of_eq {State : Type u_1} {M : MarkovChain State} {a b : M.Path} (h : a = b) : a.length = b.length

noncomputable def MarkovChain.measure {State : Type u_1} [MeasurableSpace State] (M : MarkovChain State) (s : State) : MeasureTheory.Measure State

Equations

• M.measure s = (M.P s).toMeasure

instance MarkovChain.instIsProbabilityMeasureMeasure {State : Type u_1} {M : MarkovChain State} {s : State} [MeasurableSpace State] : MeasureTheory.IsProbabilityMeasure (M.measure s)

def MarkovChain.Path.take {State : Type u_1} {M : MarkovChain State} (π : M.Path) (i : Fin π.length) : M.Path

Equations

• π.take i = { states := List.take (↑i + 1) π.states, length_pos := ⋯, initial := ⋯, property := ⋯ }

def MarkovChain.Path.take_inj {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Function.Injective π.take

Equations

• ⋯ = ⋯

@[simp]

theorem MarkovChain.Path.take_length {State : Type u_1} {M : MarkovChain State} {π : M.Path} (i : Fin π.length) : (π.take i).length = ↑i + 1

def MarkovChain.Path'.take {State : Type u_1} {M : MarkovChain State} (π' : M.Path') (n : ℕ) : M.Path

Equations

• π'.take n = { states := Stream'.take (n + 1) π'.states, length_pos := ⋯, initial := ⋯, property := ⋯ }

@[simp]

theorem MarkovChain.Path'.take_length {State : Type u_1} {M : MarkovChain State} {π : M.Path'} (i : ℕ) : (π.take i).length = i + 1

def MarkovChain.Path.pref {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Finset M.Path

Equations

• π.pref = Finset.map { toFun := π.take, inj' := ⋯ } Finset.univ

@[simp]

theorem MarkovChain.Path.take_mem_pref {State : Type u_1} {M : MarkovChain State} {π : M.Path} {i : ℕ} (hi : i < π.length) : π.take ⟨i, hi⟩ ∈ π.pref

@[simp]

theorem MarkovChain.Path'.take_take {State : Type u_1} {M : MarkovChain State} {j : ℕ} {π : M.Path'} {i : ℕ} (hi : i < (π.take j).length) : (π.take j).take ⟨i, hi⟩ = π.take i

def MarkovChain.Path'.pref {State : Type u_1} {M : MarkovChain State} (π' : M.Path') : Set M.Path

Equations

• π'.pref = Set.range π'.take

def MarkovChain.Path.Cyl {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Set M.Path'

Equations

• π.Cyl = {π' : M.Path' | π ∈ π'.pref}

instance MarkovChain.instMeasurableSpacePath' {State : Type u_1} {M : MarkovChain State} : MeasurableSpace M.Path'

Equations

• MarkovChain.instMeasurableSpacePath' = MeasurableSpace.generateFrom (Set.range MarkovChain.Path.Cyl)

noncomputable def MarkovChain.Path.succs {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Set M.Path

Equations

• π.succs = {π' : M.Path | π'.length = π.length + 1 ∧ List.take π.length π'.states = π.states}

@[simp]

theorem MarkovChain.Path.succs_length {State : Type u_1} {M : MarkovChain State} {π : M.Path} (π' : ↑π.succs) : (↑π').length = π.length + 1

@[simp]

theorem MarkovChain.Path.succs_length' {State : Type u_1} {M : MarkovChain State} {π π' : M.Path} (hπ' : π' ∈ π.succs) : π'.length = π.length + 1

@[simp]

theorem MarkovChain.Path.succs_getElem {State : Type u_1} {M : MarkovChain State} {π : M.Path} (π' : ↑π.succs) (i : ℕ) (h : i < π.length) : (↑π')[i] = π[i]

@[simp]

theorem MarkovChain.Path.succs_states_getElem {State : Type u_1} {M : MarkovChain State} {π : M.Path} (π' : ↑π.succs) (i : ℕ) (h : i < π.length) : (↑π').states[i] = π[i]

@[simp]

theorem MarkovChain.Path.succs_states_getElem' {State : Type u_1} {M : MarkovChain State} {π π' : M.Path} (hπ' : π' ∈ π.succs) (i : ℕ) (h : i < π.length) : π'.states[i] = π[i]

noncomputable def MarkovChain.Path.pmf {State : Type u_1} {M : MarkovChain State} (π : M.Path) : PMF ↑π.succs

NOTE: this is the dependent version of pmf'

Equations

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

noncomputable def MarkovChain.Path.pmf' {State : Type u_1} {M : MarkovChain State} (π : M.Path) : PMF M.Path

Equations

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

theorem MarkovChain.Path.pmf_apply {State : Type u_1} {M : MarkovChain State} {π : M.Path} {π' : ↑π.succs} : π.pmf π' = π.pmf' ↑π'

theorem MarkovChain.Path.pmf'_apply {State : Type u_1} {M : MarkovChain State} [DecidableEq State] {π π' : M.Path} : π.pmf' π' = if h : List.take π.length π'.states = π.states ∧ π'.length = π.length + 1 then (M.P π'.states[π'.length - 2]) π'.states[π'.length - 1] else 0

def MarkovChain.Path.ofLength_countable {State : Type u_1} {M : MarkovChain State} (n : ℕ) : Countable ↑{π : M.Path | π.length = n}

Equations

• ⋯ = ⋯

theorem MarkovChain.Path.complete {State : Type u_1} {M : MarkovChain State} : ⋃ (n : ℕ), {π : M.Path | π.length = n} = Set.univ

instance MarkovChain.instCountablePath {State : Type u_1} {M : MarkovChain State} : Countable M.Path

instance MarkovChain.instMeasurableSpacePath {State : Type u_1} {M : MarkovChain State} : MeasurableSpace M.Path

Equations

• MarkovChain.instMeasurableSpacePath = MeasurableSpace.generateFrom Set.univ

instance MarkovChain.instMeasurableSingletonClassPath {State : Type u_1} {M : MarkovChain State} : MeasurableSingletonClass M.Path

instance MarkovChain.instDiscreteMeasurableSpacePath {State : Type u_1} {M : MarkovChain State} : DiscreteMeasurableSpace M.Path

theorem MarkovChain.Path.pmf_toMeasure_apply {State : Type u_1} {M : MarkovChain State} {π : M.Path} {S : Set ↑π.succs} : π.pmf.toMeasure S = π.pmf'.toMeasure ((fun (x : ↑π.succs) => ↑x) '' S)

@[simp]

theorem MarkovChain.Path.pmf'_toMeasure_apply {State : Type u_1} {M : MarkovChain State} [DecidableEq State] {π : M.Path} {S : Set M.Path} [(π' : M.Path) → Decidable (π' ∈ S)] : π.pmf'.toMeasure S = ∑' (π' : M.Path), if h : List.take π.length π'.states = π.states ∧ π'.length = π.length + 1 then if π' ∈ S then (M.P π'.states[π'.length - 2]) π'.states[π'.length - 1] else 0 else 0

noncomputable def MarkovChain.Path.measure {State : Type u_1} {M : MarkovChain State} (π : M.Path) : MeasureTheory.Measure ↑π.succs

Equations

• π.measure = π.pmf.toMeasure

instance MarkovChain.instIsProbabilityMeasureElemPathSuccsMeasure {State : Type u_1} {M : MarkovChain State} {π : M.Path} : MeasureTheory.IsProbabilityMeasure π.measure

noncomputable def MarkovChain.Path.lifted {State : Type u_1} {M : MarkovChain State} : MeasureTheory.Measure ((π : M.Path) → ↑π.succs)

Equations

• MarkovChain.Path.lifted = MeasureTheory.Measure.infinitePi MarkovChain.Path.measure

instance MarkovChain.instIsProbabilityMeasureForallElemPathSuccsLifted {State : Type u_1} {M : MarkovChain State} : MeasureTheory.IsProbabilityMeasure Path.lifted

noncomputable instance MarkovChain.instInhabitedElemPathSuccs {State : Type u_1} {M : MarkovChain State} {π : M.Path} : Inhabited ↑π.succs

Equations

• MarkovChain.instInhabitedElemPathSuccs = { default := ⟨{ states := π.states ++ [Exists.choose ⋯], length_pos := ⋯, initial := ⋯, property := ⋯ }, ⋯⟩ }

noncomputable def MarkovChain.embed.help {State : Type u_1} {M : MarkovChain State} (f : (π : M.Path) → ↑π.succs) : ℕ → M.Path

Equations

• MarkovChain.embed.help f 0 = default
• MarkovChain.embed.help f n.succ = ↑(f (MarkovChain.embed.help f n))

theorem MarkovChain.embed.help_eq {State : Type u_1} {M : MarkovChain State} {n : ℕ} (f : (π : M.Path) → ↑π.succs) : help f n = (fun (x : M.Path) => ↑(f x))^[n] default

@[simp]

theorem MarkovChain.embed.help_length {State : Type u_1} {M : MarkovChain State} {f : (π : M.Path) → ↑π.succs} {n : ℕ} : (help f n).length = n + 1

@[simp]

theorem MarkovChain.embed.help_getElem {State : Type u_1} {M : MarkovChain State} {n : ℕ} {f : (π : M.Path) → ↑π.succs} (i : ℕ) (h : i < n + 1) : (help f n)[i] = (help f i)[i]

@[simp]

theorem MarkovChain.embed.help_states_getElem {State : Type u_1} {M : MarkovChain State} {n : ℕ} {f : (π : M.Path) → ↑π.succs} (i : ℕ) (h : i < n + 1) : (help f n).states[i] = (help f i).states[i]

noncomputable def MarkovChain.embed {State : Type u_1} {M : MarkovChain State} (f : (π : M.Path) → ↑π.succs) : M.Path'

Equations

• MarkovChain.embed f = { states := fun (n : ℕ) => (MarkovChain.embed.help f n)[n], initial := ⋯, property := ⋯ }

noncomputable def MarkovChain.embedInv {State : Type u_1} {M : MarkovChain State} (π' : M.Path') (π : M.Path) : ↑π.succs

Equations

• MarkovChain.embedInv π' π = if h : π ∈ π'.pref then ⟨π'.take π.length, ⋯⟩ else default

def MarkovChain.Path.theSet {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Set ((i : ↥π.pref) → ↑(↑i).succs)

Equations

• π.theSet = {f : (i : ↥π.pref) → ↑(↑i).succs | ∀ (π' : ↥π.pref), ↑π' ≠ π → ↑(f π') ∈ π.pref}

theorem MarkovChain.Path.theSet_measurable {State : Type u_1} {M : MarkovChain State} (π : M.Path) : MeasurableSet π.theSet

theorem MarkovChain.Path.theSet_eq_pi {State : Type u_1} {M : MarkovChain State} (π : M.Path) : π.theSet = Set.univ.pi fun (π' : ↥π.pref) => {π'' : ↑(↑π').succs | ¬↑π' = π → ↑π'' ∈ π.pref}

theorem MarkovChain.Path.Cyl_subset_cylinder {State : Type u_1} {M : MarkovChain State} (π : M.Path) : embed ⁻¹' π.Cyl ⊆ MeasureTheory.cylinder π.pref π.theSet

theorem MarkovChain.Path.Cyl_eq_cylinder {State : Type u_1} {M : MarkovChain State} (π : M.Path) : embed ⁻¹' π.Cyl = MeasureTheory.cylinder π.pref π.theSet

theorem MarkovChain.embed.measurable {State : Type u_1} {M : MarkovChain State} : Measurable embed

noncomputable def MarkovChain.Pr {State : Type u_1} {M : MarkovChain State} : MeasureTheory.Measure M.Path'

Equations

• MarkovChain.Pr = MeasureTheory.Measure.map MarkovChain.embed MarkovChain.Path.lifted

instance MarkovChain.instIsProbabilityMeasurePath'Pr {State : Type u_1} {M : MarkovChain State} : MeasureTheory.IsProbabilityMeasure Pr

theorem MarkovChain.Path.Cyl_measurable {State : Type u_1} {M : MarkovChain State} (π : M.Path) : MeasurableSet π.Cyl

theorem MarkovChain.Pr_cyl_help {State : Type u_1} {M : MarkovChain State} (π : M.Path) : (∏ x ∈ π.pref.attach, if h : ↑x = π then 1 else (↑x).pmf' (π.take ⟨(↑x).length, ⋯⟩)) = ∏ i : Fin (π.length - 1), (M.P π.states[↑i]) π.states[↑i + 1]

theorem MarkovChain.Pr_cyl {State : Type u_1} {M : MarkovChain State} (π : M.Path) : Pr π.Cyl = ∏ i : Fin (π.length - 1), (M.P π.states[i]) π.states[↑i + 1]