inductive Conf (P : Type u_1) (S : Type u_2) (T : Type u_3) : Type (max (max u_1 u_2) u_3)

• term {P : Type u_1} {S : Type u_2} {T : Type u_3} (t : T) (σ : S) : Conf P S T
• prog {P : Type u_1} {S : Type u_2} {T : Type u_3} : P → (σ : S) → Conf P S T
• bot {P : Type u_1} {S : Type u_2} {T : Type u_3} : Conf P S T

class SmallStepSemantics (P : Type u_1) (S : Type u_2) (T : Type u_3) (A : Type u_4) [Nonempty A] : Type (max (max (max u_1 u_2) u_3) u_4)

• r : P × S → A → ENNReal → (P ⊕ T) × S → Prop
• relation_p_pos {c : P × S} {α : A} {p : ENNReal} {c' : (P ⊕ T) × S} : r c α p c' → ¬p = 0
• succs_sum_to_one {c : P × S} {α : A} {p₀ : ENNReal} {c' : (P ⊕ T) × S} : r c α p₀ c' → ∑' (b : (P ⊕ T) × S) (p : { p : ENNReal // r c α p b }), ↑p = 1
• progress (s : P × S) : ∃ (p : ENNReal) (a : A) (x : (P ⊕ T) × S), r s a p x
• cost_p : P × S → ENNReal
• cost_t : (S → ENNReal) →o T × S → ENNReal

@[implicit_reducible]

noncomputable instance SmallStepSemantics.instInhabited {A : Type u_3} [Nonempty A] : Inhabited A

Equations

• SmallStepSemantics.instInhabited = Classical.inhabited_of_nonempty inst✝

inductive SmallStepSemantics.rr {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : Conf P S T → Option A → ENNReal → Conf P S T → Prop

• bot {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : rr Conf.bot none 1 Conf.bot
• term {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {x✝ : T} {x✝¹ : S} : rr (Conf.term x✝ x✝¹) none 1 Conf.bot
• prog₀ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {C : P} {σ : S} {α : A} {p : ENNReal} {C' : P} {σ' : S} : r (C, σ) α p (Sum.inl C', σ') → rr (Conf.prog C σ) (some α) p (Conf.prog C' σ')
• prog₁ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {C : P} {σ : S} {α : A} {p : ENNReal} {t : T} {σ' : S} : r (C, σ) α p (Sum.inr t, σ') → rr (Conf.prog C σ) (some α) p (Conf.term t σ')

@[simp]

theorem SmallStepSemantics.rr.bot_to {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {α : Option A} {p : ENNReal} {c' : Conf P S T} : rr Conf.bot α p c' ↔ α = none ∧ p = 1 ∧ c' = Conf.bot

@[simp]

theorem SmallStepSemantics.rr.term_to {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {t : T} {σ : S} {α : Option A} {p : ENNReal} {c' : Conf P S T} : rr (Conf.term t σ) α p c' ↔ α = none ∧ p = 1 ∧ c' = Conf.bot

@[reducible, inline]

abbrev SmallStepSemantics.conf₂_to_conf {P : Type u_1} {S : Type u_2} {T : Type u_4} : (P ⊕ T) × S → Conf P S T

Equations

• SmallStepSemantics.conf₂_to_conf (Sum.inl C, σ) = Conf.prog C σ
• SmallStepSemantics.conf₂_to_conf (Sum.inr t, σ) = Conf.term t σ

@[reducible, inline]

abbrev SmallStepSemantics.conf_to_conf₂ {P : Type u_1} {S : Type u_2} {T : Type u_4} : Conf P S T → Option ((P ⊕ T) × S)

Equations

• SmallStepSemantics.conf_to_conf₂ (Conf.prog C σ) = some (Sum.inl C, σ)
• SmallStepSemantics.conf_to_conf₂ (Conf.term t σ) = some (Sum.inr t, σ)
• SmallStepSemantics.conf_to_conf₂ Conf.bot = none

@[simp]

theorem SmallStepSemantics.rr_prog {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {C : P} {σ : S} {α : Option A} {p : ENNReal} {c' : Conf P S T} : rr (Conf.prog C σ) α p c' ↔ ∃ (c'' : (P ⊕ T) × S) (α' : A), r (C, σ) α' p c'' ∧ conf₂_to_conf c'' = c' ∧ some α' = α

theorem SmallStepSemantics.relation_p_pos' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {c : Conf P S T} {α : Option A} {p : ENNReal} {c' : Conf P S T} : rr c α p c' → ¬p = 0

theorem SmallStepSemantics.succs_tum_to_one' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {c : Conf P S T} {α : Option A} {p₀ : ENNReal} {c' : Conf P S T} : rr c α p₀ c' → ∑' (b : Conf P S T) (p : { p : ENNReal // rr c α p b }), ↑p = 1

theorem SmallStepSemantics.progress' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (s : Conf P S T) : ∃ (p : ENNReal) (a : Option A) (x : Conf P S T), rr s a p x

noncomputable def SmallStepSemantics.mdp {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : MDP (Conf P S T) (Option A)

Equations

• SmallStepSemantics.mdp = MDP.ofRelation SmallStepSemantics.rr ⋯ ⋯ ⋯

def SmallStepSemantics.psucc {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (C : P) (σ : S) (α : A) : Set (ENNReal × (P ⊕ T) × S)

Equations

• SmallStepSemantics.psucc C σ α = {s : ENNReal × (P ⊕ T) × S | SmallStepSemantics.r (C, σ) α s.1 s.2}

theorem SmallStepSemantics.sub_psucc_eq_sum_r {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (C : P) (σ : S) (α : A) (f : ENNReal × (P ⊕ T) × S → ENNReal) : ∑' (s : ↑(psucc C σ α)), f ↑s = ∑' (s : { s : (P ⊕ T) × S // ∃ (p : ENNReal), r (C, σ) α p s }) (p : { sp : ENNReal × (P ⊕ T) × S // sp.2 = ↑s ∧ r (C, σ) α sp.1 sp.2 }), f ↑p

theorem SmallStepSemantics.sum_psucc_eq_sub_succ_univ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (C : P) (σ : S) (α : A) (f : ENNReal × (P ⊕ T) × S → ENNReal) : ∑' (s : ↑(psucc C σ α)), f ↑s = ∑' (x : ↑(mdp.succs_univ (Conf.prog C σ))) (p : { p : ENNReal // rr (Conf.prog C σ) (some α) p ↑x }), match conf_to_conf₂ ↑x with | some C_1 => f (↑p, C_1) | x => 0

def SmallStepSemantics.cost {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (X : S → ENNReal) : mdp.Costs

Equations

• SmallStepSemantics.cost X Conf.bot = 0
• SmallStepSemantics.cost X (Conf.term t σ) = (SmallStepSemantics.cost_t P A) X (t, σ)
• SmallStepSemantics.cost X (Conf.prog C σ) = SmallStepSemantics.cost_p T A (C, σ)

def SmallStepSemantics.cost_mono {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : Monotone cost

Equations

• ⋯ = ⋯

theorem SmallStepSemantics.cost_le_apply {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {a b : S → ENNReal} {x : Conf P S T} (h : a ≤ b) : cost a x ≤ cost b x

@[simp]

theorem SmallStepSemantics.cost_bot {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (X : S → ENNReal) : cost X Conf.bot = 0

def SmallStepSemantics.act {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (c : Conf P S T) : Set (Option A)

Equations

• SmallStepSemantics.act c = {α : Option A | ∃ (p : ENNReal) (c' : Conf P S T), SmallStepSemantics.rr c α p c'}

noncomputable def Optimization.act {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (O : Optimization) (C : Conf P S T) : (Option A → ENNReal) →o ENNReal

Equations

• O.act C = O.sOpt (SmallStepSemantics.act C)

theorem Optimization.act_gcongr {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {C : Conf P S T} {f₁ f₂ : Option A → ENNReal} (h : ∀ (α : Option A), f₁ α ≤ f₂ α) : (O.act C) f₁ ≤ (O.act C) f₂

noncomputable def SmallStepSemantics.op {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (O : Optimization) (C : P) : (S → ENNReal) →o S → ENNReal

Equations

• SmallStepSemantics.op O C = { toFun := fun (X : S → ENNReal) (x : S) => OrderHom.lfp (MDP.Φ O (SmallStepSemantics.cost X)) (Conf.prog C x), monotone' := ⋯ }

theorem SmallStepSemantics.tsum_succs_univ' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {c : Conf P S T} (f : ↑(mdp.succs_univ c) → ENNReal) : ∑' (s' : ↑(mdp.succs_univ c)), f s' = ∑' (s' : Conf P S T), if h : s' ∈ mdp.succs_univ c then f ⟨s', h⟩ else 0

noncomputable def SmallStepSemantics.Φ' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (O : Optimization) (c : mdp.Costs) (C : Conf P S T) (f : mdp.Costs) : ENNReal

Equations

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

@[simp]

theorem SmallStepSemantics.Φ_simp {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {c f : mdp.Costs} {C : Conf P S T} : (MDP.Φ O c) f C = Φ' O c C f

@[simp]

theorem SmallStepSemantics.succs_univ_term {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {t : T} {σ : S} : mdp.succs_univ (Conf.term t σ) = {Conf.bot}

@[simp]

theorem SmallStepSemantics.succs_univ_bot {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : mdp.succs_univ Conf.bot = {Conf.bot}

@[simp]

theorem SmallStepSemantics.succs_univ_prog {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {C : P} {σ : S} : mdp.succs_univ (Conf.prog C σ) = conf₂_to_conf '' {c' : (P ⊕ T) × S | ∃ (p : ENNReal) (α : A), r (C, σ) α p c'}

@[simp]

theorem SmallStepSemantics.Φ_bot_eq {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {X : S → ENNReal} {n : ℕ} : (⇑(MDP.Φ O (cost X)))^[n] ⊥ Conf.bot = 0

@[simp]

theorem SmallStepSemantics.Φ_term_eq {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {X : S → ENNReal} {n : ℕ} {t : T} {σ : S} : (⇑(MDP.Φ O (cost X)))^[n] ⊥ (Conf.term t σ) = if n = 0 then 0 else cost X (Conf.term t σ)

noncomputable def SmallStepSemantics.ξ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] (O : Optimization) : (P → (S → ENNReal) →o S → ENNReal) →o P → (S → ENNReal) →o S → ENNReal

Equations

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

theorem SmallStepSemantics.ξ_apply {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {Y : P → (S → ENNReal) →o S → ENNReal} {C : P} {X : S → ENNReal} : ((ξ O) Y C) X = fun (σ : S) => Φ' O (cost X) (Conf.prog C σ) fun (x : Conf P S T) => match x with | Conf.prog C' σ' => (Y C') X σ' | Conf.term t σ' => (cost_t P A) X (t, σ') | Conf.bot => 0

theorem SmallStepSemantics.ξ_apply' {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {Y : P → (S → ENNReal) →o S → ENNReal} {C : P} {X : S → ENNReal} {σ : S} : ((ξ O) Y C) X σ = Φ' O (cost X) (Conf.prog C σ) fun (x : Conf P S T) => match x with | Conf.prog C' σ' => (Y C') X σ' | Conf.term t σ' => (cost_t P A) X (t, σ') | Conf.bot => 0

theorem SmallStepSemantics.tsum_ite_left {α : Type u_5} {β : Type u_6} [AddCommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (x : β → α) : (∑' (b : β), if P then x b else 0) = if P then ∑' (b : β), x b else 0

class SmallStepSemantics.FiniteBranching (P : Type u_5) (S : Type u_6) (T : Type u_7) (A : Type u_8) [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : Prop

• finite (C : P × S) : {(α, p, C') : A × ENNReal × (P ⊕ T) × S | r C α p C'}.Finite

theorem SmallStepSemantics.finiteBranching_iff (P : Type u_5) (S : Type u_6) (T : Type u_7) (A : Type u_8) [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : FiniteBranching P S T A ↔ ∀ (C : P × S), {(α, p, C') : A × ENNReal × (P ⊕ T) × S | r C α p C'}.Finite

@[simp]

theorem SmallStepSemantics.mdp_act_term {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {t : T} {σ : S} : mdp.act (Conf.term t σ) = {none}

@[simp]

theorem SmallStepSemantics.mdp_act_bot {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] : mdp.act Conf.bot = {none}

instance SmallStepSemantics.instFiniteBranchingMDP {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] [instFin : FiniteBranching P S T A] : mdp.FiniteBranching

@[simp]

theorem SmallStepSemantics.lfp_Φ_O_bot {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {X : S → ENNReal} [O.ΦContinuous mdp] : OrderHom.lfp (MDP.Φ O (cost X)) Conf.bot = 0

@[simp]

theorem SmallStepSemantics.lfp_Φ_O_term {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} {X : S → ENNReal} {t : T} {σ : S} [O.ΦContinuous mdp] : OrderHom.lfp (MDP.Φ O (cost X)) (Conf.term t σ) = cost X (Conf.term t σ)

theorem SmallStepSemantics.op_eq_iSup_Φ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [O.ΦContinuous mdp] : op O = ⨆ (n : ℕ), fun (C : P) => { toFun := fun (X : S → ENNReal) (σ : S) => (⇑(MDP.Φ O (cost X)))^[n] ⊥ (Conf.prog C σ), monotone' := ⋯ }

theorem SmallStepSemantics.op_eq_iSup_succ_Φ {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [i : O.ΦContinuous mdp] : op O = ⨆ (n : ℕ), fun (C : P) => { toFun := fun (X : S → ENNReal) (σ : S) => (⇑(MDP.Φ O (cost X)))^[n + 1] ⊥ (Conf.prog C σ), monotone' := ⋯ }

theorem SmallStepSemantics.ξ_op_eq_op {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [O.ΦContinuous mdp] : (ξ O) (op O) = op O

theorem SmallStepSemantics.op_isLeast {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [O.ΦContinuous mdp] (b : P → (S → ENNReal) →o S → ENNReal) (h : (ξ O) b ≤ b) : op O ≤ b

theorem SmallStepSemantics.lfp_ξ_eq_op {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [O.ΦContinuous mdp] : OrderHom.lfp (ξ O) = op O

theorem SmallStepSemantics.ξ_continuous {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [i : O.ΦContinuous mdp] : OmegaCompletePartialOrder.ωScottContinuous ⇑(ξ O)

theorem SmallStepSemantics.op_eq_iter {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {O : Optimization} [O.ΦContinuous mdp] : op O = ⨆ (n : ℕ), (⇑(ξ O))^[n] ⊥

class SmallStepSemantics.ET {P : Type u_5} {S : Type u_6} {T : Type u_7} {A : Type u_8} [Nonempty A] (𝕊 : SmallStepSemantics P S T A) (O : Optimization) [O.ΦContinuous mdp] (et : P → (S → ENNReal) →o S → ENNReal) : Prop

• et_le_op : et ≤ op O
• et_prefixed_point : (ξ O) et ≤ et

theorem SmallStepSemantics.ET.et_eq_op {O : Optimization} {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] {et : P → (S → ENNReal) →o S → ENNReal} [O.ΦContinuous mdp] [i' : 𝕊.ET O et] : et = op O

theorem SmallStepSemantics.op_le_seq {O : Optimization} {P : Type u_1} {S : Type u_2} {A : Type u_3} {T : Type u_4} [Nonempty A] [𝕊 : SmallStepSemantics P S T A] [O.ΦContinuous mdp] {C C' : P} (seq : P → P → P) (after : P → (P ⊕ T) × S → (P ⊕ T) × S) (t_const : S → ENNReal) (h_cost_seq : ∀ (C C' : P) (σ : S), cost_p T A (seq C C', σ) = cost_p T A (C, σ)) (h_seq_act : ∀ (C C' : P) (σ : S), act (Conf.prog (seq C C') σ) = act (Conf.prog C σ)) (h_succ : ∀ {C C' : P} {σ : S} {p : ENNReal} {α : A} {s : (P ⊕ T) × S}, (p, s) ∈ psucc C σ α → (p, after C' s) ∈ psucc (seq C C') σ α) (h_after_p : ∀ {C C' : P} {σ : S}, after C' (Sum.inl C, σ) = (Sum.inl (seq C C'), σ)) (h_after_t : ∀ {t : T} {C : P} {C' : (P ⊕ T) × S} {σ : S}, after C (Sum.inr t, σ) = C' → C' = (Sum.inl C, σ) ∨ C' = (Sum.inr t, σ) ∧ ∀ (X : S → ENNReal), (cost_t P A) X (t, σ) = t_const σ) (h_c : ∀ {X : S → ENNReal} {t : T} {σ : S} {C' : P}, after C' (Sum.inr t, σ) = (Sum.inl C', σ) → (cost_t P A) ((op O C') X) (t, σ) ≤ (op O C') X σ) (after_inj : ∀ (x : P), Function.Injective (after x)) : ⇑(op O C) ∘ ⇑(op O C') ≤ ⇑(op O (seq C C'))