BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonOptimality

# Finite-horizon Bellman optimality This module adds finite-action maximization to the compiled policy-evaluation route. On a finite discrete state space, the pointwise finite argmax is a measurable deterministic selector. The resulting greedy Markov policy attains the backward optimal value, which dominates every Markov policy value.

Module map

Declarations
22
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonTrajectory

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonOccupancyRegret

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.MDP.optimalAction Compiled

A finite action maximizing the one-step Bellman action value.

noncomputable def optimalAction (mdp : MDP State Action) (value : State -> Real) (state : State) : Action
Source line 27 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.bellmanQ_le_optimalAction Compiled

The selected finite action dominates every Bellman action value.

theorem bellmanQ_le_optimalAction (mdp : MDP State Action) (value : State -> Real) (state : State) (action : Action) : mdp.bellmanQ value state action <= mdp.bellmanQ value state (mdp.optimalAction value state)
Source line 34 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_optimalAction Compiled

The finite-state maximizing selector is measurable.

theorem measurable_optimalAction (mdp : MDP State Action) (value : State -> Real) : Measurable (mdp.optimalAction value)
Source line 43 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.optimalBellman Compiled

Pointwise finite-action Bellman maximum.

noncomputable def optimalBellman (mdp : MDP State Action) (value : State -> Real) (state : State) : Real
Source line 49 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.bellmanQ_le_optimalBellman Compiled

Every action value is bounded by the finite-action Bellman maximum.

theorem bellmanQ_le_optimalBellman (mdp : MDP State Action) (value : State -> Real) (state : State) (action : Action) : mdp.bellmanQ value state action <= mdp.optimalBellman value state
Source line 55 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_optimalBellman Compiled

The optimal Bellman value is measurable on the finite discrete state space.

theorem measurable_optimalBellman (mdp : MDP State Action) (value : State -> Real) : Measurable (mdp.optimalBellman value)
Source line 62 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.transitionValue_mono Compiled

Transition expectation is monotone in the continuation value.

theorem transitionValue_mono (mdp : MDP State Action) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) (action : Action) : mdp.transitionValue left state action <= mdp.transitionValue right state action
Source line 69 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.bellmanQ_mono Compiled

Bellman action values are monotone in their continuation value.

theorem bellmanQ_mono (mdp : MDP State Action) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) (action : Action) : mdp.bellmanQ left state action <= mdp.bellmanQ right state action
Source line 83 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.optimalValueRemaining Compiled

Backward optimal value indexed by the number of decisions remaining.

noncomputable def optimalValueRemaining (mdp : MDP State Action) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _ => 0 | remaining + 1, hremaining => mdp.optimalBellman (mdp.optimalValueRemaining remaining (by omega)) /-- Every backward optimal-value surface is measurable. -/ theorem measurable_optimalValueRemaining (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (mdp.optimalValueRemaining remaining hremaining)
Source line 92 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_optimalValueRemaining Compiled

Every backward optimal-value surface is measurable.

theorem measurable_optimalValueRemaining (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (mdp.optimalValueRemaining remaining hremaining)
Source line 100 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt Compiled

Optimal value at chronological stage `stage <= horizon`.

noncomputable def optimalValueAt (mdp : MDP State Action) (stage : Nat) (_hstage : stage <= mdp.horizon) : State -> Real
Source line 107 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_optimalValueAt Compiled

Every chronological optimal-value surface is measurable.

theorem measurable_optimalValueAt (mdp : MDP State Action) (stage : Nat) (hstage : stage <= mdp.horizon) : Measurable (mdp.optimalValueAt stage hstage)
Source line 112 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalValueRemaining_eq_of_eq Compiled

Transport the dependent optimal-value recursion across equal remaining horizons.

theorem optimalValueRemaining_eq_of_eq (mdp : MDP State Action) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : mdp.optimalValueRemaining left hleft = mdp.optimalValueRemaining right hright
Source line 120 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt_horizon Compiled

The optimal value is zero at the terminal stage.

theorem optimalValueAt_horizon (mdp : MDP State Action) : mdp.optimalValueAt mdp.horizon le_rfl = fun _ => 0
Source line 132 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt_bellman Compiled

Finite-action Bellman recursion for the chronological optimal value.

theorem optimalValueAt_bellman (mdp : MDP State Action) (stage : Nat) (hstage : stage < mdp.horizon) : mdp.optimalValueAt stage (Nat.le_of_lt hstage) = mdp.optimalBellman (mdp.optimalValueAt (stage + 1) (by omega))
Source line 144 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.bellman_mono Compiled

Policy Bellman expectation is monotone in the continuation value.

theorem bellman_mono {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) : policy.bellman stage left state <= policy.bellman stage right state
Source line 172 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.bellman_le_optimalBellman Compiled

Every policy Bellman expectation is bounded by the finite-action maximum.

theorem bellman_le_optimalBellman {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : policy.bellman stage value state <= mdp.optimalBellman value state
Source line 192 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueAt_le_optimalValueAt Compiled

Every Markov policy value is pointwise bounded by the optimal value.

theorem valueAt_le_optimalValueAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) (state : State) : policy.valueAt stage hstage state <= mdp.optimalValueAt stage hstage state
Source line 213 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.optimalPolicy Compiled

Greedy deterministic Markov policy for the backward optimal value.

noncomputable def optimalPolicy (mdp : MDP State Action) : MarkovPolicy mdp where
Source line 241 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalPolicy_bellman_eq_optimalBellman Compiled

One greedy-policy Bellman step is exactly the finite-action maximum.

theorem optimalPolicy_bellman_eq_optimalBellman (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) : mdp.optimalPolicy.bellman stage (mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt)) state = mdp.optimalBellman (mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt)) state
Source line 252 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalPolicy_valueAt_eq_optimalValueAt Compiled

The measurable greedy deterministic policy attains the optimal value at every stage.

theorem optimalPolicy_valueAt_eq_optimalValueAt (mdp : MDP State Action) (stage : Nat) (hstage : stage <= mdp.horizon) : mdp.optimalPolicy.valueAt stage hstage = mdp.optimalValueAt stage hstage
Source line 269 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt_dominates_and_is_attained Compiled

Route endpoint: the backward Bellman value dominates every Markov policy and is attained by the measurable greedy deterministic policy.

theorem optimalValueAt_dominates_and_is_attained (mdp : MDP State Action) : (forall (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) (state : State), policy.valueAt stage hstage state <= mdp.optimalValueAt stage hstage state) /\ (exists policy : MarkovPolicy mdp, forall (stage : Nat) (hstage : stage <= mdp.horizon), policy.valueAt stage hstage = mdp.optimalValueAt stage hstage)
Source line 298 Chapter context: Finite-horizon RL