def MDP.Path_eq {State : Type u_1} {Act : Type u_2} (M : MDP State Act) (n : ℕ) (s : State) : Set M.Path

Paths starting in s with length n

Equations

• Path[M,s,=n] = {π : M.Path | ‖π‖ = n ∧ π[0] = s}

def MDP.Path_le {State : Type u_1} {Act : Type u_2} (M : MDP State Act) (n : ℕ) (s : State) : Set M.Path

Paths starting in s with length at most n

Equations

• Path[M,s,≤n] = {π : M.Path | ‖π‖ ≤ n ∧ π[0] = s}

def MDP.«termPath[_,_,=_]» : Lean.ParserDescr

Paths starting in s with length n

Equations

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

def MDP.«termPath[_,_,≤_]» : Lean.ParserDescr

Paths starting in s with length at most n

Equations

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

instance MDP.instDecidableMemPathSetPath_eqOfDecidableEq {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {n : ℕ} {s : State} {π : M.Path} [DecidableEq State] : Decidable (π ∈ Path[M,s,=n])

Equations

• M.instDecidableMemPathSetPath_eqOfDecidableEq = instDecidableAnd

instance MDP.instDecidableMemPathSetPath_leOfDecidableEq {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {n : ℕ} {s : State} {π : M.Path} [DecidableEq State] : Decidable (π ∈ Path[M,s,≤n])

Equations

• M.instDecidableMemPathSetPath_leOfDecidableEq = instDecidableAnd

@[simp]

theorem MDP.Path_eq.length_pos {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,=n]) : 0 < ‖↑π‖

@[simp]

theorem MDP.Path_eq.first_eq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,=n]) : (↑π)[0] = s

@[simp]

theorem MDP.Path_eq.length_eq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,=n]) : ‖↑π‖ = n

@[simp]

theorem MDP.Path_eq.iff {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : M.Path) : π ∈ Path[M,s,=n] ↔ ‖π‖ = n ∧ π[0] = s

instance MDP.Path_eq.instSubsingletonElemPathOfNatNat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : Subsingleton ↑Path[M,s,=0]

@[simp]

theorem MDP.Path_eq.length_zero {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : Path[M,s,=0] = ∅

@[simp]

theorem MDP.Path_eq.length_one_singleton {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : Path[M,s,=1] = {{s}}

@[simp]

theorem MDP.Path_eq.length_zero_tsum {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} (f : ↑Path[M,s,=0] → ENNReal) : ∑' (π : ↑Path[M,s,=0]), f π = 0

@[simp]

theorem MDP.Path_eq.length_zero_tsum_singleton {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} (f : ↑Path[M,s,=1] → ENNReal) : ∑' (π : ↑Path[M,s,=1]), f π = f ⟨{s}, ⋯⟩

theorem MDP.Path_le.succs_univ_Finite {State : Type u_1} {Act : Type u_2} {M : MDP State Act} [DecidableEq State] [M.FiniteBranching] (π : M.Path) : π.succs_univ.Finite

noncomputable instance MDP.Path_le.instFintypeElemPathSuccs_univOfDecidableEqOfFiniteBranching {State : Type u_1} {Act : Type u_2} {M : MDP State Act} [DecidableEq State] [M.FiniteBranching] (π : M.Path) : Fintype ↑π.succs_univ

Equations

• MDP.Path_le.instFintypeElemPathSuccs_univOfDecidableEqOfFiniteBranching π = ⋯.fintype

@[simp]

theorem MDP.Path_le.length_pos {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,≤n]) : 0 < ‖↑π‖

@[simp]

theorem MDP.Path_le.length_le {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,≤n]) : ‖↑π‖ ≤ n

@[simp]

theorem MDP.Path_le.first_le {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : ↑Path[M,s,≤n]) : (↑π)[0] = s

@[simp]

theorem MDP.Path_le.iff {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} (π : M.Path) : π ∈ Path[M,s,≤n] ↔ ‖π‖ ≤ n ∧ π[0] = s

instance MDP.Path_le.instSubsingletonElemPathOfNatNat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : Subsingleton ↑Path[M,s,≤0]

theorem MDP.Path_le.finite {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} [DecidableEq State] [M.FiniteBranching] : Path[M,s,≤n].Finite

noncomputable instance MDP.Path_le.instFintypeElemPathOfDecidableEqOfFiniteBranching {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {n : ℕ} {s : State} [DecidableEq State] [M.FiniteBranching] : Fintype ↑Path[M,s,≤n]

Equations

• MDP.Path_le.instFintypeElemPathOfDecidableEqOfFiniteBranching = ⋯.fintype

@[reducible, inline]

abbrev MDP.Path_eq_follows {State : Type u_1} {Act : Type u_2} (M : MDP State Act) (s₀ : State) (n : ℕ) (s₁ : ↑(M.succs_univ s₀)) : Set M.Path

The set of paths of the kind s₀ s₁ ⋯ sₙ₊₁

Equations

• Path[M,s₀─s₁,=n] = {π : M.Path | ∃ (h : π ∈ Path[M,s₀,=n + 2]), π[1] = ↑s₁}

def MDP.«termPath[_,_─_,=_]» : Lean.ParserDescr

The set of paths of the kind s₀ s₁ ⋯ sₙ₊₁

Equations

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

theorem MDP.Path_eq_follows_disjoint {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {s₀ : State} {n : ℕ} : Set.univ.PairwiseDisjoint fun (x : ↑(M.succs_univ s₀)) => Path[M,s₀─x,=n]

theorem MDP.Path_eq.succs_univ_disjoint {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {n : ℕ} {s : State} : Path[M,s,=n].PairwiseDisjoint Path.succs_univ

theorem MDP.Path_eq.eq_biUnion_succs_univ {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {n : ℕ} {s : State} : Path[M,s,=n + 2] = ⋃ (π : ↑Path[M,s,=n + 1]), (↑π).succs_univ

theorem MDP.Path_eq.eq_succs_univ_biUnion {State : Type u_1} {Act : Type u_2} (M : MDP State Act) {n : ℕ} {s : State} : Path[M,s,=n + 2] = ⋃ (s' : ↑(M.succs_univ s)), Path[M,s─s',=n]