Documentation

MDP.Counterexample.D

source
inductive MDP.Counterexample.D.State :
Type
Instances For
    source
    instance MDP.Counterexample.D.instDecidableEqState :
    DecidableEq State
    Equations
    source
    inductive MDP.Counterexample.D.Step :
    State โ†’ โ„• โ†’ ENNReal โ†’ State โ†’ Prop
    Instances For
      source
      theorem MDP.Counterexample.D.step_iff (aโœ : State) (aโœยน : โ„•) (aโœยฒ : ENNReal) (aโœยณ : State) :
      Step aโœ aโœยน aโœยฒ aโœยณ โ†” aโœ = State.init โˆง aโœยฒ = 1 โˆง aโœยณ = State.node aโœยน โˆจ (โˆƒ (i : โ„•), aโœ = State.node i โˆง aโœยน = 0 โˆง aโœยฒ = 1 โˆง aโœยณ = State.term) โˆจ aโœ = State.term โˆง aโœยน = 0 โˆง aโœยฒ = 1 โˆง aโœยณ = State.term
      source
      noncomputable instance MDP.Counterexample.D.instDecidableStep {c : State} {ฮฑ : โ„•} {p : ENNReal} {c' : State} :
      Decidable (Step c ฮฑ p c')
      Equations
      source
      @[simp]
      theorem MDP.Counterexample.D.init_iff {ฮฑ : โ„•} {p : ENNReal} {s' : State} :
      Step State.init ฮฑ p s' โ†” p = 1 โˆง s' = State.node ฮฑ
      source
      @[simp]
      theorem MDP.Counterexample.D.node_iff {i ฮฑ : โ„•} {p : ENNReal} {s' : State} :
      Step (State.node i) ฮฑ p s' โ†” p = 1 โˆง ฮฑ = 0 โˆง s' = State.term
      source
      @[simp]
      theorem MDP.Counterexample.D.term_iff {ฮฑ : โ„•} {p : ENNReal} {s' : State} :
      Step State.term ฮฑ p s' โ†” p = 1 โˆง ฮฑ = 0 โˆง s' = State.term
      source
      @[simp]
      theorem MDP.Counterexample.D.not_to_init {s : State} {ฮฑ : โ„•} {p : ENNReal} :
      ยฌStep s ฮฑ p State.init
      source
      @[simp]
      theorem MDP.Counterexample.D.tsum_p {c : State} {ฮฑ : โ„•} {c' : State} :
      โˆ‘' (p : { p : ENNReal // Step c ฮฑ p c' }), โ†‘p = โˆ‘' (p : ENNReal), if Step c ฮฑ p c' then p else 0
      source
      noncomputable def MDP.Counterexample.D.M :
      MDP State โ„•
      Equations
      Instances For
        source
        noncomputable def MDP.Counterexample.D.M.cost :
        M.Costs
        Equations
        Instances For
          source
          noncomputable def MDP.Counterexample.D.M.rew :
          M.Costs
          Equations
          Instances For
            source
            @[simp]
            theorem MDP.Counterexample.D.M.act_eq :
            M.act = fun (s : State) => if s = State.init then Set.univ else {0}
            source
            @[simp]
            theorem MDP.Counterexample.D.๐’ฎ_node {๐’ฎ : ๐”–[M]} {i : โ„•} :
            ๐’ฎ {State.node i} = 0
            source
            @[simp]
            theorem MDP.Counterexample.D.๐’ฎ_term {๐’ฎ : ๐”–[M]} :
            ๐’ฎ {State.term} = 0
            source
            @[simp]
            theorem MDP.Counterexample.D.succs_univ_init :
            M.succs_univ State.init = {x : State | โˆƒ (ฮฑ : โ„•), State.node ฮฑ = x}
            source
            @[simp]
            theorem MDP.Counterexample.D.succs_univ_node {i : โ„•} :
            M.succs_univ (State.node i) = {State.term}
            source
            @[simp]
            theorem MDP.Counterexample.D.succs_univ_term :
            M.succs_univ State.term = {State.term}
            source
            @[simp]
            theorem MDP.Counterexample.D.P_init_node {ฮฑ ฮฒ : โ„•} :
            M.P State.init ฮฑ (State.node ฮฒ) = if ฮฑ = ฮฒ then 1 else 0
            source
            @[simp]
            theorem MDP.Counterexample.D.P_node_term {i : โ„•} :
            M.P (State.node i) 0 State.term = 1
            source
            @[simp]
            theorem MDP.Counterexample.D.P_term_term :
            M.P State.term 0 State.term = 1
            source
            @[simp]
            theorem MDP.Counterexample.D.EC_term_eq_0 {๐’ฎ : ๐”–[M]} {n : โ„•} :
            EC M.cost ๐’ฎ n State.term = 0
            source
            @[simp]
            theorem MDP.Counterexample.D.EC_node_i_le_j_eq_top {๐’ฎ : ๐”–[M]} {n i : โ„•} :
            EC M.cost ๐’ฎ n (State.node i) = if n = 0 then 0 else 1 / โ†‘i
            source
            theorem MDP.Counterexample.D.EC_init {๐’ฎ : ๐”–[M]} {n : โ„•} :
            EC M.cost ๐’ฎ n State.init = if n < 2 then 0 else 1 / โ†‘(๐’ฎ {State.init})
            source
            @[simp]
            theorem MDP.Counterexample.D.all_๐’ฎ_lt_iSup_iInf_EC (๐’ฎ : ๐”–[M]) :
            โจ… (๐’ฎ : ๐”–[M]), โจ† (n : โ„•), EC M.cost ๐’ฎ n State.init < โจ† (n : โ„•), EC M.cost ๐’ฎ n State.init
            source
            @[simp]
            theorem MDP.Counterexample.D.ER_term_eq_0 {๐’ฎ : ๐”–[M]} {n : โ„•} :
            EC M.rew ๐’ฎ n State.term = 0
            source
            @[simp]
            theorem MDP.Counterexample.D.ER_node_i_le_j_eq_top {๐’ฎ : ๐”–[M]} {n i : โ„•} :
            EC M.rew ๐’ฎ n (State.node i) = โ†‘(if n = 0 then 0 else i)
            source
            theorem MDP.Counterexample.D.ER_init {๐’ฎ : ๐”–[M]} {n : โ„•} :
            EC M.rew ๐’ฎ n State.init = โ†‘(if n < 2 then 0 else ๐’ฎ {State.init})
            source
            @[simp]
            theorem MDP.Counterexample.D.all_๐’ฎ_iSup_iSup_ER_lt (๐’ฎ : ๐”–[M]) :
            โจ† (n : โ„•), EC M.rew ๐’ฎ n State.init < โจ† (๐’ฎ : ๐”–[M]), โจ† (n : โ„•), EC M.rew ๐’ฎ n State.init