noncomputable def Finset.argmax' {τ : Type u_1} (I : Finset τ) (H : I.Nonempty) (f : { x : τ // x ∈ I } → ℝ) : { x : τ // x ∈ I }

Equations

• I.argmax' H f = match List.argmax f I.attach.toList, ⋯ with | some x, x_1 => x

theorem le_of_mem_argmax' {τ : Type u_1} {a : τ} {S : Finset τ} {f : { x : τ // x ∈ S } → ℝ} (h : a ∈ S) (NE : S.Nonempty) : f ⟨a, h⟩ ≤ f (S.argmax' NE f)

theorem argmax_eq_sup {τ : Type u_1} {S : Finset τ} {f : { x : τ // x ∈ S } → ℝ} (NE : S.Nonempty) : S.attach.sup' ⋯ f = f (S.argmax' NE f)

structure MDPs.ObjectiveFH {σ α : Type} (M : MDPs.MDP σ α) : Type

Finite horizon objective parameters

• s₀ : { x : σ // x ∈ M.S }
• T : ℕ

def MDPs.objective_fh {σ α : Type} {M : MDPs.MDP σ α} (O : MDPs.ObjectiveFH M) (π : MDPs.PolicyHR M) : ℝ

Objective function

Equations

• MDPs.objective_fh O π = MDPs.expect_h (MDPs.Hist.init ↑O.s₀) π O.T MDPs.reward

def MDPs.Optimal_fh {σ α : Type} {M : MDPs.MDP σ α} (O : MDPs.ObjectiveFH M) (πopt : MDPs.PolicyHR M) : Prop

An optimal policy πopt

Equations

• MDPs.Optimal_fh O πopt = ∀ (π : MDPs.PolicyHR M), MDPs.objective_fh O πopt ≥ MDPs.objective_fh O π

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

Value function type for history-dependent value functions

Equations

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

def MDPs.hvalue_π {σ α : Type} {M : MDPs.MDP σ α} (π : MDPs.PolicyHR M) : ℕ → MDPs.ValuesH M

History-dependent value function

Equations

• MDPs.hvalue_π π Nat.zero = fun (x : MDPs.Hist M) => 0
• MDPs.hvalue_π π t.succ = fun (h : MDPs.Hist M) => MDPs.expect_h h π t.succ (MDPs.reward_from h.length)

def MDPs.OptimalVF_fh {σ α : Type} {M : MDPs.MDP σ α} (t : ℕ) (πopt : MDPs.PolicyHR M) : Prop

A value-optimal policy πopt

Equations

• MDPs.OptimalVF_fh t πopt = ∀ (π : MDPs.PolicyHR M) (h : MDPs.Hist M), MDPs.hvalue_π πopt t h ≥ MDPs.hvalue_π π t h

theorem MDPs.reward_eq_reward_from_0 {σ α : Type} {M : MDPs.MDP σ α} (h : MDPs.Hist M) : MDPs.reward h = MDPs.reward_from 0 h

theorem MDPs.optimalvf_imp_optimal {σ α : Type} {M : MDPs.MDP σ α} {O : MDPs.ObjectiveFH M} (πopt : MDPs.PolicyHR M) (opt : MDPs.OptimalVF_fh O.T πopt) : MDPs.Optimal_fh O πopt

def MDPs.DPhπ {σ α : Type} {M : MDPs.MDP σ α} (π : MDPs.PolicyHR M) (v : MDPs.ValuesH M) : MDPs.ValuesH M

Bellman operator on history-dependent value functions

Equations

• MDPs.DPhπ π v x✝ = MDPs.expect_h x✝ π 1 fun (h' : MDPs.Hist M) => MDPs.reward h' + v h'

def MDPs.DPhopt {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (u : MDPs.ValuesH M) : MDPs.ValuesH M

Bellman operator on history-dependent value functions

Equations

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

def MDPs.u_dp_π {σ α : Type} {M : MDPs.MDP σ α} (π : MDPs.PolicyHR M) : ℕ → MDPs.ValuesH M

Dynamic program value function, finite-horizon history dependent

Equations

• MDPs.u_dp_π π Nat.zero = fun (x : MDPs.Hist M) => 0
• MDPs.u_dp_π π t.succ = MDPs.DPhπ π (MDPs.u_dp_π π t)

def MDPs.u_dp_opt {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} : ℕ → MDPs.ValuesH M

Dynamic program value function, finite-horizon history dependent

Equations

• MDPs.u_dp_opt Nat.zero = fun (x : MDPs.Hist M) => 0
• MDPs.u_dp_opt t.succ = MDPs.DPhopt (MDPs.u_dp_opt t)

theorem MDPs.dp_opt_ge_dp_pi {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} (h : MDPs.Hist M) (u₁ u₂ : MDPs.ValuesH M) (uge : ∀ (h : MDPs.Hist M), u₁ h ≥ u₂ h) (h✝ : MDPs.Hist M) (π : MDPs.PolicyHR M) : MDPs.DPhopt u₁ h✝ ≥ MDPs.DPhπ π u₂ h✝

theorem MDPs.dph_correct_vf {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} (π : MDPs.PolicyHR M) (t : ℕ) (h : MDPs.Hist M) : MDPs.hvalue_π π t h = MDPs.u_dp_π π t h

theorem MDPs.dph_opt_vf_opt {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} (t : ℕ) (π : MDPs.PolicyHR M) (h : MDPs.Hist M) : MDPs.u_dp_opt t h ≥ MDPs.u_dp_π π t h

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

A deterministic Markov policy. Depends on the time step, and does not depend on the horizon.

Equations

• MDPs.PolicyMD M = (ℕ → MDPs.DecisionRule M)

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

Equations

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

def MDPs.Values {σ α : Type} : MDPs.MDP σ α → Type

History-independent value function. Note that the optimal value function is history-independent, while the value function of a Markov policy depends on the time step.

Equations

• MDPs.Values x✝ = (σ → ℝ)

def MDPs.q_of_v {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (s : σ) (a : { x : α // x ∈ M.A }) (v : MDPs.Values M) : ℝ

Markov q function

Equations

• MDPs.q_of_v s a v = MDPs.expect_h (MDPs.Hist.init s) (fun (x : MDPs.Hist M) => Finprob.dirac_dist M.A a) 1 fun (h : MDPs.Hist M) => MDPs.reward h + v h.last

def MDPs.DPMopt {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (v : MDPs.Values M) : MDPs.Values M

Bellman operator on history-dependent value functions

Equations

• MDPs.DPMopt v x✝ = M.A.attach.sup' ⋯ fun (a : { x : α // x ∈ M.A }) => MDPs.q_of_v x✝ a v

def MDPs.v_dp_opt {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} : ℕ → MDPs.Values M

Optimal value function

Equations

• MDPs.v_dp_opt Nat.zero = fun (x : σ) => 0
• MDPs.v_dp_opt t.succ = MDPs.DPMopt (MDPs.v_dp_opt t)

theorem MDPs.v_dp_opt_eq_u_opt {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} {t : ℕ} (h : MDPs.Hist M) : MDPs.v_dp_opt t h.last = MDPs.u_dp_opt t h

The Markov DP is optimal

noncomputable def MDPs.πopt {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (t : ℕ) : MDPs.PolicyMD M

Optimal policy for horizon t

Equations

• MDPs.πopt t x✝¹ x✝ = if t ≥ x✝¹ then M.A.argmax' ⋯ fun (a : { x : α // x ∈ M.A }) => MDPs.q_of_v x✝ a (MDPs.v_dp_opt (t - x✝¹)) else Classical.indefiniteDescription (fun (a : α) => a ∈ M.A) ⋯

theorem MDPs.v_dp_opt_eq_v_dp_π {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} {T : ℕ} (h : MDPs.Hist M) : h.length ≤ T → MDPs.v_dp_opt (T - h.length) h.last = MDPs.u_dp_π (fun (h : MDPs.Hist M) => Finprob.dirac_dist M.A (MDPs.πopt T h.length h.last)) (T - h.length) h

Greedy to v_opt is optimal policy

def MDPs.ValuesM {σ α : Type} : MDPs.MDP σ α → Type

Equations

• MDPs.ValuesM x✝ = (ℕ → σ → ℝ)

def MDPs.DPMπ {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (π : MDPs.PolicyMD M) (v : MDPs.ValuesM M) : MDPs.ValuesM M

Optimal Bellman operator on state-dependent value functions. Also includes the prior history's reward.

Equations

• MDPs.DPMπ π v x✝¹ x✝ = MDPs.expect_h (MDPs.Hist.init x✝) (fun (h : MDPs.Hist M) => Finprob.dirac_dist M.A (π h.length h.last)) 1 fun (h : MDPs.Hist M) => MDPs.reward h + v (x✝¹ + 1) h.last

def MDPs.v_dp_π {σ α : Type} [DecidableEq α] {M : MDPs.MDP σ α} (π : MDPs.PolicyMD M) : ℕ → MDPs.ValuesM M

Value function of a Markov policy. Horizon to value function.

Equations

• MDPs.v_dp_π π Nat.zero = fun (x : ℕ) => 0
• MDPs.v_dp_π π t.succ = MDPs.DPMπ π (MDPs.v_dp_π π t)

theorem MDPs.v_eq_u_π {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} {t : ℕ} {π : MDPs.PolicyMD M} (h : MDPs.Hist M) : MDPs.u_dp_π (fun (h : MDPs.Hist M) => Finprob.dirac_dist M.A (π h.length h.last)) t h = MDPs.v_dp_π π t h.length h.last

theorem MDPs.markov_u_quot {σ : Type} [Inhabited σ] [DecidableEq σ] {α : Type} [Inhabited α] [DecidableEq α] {M : MDPs.MDP σ α} {t : ℕ} {π : MDPs.PolicyMD M} (h₁ h₂ : MDPs.Hist M) : h₁.length = h₂.length ∧ h₁.last = h₂.last → MDPs.u_dp_π (fun (h : MDPs.Hist M) => Finprob.dirac_dist M.A (π h.length h.last)) t h₁ = MDPs.u_dp_π (fun (h : MDPs.Hist M) => Finprob.dirac_dist M.A (π h.length h.last)) t h₂