noncomputable def MDP.Path.Prob {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (𝒮 : 𝔖[M]) (π : M.Path) : ENNReal

Equations

• MDP.Path.Prob 𝒮 π = ∏ i : Fin (‖π‖ - 1), M.P π[i] (𝒮 (π.take ↑i)) π[i.succ]

@[simp]

theorem MDP.Path.singleton_Prob {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (x : State) (𝒮 : 𝔖[M]) : Prob 𝒮 {x} = 1

@[simp]

theorem MDP.Path.Prob_le_one {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (𝒮 : 𝔖[M]) : Prob 𝒮 π ≤ 1

@[simp]

theorem MDP.Path.Prob_ne_top {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (𝒮 : 𝔖[M]) : Prob 𝒮 π ≠ ⊤

theorem MDP.Path.extend_Prob {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.succs_univ π.last)) (𝒮 : 𝔖[M]) : Prob 𝒮 (π.extend s) = M.P π.last (𝒮 π) ↑s * Prob 𝒮 π

theorem MDP.Path.prepend_Prob {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) [DecidableEq State] (𝒮 : 𝔖[M]) (s : ↑(M.prev_univ π[0])) : Prob 𝒮 (π.prepend s) = M.P (↑s) (𝒮 {↑s}) π[0] * Prob (𝒮.specialize ↑s ⟨π[0], ⋯⟩) π

theorem MDP.Path.Prob_tail {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) [DecidableEq State] (h : 1 < ‖π‖) (𝒮 : 𝔖[M]) : Prob 𝒮 π = M.P π[0] (𝒮 {π[0]}) π[1] * Prob (𝒮.specialize π[0] ⟨π[1], ⋯⟩) π.tail

@[simp]

theorem MDP.Path.tsum_succs_univ_Prob_eq_one {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {𝒮 : 𝔖[M]} (π : M.Path) : ∑' (π' : ↑π.succs_univ), Prob 𝒮 ↑π' = Prob 𝒮 π

@[simp]

theorem MDP.Path.tsum_Prob_eq_one {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {𝒮 : 𝔖[M]} (n : ℕ) : ∑' (π : ↑Path[M,s,=n + 1]), Prob 𝒮 ↑π = 1

theorem MDP.Path_eq.tsum_add_left {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s' : State} {𝒮 : 𝔖[M]} {a : ENNReal} (f : ↑Path[M,s',=n + 1] → ENNReal) : ∑' (π : ↑Path[M,s',=n + 1]), (Path.Prob 𝒮 ↑π * a + f π) = a + ∑' (π : ↑Path[M,s',=n + 1]), f π

@[simp]

theorem MDP.Path.tsum_Prob_eq_one_comp {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {𝒮 : 𝔖[M]} (n : ℕ) (S : Set ↑Path[M,s,=n + 1]) : ∑' (π : ↑S), Prob 𝒮 ↑↑π + ∑' (π : ↑Sᶜ), Prob 𝒮 ↑↑π = 1

@[simp]

theorem MDP.Path.one_sub_tsum_ite_Prob_eq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {𝒮 : 𝔖[M]} (n : ℕ) (p : ↑Path[M,s,=n + 1] → Prop) [DecidablePred p] : (1 - ∑' (π : ↑Path[M,s,=n + 1]), if p π then Prob 𝒮 ↑π else 0) = ∑' (π : ↑Path[M,s,=n + 1]), if p π then 0 else Prob 𝒮 ↑π

@[simp]

theorem MDP.Path.one_sub_tsum_ite_Prob_eq' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {𝒮 : 𝔖[M]} (n : ℕ) (p : ↑Path[M,s,=n + 1] → Prop) [DecidablePred p] : (1 - ∑' (π : ↑Path[M,s,=n + 1]), if p π then 0 else Prob 𝒮 ↑π) = ∑' (π : ↑Path[M,s,=n + 1]), if p π then Prob 𝒮 ↑π else 0