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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonPolicy

# Finite-horizon Markov policy evaluation This module defines a Markov action kernel at every valid decision stage of a finite-horizon MDP. It constructs the induced next-state kernel, the policy Bellman operator, and the backward finite-horizon policy value. The terminal and Bellman recursion theorems are policy-evaluation facts; no maximization, optimality, occupancy, or regret statement is made here.

Module map

Declarations
11
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonMDP

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonTrajectory

Declarations

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

structure BanditRLProof.FiniteHorizonRL.MarkovPolicy Compiled

A Markov action kernel for every decision stage before `mdp.horizon`.

structure MarkovPolicy (mdp : MDP State Action) where
Source line 27 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.inducedStateKernel Compiled

State transition kernel induced by sampling the policy action and then the MDP transition.

noncomputable def inducedStateKernel {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State State
Source line 42 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.bellman Compiled

Bellman expectation under one stage of the supplied Markov policy.

noncomputable def bellman {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : Real
Source line 57 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_bellman Compiled

A measurable continuation value gives a measurable policy Bellman value.

theorem measurable_bellman {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) {value : State -> Real} (hvalue : Measurable value) : Measurable (policy.bellman stage value)
Source line 65 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueRemaining Compiled

Backward policy value indexed by the number of decisions remaining. The first kernel used at `remaining` is chronological stage `horizon - remaining`.

noncomputable def valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _ => 0 | remaining + 1, hremaining => policy.bellman ⟨mdp.horizon - (remaining + 1), by omega⟩ (policy.valueRemaining remaining (by omega)) /-- The backward policy value is measurable for every valid remaining horizon. -/ theorem measurable_valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (policy.valueRemaining remaining hremaining)
Source line 77 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_valueRemaining Compiled

The backward policy value is measurable for every valid remaining horizon.

theorem measurable_valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (policy.valueRemaining remaining hremaining)
Source line 87 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueAt Compiled

Policy value at a chronological stage `stage <= horizon`.

noncomputable def valueAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Nat) (_hstage : stage <= mdp.horizon) : State -> Real
Source line 99 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_valueAt Compiled

Every chronological policy-value surface is measurable.

theorem measurable_valueAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) : Measurable (policy.valueAt stage hstage)
Source line 105 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueRemaining_eq_of_eq Compiled

Transport `valueRemaining` across equality of the remaining horizon.

theorem valueRemaining_eq_of_eq {mdp : MDP State Action} (policy : MarkovPolicy mdp) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : policy.valueRemaining left hleft = policy.valueRemaining right hright
Source line 112 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueAt_horizon Compiled

The finite-horizon policy value is zero at the terminal stage.

theorem valueAt_horizon {mdp : MDP State Action} (policy : MarkovPolicy mdp) : policy.valueAt mdp.horizon le_rfl = fun _ => 0
Source line 123 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueAt_bellman Compiled

Finite-horizon policy evaluation satisfies the Bellman recursion at every decision stage.

theorem valueAt_bellman {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage < mdp.horizon) : policy.valueAt stage (Nat.le_of_lt hstage) = policy.bellman ⟨stage, hstage⟩ (policy.valueAt (stage + 1) (by omega))
Source line 138 Chapter context: Finite-horizon RL