MDP.Counterexample

theorem MDP.exists_iSup_iInf_EC_lt_iInf_iSup_EC :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ⨆ (n : ℕ), ⨅ (𝒮 : 𝔖[M]), EC c 𝒮 n s < ⨅ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s

There exists a (necessarily infinite branching) MDP such that the two notions of optimization order (⨆⨅ vs. ⨅⨆) is not equivalent. See MDP.Counterexample.A.M for an instance of such and MDP.

source

theorem MDP.exists_iSup_iInf_ECℒ_lt_iInf_iSup_ECℒ :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ⨆ (n : ℕ), ⨅ (ℒ : 𝔏[M]), EC c (↑ℒ) n s < ⨅ (ℒ : 𝔏[M]), ⨆ (n : ℕ), EC c (↑ℒ) n s

There exists a (necessarily infinite branching) MDP such that the two notions of optimization order (⨆⨅ vs. ⨅⨆) is not equivalent with Markovian schedulers. See MDP.Counterexample.A.M for an instance of such and MDP.

source

theorem MDP.exists_iSup_iInf_EC_lt_lfp_Φ :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ⨆ (n : ℕ), ⨅ (𝒮 : 𝔖[M]), EC c 𝒮 n s < lfp_Φ c s

There exists a (necessarily infinite branching) MDP such that the ⨅⨆ notions of optimization order is not equivalent to the lfp formulation. See MDP.Counterexample.A.M for an instance of such and MDP.

source

theorem MDP.exists_iInf_iSup_EC_lt_iInf_iSup_ECℒ :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ⨅ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s < ⨅ (ℒ : 𝔏[M]), ⨆ (n : ℕ), EC c (↑ℒ) n s

There exists a (necessarily infinite branching) MDP such that the optimal cost given by ⨅⨆ with history is strictly less than that of the memoryless. See MDP.Counterexample.C.M for an instance of such and MDP.

source

theorem MDP.not_exists_optimal_𝒮_for_iSup_iInf_EC :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ¬∃ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s = ⨅ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s

There exists a (necessarily infinite branching) MDP such that there does not exist an optimal scheduler for the ⨅⨆ notion of optimization. See MDP.Counterexample.D.M for an instance of such and MDP.

source

theorem MDP.not_exists_optimal_𝒮_for_iSup_iSup_EC :

∃ (State : Type) (Act : Type) (M : MDP State Act) (c : M.Costs) (s : State), ¬∃ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s = ⨆ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), EC c 𝒮 n s

There exists a (necessarily infinite branching) MDP such that there does not exist an optimal scheduler for the ⨆⨆ notion of optimization. See MDP.Counterexample.D.M for an instance of such and MDP.