structure MDPs.MDP (σ α : Type) : Type

Markov decision process

• S : Finset σ

  states

• S_ne : self.S.Nonempty
• A : Finset α

  actions

• A_ne : self.A.Nonempty
• P : σ → α → Δ self.S

  transition probability s, a, s'

• r : σ → α → σ → ℝ

  reward function s, a, s'

inductive MDPs.Hist {σ α : Type} (M : MDPs.MDP σ α) : Type

Represents a history. The state is type σ and action is type α.

• init {σ α : Type} {M : MDPs.MDP σ α} : σ → MDPs.Hist M
• foll {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → α → σ → MDPs.Hist M

instance MDPs.instCoeHist {σ α : Type} {M : MDPs.MDP σ α} : Coe σ (MDPs.Hist M)

Coerces a state to a history

Equations

• MDPs.instCoeHist = { coe := fun (s : σ) => MDPs.Hist.init s }

@[reducible]

def MDPs.Hist.length {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → ℕ

The length of the history corresponds to the zero-based step of the decision

Equations

• (MDPs.Hist.init a).length = 0
• (h.foll a a_1).length = 1 + h.length

@[reducible, inline]

abbrev MDPs.HistNE {σ α : Type} (m : MDPs.MDP σ α) : Type

Nonempty histories

Equations

• MDPs.HistNE m = { h : MDPs.Hist m // h.length ≥ 1 }

def MDPs.Hist.last {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → σ

Returns the last state of the history

Equations

• (MDPs.Hist.init a).last = a
• (h.foll a a_1).last = a_1

def MDPs.Hist.append {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (as : α × σ) : MDPs.Hist M

Appends the state and action to the history -

Equations

• h.append as = h.foll as.1 as.2

def MDPs.Hist.one {σ α : Type} {M : MDPs.MDP σ α} (s₀ : σ) (a : α) (s : σ) : MDPs.Hist M

Equations

• MDPs.Hist.one s₀ a s = (MDPs.Hist.init s₀).foll a s

def MDPs.Hist.prefix {σ α : Type} {M : MDPs.MDP σ α} (k : ℕ) (h : MDPs.Hist M) : MDPs.Hist M

Return the prefix of hist of length k

Equations

• MDPs.Hist.prefix k (MDPs.Hist.init a) = MDPs.Hist.init a
• MDPs.Hist.prefix k (h_1.foll a a_1) = if h_1.length + 1 ≤ k then h_1.foll a a_1 else MDPs.Hist.prefix k h_1

def MDPs.tuple2hist {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M × α × σ → MDPs.HistNE M

Equations

• MDPs.tuple2hist (h, as) = ⟨h.append as, ⋯⟩

def MDPs.hist2tuple {σ α : Type} {M : MDPs.MDP σ α} : MDPs.HistNE M → MDPs.Hist M × α × σ

Equations

• MDPs.hist2tuple ⟨h.foll a s, property⟩ = (h, a, s)

theorem MDPs.linv_hist2tuple_tuple2hist {σ α : Type} {M : MDPs.MDP σ α} : Function.LeftInverse MDPs.hist2tuple MDPs.tuple2hist

theorem MDPs.inj_tuple2hist_l1 {σ α : Type} {M : MDPs.MDP σ α} : Function.Injective MDPs.tuple2hist

theorem MDPs.inj_tuple2hist {σ α : Type} {M : MDPs.MDP σ α} : Function.Injective (Subtype.val ∘ MDPs.tuple2hist)

def MDPs.emb_tuple2hist_l1 {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M × α × σ ↪ MDPs.HistNE M

Equations

• MDPs.emb_tuple2hist_l1 = { toFun := MDPs.tuple2hist, inj' := ⋯ }

def MDPs.emb_tuple2hist {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M × α × σ ↪ MDPs.Hist M

Equations

• MDPs.emb_tuple2hist = { toFun := fun (x : MDPs.Hist M × α × σ) => ↑(MDPs.tuple2hist x), inj' := ⋯ }

def MDPs.state2hist {σ α : Type} {M : MDPs.MDP σ α} (s : σ) : MDPs.Hist M

Equations

• MDPs.state2hist s = MDPs.Hist.init s

def MDPs.hist2state {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → σ

Equations

• MDPs.hist2state (MDPs.Hist.init a) = a
• MDPs.hist2state (h.foll a a_1) = a_1

theorem MDPs.linv_hist2state_state2hist {σ α : Type} {M : MDPs.MDP σ α} : Function.LeftInverse MDPs.hist2state MDPs.state2hist

theorem MDPs.inj_state2hist {σ α : Type} {M : MDPs.MDP σ α} : Function.Injective MDPs.state2hist

def MDPs.state2hist_emb {σ α : Type} {M : MDPs.MDP σ α} : σ ↪ MDPs.Hist M

Equations

• MDPs.state2hist_emb = { toFun := MDPs.state2hist, inj' := ⋯ }

def MDPs.isprefix {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → MDPs.Hist M → Prop

Checks if the first hist is the prefix of the second hist.

Equations

• One or more equations did not get rendered due to their size.
• MDPs.isprefix (MDPs.Hist.init s₁) (MDPs.Hist.init s₂) = (s₁ = s₂)
• MDPs.isprefix (MDPs.Hist.init s₁) (hp.foll a a_1) = MDPs.isprefix (MDPs.Hist.init s₁) hp
• MDPs.isprefix (a.foll a_1 a_2) (MDPs.Hist.init a_3) = False

def MDPs.Histories {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) : ℕ → Finset (MDPs.Hist M)

All histories of additional length t that follow history h

Equations

• MDPs.Histories h Nat.zero = {h}
• MDPs.Histories h t.succ = Finset.map MDPs.emb_tuple2hist (MDPs.Histories h t ×ˢ M.A ×ˢ M.S)

@[reducible, inline]

abbrev MDPs.ℋ {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → ℕ → Finset (MDPs.Hist M)

Equations

• MDPs.ℋ = MDPs.Histories

theorem MDPs.hist_lenth_eq_horizon {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (t : ℕ) (h' : MDPs.Hist M) : h' ∈ MDPs.ℋ h t → h'.length = h.length + t

def MDPs.HistoriesHorizon {σ α : Type} {M : MDPs.MDP σ α} : ℕ → Finset (MDPs.Hist M)

All histories of a given length

Equations

• MDPs.HistoriesHorizon Nat.zero = Finset.map MDPs.state2hist_emb M.S
• MDPs.HistoriesHorizon t.succ = Finset.map MDPs.emb_tuple2hist (MDPs.HistoriesHorizon t ×ˢ M.A ×ˢ M.S)

@[reducible, inline]

abbrev MDPs.ℋₜ {σ α : Type} {M : MDPs.MDP σ α} : ℕ → Finset (MDPs.Hist M)

Equations

• MDPs.ℋₜ = MDPs.HistoriesHorizon

def MDPs.PolicyHR {σ α : Type} (M : MDPs.MDP σ α) : Type

A randomized history-dependent policy

Equations

• MDPs.PolicyHR M = (MDPs.Hist M → Δ M.A)

instance MDPs.instCoeSubtypeMemFinsetAPolicyHROfDecidableEq {σ α : Type} {M : MDPs.MDP σ α} [DecidableEq α] : Coe { x : α // x ∈ M.A } (MDPs.PolicyHR M)

Equations

• MDPs.instCoeSubtypeMemFinsetAPolicyHROfDecidableEq = { coe := fun (a : { x : α // x ∈ M.A }) (x : MDPs.Hist M) => Finprob.dirac_dist M.A a }

def MDPs.DecisionRule {σ α : Type} (M : MDPs.MDP σ α) : Type

Decision rule

Equations

• MDPs.DecisionRule M = (σ → { x : α // x ∈ M.A })

instance MDPs.instCoeSubtypeMemFinsetADecisionRuleOfDecidableEq {σ α : Type} {M : MDPs.MDP σ α} [DecidableEq α] : Coe { x : α // x ∈ M.A } (MDPs.DecisionRule M)

Equations

• MDPs.instCoeSubtypeMemFinsetADecisionRuleOfDecidableEq = { coe := fun (a : { x : α // x ∈ M.A }) (x : σ) => a }

def MDPs.PolicySD {σ α : Type} (M : MDPs.MDP σ α) : Type

A deterministic stationary policy

Equations

• MDPs.PolicySD M = MDPs.DecisionRule M

instance MDPs.instCoePolicySDPolicyHROfDecidableEq {σ α : Type} {M : MDPs.MDP σ α} [DecidableEq α] : Coe (MDPs.PolicySD M) (MDPs.PolicyHR M)

Equations

• MDPs.instCoePolicySDPolicyHROfDecidableEq = { coe := fun (d : MDPs.PolicySD M) (h : MDPs.Hist M) => Finprob.dirac_dist M.A (d h.last) }

def MDPs.HistDist {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) : Δ (MDPs.ℋ h T)

Probability distribution over histories induced by the policy and transition probabilities

Equations

• One or more equations did not get rendered due to their size.
• MDPs.HistDist h π Nat.zero = Finprob.dirac_ofsingleton h

@[reducible, inline]

abbrev MDPs.Δℋ {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) : Finprob (MDPs.Hist M)

Equations

• MDPs.Δℋ h π T = { Ω := MDPs.ℋ h T, prob := MDPs.HistDist h π T }

def MDPs.reward {σ α : Type} {M : MDPs.MDP σ α} : MDPs.Hist M → ℝ

Reward of a history

Equations

• MDPs.reward (MDPs.Hist.init a) = 0
• MDPs.reward (h.foll a a_1) = M.r h.last a a_1 + MDPs.reward h

def MDPs.reward_at {σ α : Type} {M : MDPs.MDP σ α} (i : ℕ) : MDPs.Hist M → ℝ

Reward at a specific position; 0-based

Equations

• MDPs.reward_at i (MDPs.Hist.init a) = 0
• MDPs.reward_at i (h.foll a a_1) = if h.length = i then M.r h.last a a_1 else MDPs.reward_at i h

def MDPs.reward_to {σ α : Type} {M : MDPs.MDP σ α} (j : ℕ) : MDPs.Hist M → ℝ

Sum of rewards from a specific position to the end

Equations

• MDPs.reward_to j (MDPs.Hist.init a) = 0
• MDPs.reward_to j (h.foll a a_1) = if h.length ≤ j then M.r h.last a a_1 + MDPs.reward h else MDPs.reward_to j h

def MDPs.reward_from {σ α : Type} {M : MDPs.MDP σ α} (j : ℕ) : MDPs.Hist M → ℝ

Sum of rewards from a specific position to the end

Equations

• MDPs.reward_from j (MDPs.Hist.init a) = 0
• MDPs.reward_from j (h.foll a a_1) = if h.length ≥ j then M.r h.last a a_1 + MDPs.reward_from j h else 0

def MDPs.prob_h {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) (h' : { x : MDPs.Hist M // x ∈ MDPs.ℋ h T }) : NNReal

The probability of a history

Equations

• MDPs.prob_h h π T h' = (MDPs.Δℋ h π T).prob.p ↑h'

def MDPs.probability_h {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) (B : MDPs.Hist M → Bool) : NNReal

Probability of a boolean event

Equations

• MDPs.probability_h h π T B = ℙ[{ val := B }]

def MDPs.«termℙₕ[_//_,_,_]» : Lean.ParserDescr

Equations

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

def MDPs.expect_h {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) (X : MDPs.Hist M → ℝ) : ℝ

Expectation over histories for a r.v. X for horizon T and policy π

Equations

• MDPs.expect_h h π T X = 𝔼[{ val := X }]

def MDPs.«term𝔼ₕ[_//_,_,_]» : Lean.ParserDescr

Equations

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

noncomputable def MDPs.expect_h_cnd {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) (X : MDPs.Hist M → ℝ) (B : MDPs.Hist M → Bool) : ℝ

Condtional expectation over histories for a r.v. X for horizon T and policy π

Equations

• MDPs.expect_h_cnd h π T X B = 𝔼[{ val := X }|{ val := B }]

def MDPs.«term𝔼ₕ[_|_//_,_,_]» : Lean.ParserDescr

Equations

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

noncomputable def MDPs.expect_h_cnd_rv {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) (π : MDPs.PolicyHR M) (T : ℕ) (X : MDPs.Hist M → ℝ) {ν : Type} [DecidableEq ν] (Y : MDPs.Hist M → ν) : MDPs.Hist M → ℝ

Equations

• MDPs.expect_h_cnd_rv h π T X Y = fun (h_1 : MDPs.Hist M) => 𝔼[{ val := X }|{ val := Y } ᵣ== Y h_1]

def MDPs.«term𝔼ₕ[_|ᵥ_//_,_,_]» : Lean.ParserDescr

Equations

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

def MDPs.state {σ α : Type} {M : MDPs.MDP σ α} (k : ℕ) (h : MDPs.Hist M) : σ

The k-th state of a history. The initial state is state 0.

Equations

• MDPs.state k (MDPs.Hist.init a) = a
• MDPs.state k (h_1.foll a a_1) = if (h_1.foll a a_1).length = k then a_1 else MDPs.state k h_1

def MDPs.action {σ α : Type} {M : MDPs.MDP σ α} [Inhabited α] (k : ℕ) (h : MDPs.Hist M) : α

The k-th action of a history. The first action is action 0.

Equations

• MDPs.action k (MDPs.Hist.init a) = default
• MDPs.action k (h_1.foll a a_1) = if (h_1.foll a a_1).length = k then a else MDPs.action k h_1

def MDPs.Histrv {σ α : Type} (M : MDPs.MDP σ α) : Type

Random variable on histories sans distribution (policy dependent)

Equations

• MDPs.Histrv M = (MDPs.Hist M → ℝ)

instance MDPs.instCoeRtoRV {σ α : Type} {M : MDPs.MDP σ α} : Coe ℝ (MDPs.Histrv M)

Equations

• MDPs.instCoeRtoRV = { coe := fun (c : ℝ) (x : MDPs.Hist M) => c }

instance MDPs.instHAddHRV {σ α : Type} {M : MDPs.MDP σ α} : HAdd (MDPs.Histrv M) (MDPs.Histrv M) (MDPs.Histrv M)

Equations

• MDPs.instHAddHRV = { hAdd := fun (a b : MDPs.Histrv M) (h : MDPs.Hist M) => a h + b h }

instance MDPs.instHAddRVRV {σ α : Type} {M : MDPs.MDP σ α} : HAdd ℝ (MDPs.Histrv M) (MDPs.Histrv M)

Equations

• MDPs.instHAddRVRV = { hAdd := fun (a : ℝ) (b : MDPs.Histrv M) (h : MDPs.Hist M) => a + b h }

theorem MDPs.exph_add_rv {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} (X Y : MDPs.Histrv M) : MDPs.expect_h h π t (X + Y) = MDPs.expect_h h π t X + MDPs.expect_h h π t Y

theorem MDPs.exph_const {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} (X : MDPs.Histrv M) (c : ℝ) : (MDPs.expect_h h π t fun (x : MDPs.Hist M) => c) = c

theorem MDPs.exph_add_const {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} (X : MDPs.Hist M → ℝ) (c : ℝ) : MDPs.expect_h h π t ((fun (x : MDPs.Hist M) => c) + X) = c + MDPs.expect_h h π t X

theorem MDPs.exph_congr {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} (X Y : MDPs.Hist M → ℝ) (rv_eq : ∀ h' ∈ MDPs.ℋ h t, X h' = Y h') : MDPs.expect_h h π t X = MDPs.expect_h h π t Y

Expected return can be expressed as a sum of expected rewards

def MDPs.rew_sum {σ α : Type} {M : MDPs.MDP σ α} [Inhabited α] (h : MDPs.Hist M) : ℝ

Equations

• MDPs.rew_sum h = ∑ k ∈ Finset.range h.length, M.r (MDPs.state k h) (MDPs.action k h) (MDPs.state (k + 1) h)

def MDPs.rew_sum_rg {σ α : Type} {M : MDPs.MDP σ α} [Inhabited α] (b e : ℕ) (h : MDPs.Hist M) : ℝ

Sum of rewards with start (b) and end (e) (is exclusive)

Equations

• MDPs.rew_sum_rg b e h = ∑ k ∈ Finset.range (e - b), M.r (MDPs.state (b + k) h) (MDPs.action (b + k) h) (MDPs.state (b + k + 1) h)

theorem MDPs.state_last {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {k : ℕ} (keq : k = h.length) : MDPs.state k h = h.last

theorem MDPs.state_foll_last {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {s : σ} {a : α} {k : ℕ} (keq : k = h.length) : MDPs.state k (h.foll a s) = h.last

theorem MDPs.action_last {σ α : Type} {M : MDPs.MDP σ α} {s : σ} {a : α} [Inhabited α] {h : MDPs.Hist M} {k : ℕ} (keq : k = h.length + 1) : MDPs.action (h.foll a s).length (h.foll a s) = a

theorem MDPs.state_foll_eq {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {s : σ} {a : α} {k : ℕ} (kleq : k ≤ h.length) : MDPs.state k h = MDPs.state k (h.foll a s)

theorem MDPs.ret_eq_sum_rew {σ α : Type} {M : MDPs.MDP σ α} [Inhabited σ] [Inhabited α] (h : MDPs.Hist M) : MDPs.reward h = MDPs.rew_sum h

theorem MDPs.expret_eq_sum_rew {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} [Inhabited σ] [Inhabited α] : MDPs.expect_h h π t MDPs.reward = MDPs.expect_h h π t MDPs.rew_sum

Expected return can be expressed as a sum of expected rewards

theorem MDPs.sum_rew_eq_sum_rew_rg {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} [Inhabited σ] [Inhabited α] : MDPs.expect_h h π t MDPs.rew_sum = MDPs.rew_sum h + MDPs.expect_h h π t (MDPs.rew_sum_rg h.length t)

theorem MDPs.exph_zero_horizon_eq_zero {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} [Inhabited σ] [Inhabited α] (hzero : h.length = 0) : MDPs.expect_h h π 0 MDPs.reward = 0

theorem MDPs.exph_zero_horizon_eq_zero_f {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} [Inhabited σ] [Inhabited α] (hzero : h.length = 0) : MDPs.expect_h h π 0 (MDPs.reward_from 0) = 0

theorem MDPs.exph_horizon_cut {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} [Inhabited σ] [Inhabited α] {X : MDPs.Histrv M} (k : ℕ) (kle : k ≤ t) (eqpastk : ∀ (h : MDPs.Hist M), X h = X (MDPs.Hist.prefix k h)) : MDPs.expect_h h π t X = MDPs.expect_h h π k X

When the random variable beyond a point does not matter, cut the horizon's expectation

theorem MDPs.exph_horizon_trim {σ α : Type} {M : MDPs.MDP σ α} {π : MDPs.PolicyHR M} [Inhabited σ] [Inhabited α] {X : MDPs.Histrv M} {h : MDPs.Hist M} (s : { x : σ // x ∈ M.S }) (a : { x : α // x ∈ M.A }) : X (h.foll ↑a ↑s) = X (MDPs.Hist.one h.last ↑a ↑s) → MDPs.expect_h h π 1 X = MDPs.expect_h (MDPs.Hist.init h.last) π 1 X

theorem MDPs.total_expectation_h {σ α : Type} {M : MDPs.MDP σ α} {ν : Type} [DecidableEq ν] {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} {X : MDPs.Hist M → ℝ} {Y : MDPs.Hist M → ν} : MDPs.expect_h h π t (MDPs.expect_h_cnd_rv h π t X Y) = MDPs.expect_h h π t X

theorem MDPs.exph_cond_eq_hist {σ α : Type} {M : MDPs.MDP σ α} {h : MDPs.Hist M} {π : MDPs.PolicyHR M} {t : ℕ} (s : { x : σ // x ∈ M.S }) (a : { x : α // x ∈ M.A }) [Inhabited α] [Inhabited σ] [BEq α] [BEq σ] : (MDPs.expect_h_cnd h π (t + 1) MDPs.reward fun (h' : MDPs.Hist M) => decide ((MDPs.action h.length h' == ↑a) = true ∧ (MDPs.state (h.length + 1) h' == ↑s) = true)) = MDPs.expect_h (h.foll ↑a ↑s) π t MDPs.reward