noncomputable def MDP.ofRelation {S : Type u_1} {A : Type u_2} (r : S → A → ENNReal → S → Prop) (h₀ : ∀ {c : S} {α : A} {p : ENNReal} {c' : S}, r c α p c' → ¬p = 0) (h₁ : ∀ {c : S} {α : A} {p₀ : ENNReal} {c' : S}, r c α p₀ c' → ∑' (b : S) (p : { p : ENNReal // r c α p b }), ↑p = 1) (h₂ : ∀ (s : S), ∃ (p : ENNReal) (a : A) (x : S), r s a p x) : MDP S A

Equations

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

@[simp]

theorem MDP.ofRelation_P {S : Type u_1} {A : Type u_2} {r : S → A → ENNReal → S → Prop} {h₀ : ∀ {c : S} {α : A} {p : ENNReal} {c' : S}, r c α p c' → ¬p = 0} {h₁ : ∀ {c : S} {α : A} {p₀ : ENNReal} {c' : S}, r c α p₀ c' → ∑' (b : S) (p : { p : ENNReal // r c α p b }), ↑p = 1} {h₂ : ∀ (s : S), ∃ (p : ENNReal) (a : A) (x : S), r s a p x} : (ofRelation r h₀ h₁ h₂).P = fun (c : S) (α : A) (c' : S) => ∑' (p : { p : ENNReal // r c α p c' }), ↑p

@[simp]

theorem MDP.ofRelation_act {S : Type u_1} {A : Type u_2} {r : S → A → ENNReal → S → Prop} {h₀ : ∀ {c : S} {α : A} {p : ENNReal} {c' : S}, r c α p c' → ¬p = 0} {h₁ : ∀ {c : S} {α : A} {p₀ : ENNReal} {c' : S}, r c α p₀ c' → ∑' (b : S) (p : { p : ENNReal // r c α p b }), ↑p = 1} {h₂ : ∀ (s : S), ∃ (p : ENNReal) (a : A) (x : S), r s a p x} : (ofRelation r h₀ h₁ h₂).act = fun (c : S) => {α : A | ∃ (p : ENNReal) (c' : S), r c α p c'}

@[simp]

theorem MDP.ofRelation_succs {S : Type u_1} {A : Type u_2} {r : S → A → ENNReal → S → Prop} {h₀ : ∀ {c : S} {α : A} {p : ENNReal} {c' : S}, r c α p c' → ¬p = 0} {h₁ : ∀ {c : S} {α : A} {p₀ : ENNReal} {c' : S}, r c α p₀ c' → ∑' (b : S) (p : { p : ENNReal // r c α p b }), ↑p = 1} {h₂ : ∀ (s : S), ∃ (p : ENNReal) (a : A) (x : S), r s a p x} : (ofRelation r h₀ h₁ h₂).succs = fun (α : A) (c : S) => {c' : S | ∃ (p : ENNReal), r c α p c'}

@[simp]

theorem MDP.ofRelation_succs_univ {S : Type u_1} {A : Type u_2} {r : S → A → ENNReal → S → Prop} {h₀ : ∀ {c : S} {α : A} {p : ENNReal} {c' : S}, r c α p c' → ¬p = 0} {h₁ : ∀ {c : S} {α : A} {p₀ : ENNReal} {c' : S}, r c α p₀ c' → ∑' (b : S) (p : { p : ENNReal // r c α p b }), ↑p = 1} {h₂ : ∀ (s : S), ∃ (p : ENNReal) (a : A) (x : S), r s a p x} : (ofRelation r h₀ h₁ h₂).succs_univ = fun (c : S) => {c' : S | ∃ (α : A) (p : ENNReal), r c α p c'}