noncomputable def MDP.Ψ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (c : M.Costs) : M.Costs →o M.Costs

Equations

• MDP.Ψ c = { toFun := fun (v : M.Costs) (s : State) => c s + ⨆ (α : ↑(M.act s)), (MDP.Φf s ↑α) v, monotone' := ⋯ }

theorem MDP.tsum_succs_univ_iSup_iSup_EC_comm {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {α : Act} {c : M.Costs} [DecidableEq State] : ∑' (s' : ↑(M.succs_univ s)), ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), M.P s α ↑s' * EC c 𝒮 n ↑s' ≤ ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), ∑' (s' : ↑(M.succs_univ s)), M.P s α ↑s' * EC c 𝒮 n ↑s'

theorem MDP.iSup_iSup_EC_eq_lfp_Ψ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {c : M.Costs} [DecidableEq State] : ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), EC c 𝒮 n = OrderHom.lfp (Ψ c)

theorem MDP.iSup_iSup_ECℒ_le_iSup_iSup_EC {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {c : M.Costs} : ⨆ (n : ℕ), ⨆ (ℒ : 𝔏[M]), EC c (↑ℒ) n ≤ ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), EC c 𝒮 n