Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonMDP
# Finite-horizon MDP kernel surface This module fixes the dependency layer for the first finite-horizon RL leaf. A finite MDP uses Mathlib Markov kernels for transitions and a measurable Real reward. The only derived objects here are the one-step continuation value and Bellman action value. Policies, trajectories, value recursion, optimality, and regret remain downstream.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.FiniteHorizonRL.MDP
Compiled
A finite-state, finite-action, finite-horizon MDP backed by a Mathlib Markov transition kernel. The reward is allowed to depend on the current state and action; stochastic rewards can be added later through a separate reward kernel.
structure MDP (State : Type u) (Action : Type v) [MeasurableSpace State] [MeasurableSpace Action] [Fintype State] [Fintype Action] where
def
BanditRLProof.FiniteHorizonRL.MDP.transitionValue
Compiled
Expected continuation value after taking `action` in `state`.
noncomputable def transitionValue (mdp : MDP State Action) (value : State → Real) (state : State) (action : Action) : Real
def
BanditRLProof.FiniteHorizonRL.MDP.bellmanQ
Compiled
One-step Bellman action value `r(s,a) + E[V(S') | s,a]`.
noncomputable def bellmanQ (mdp : MDP State Action) (value : State → Real) (state : State) (action : Action) : Real
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_transitionValue
Compiled
The continuation-value surface is measurable in the state-action pair.
theorem measurable_transitionValue (mdp : MDP State Action) {value : State → Real} (hvalue : Measurable value) : Measurable (Function.uncurry (mdp.transitionValue value))
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_bellmanQ
Compiled
The one-step Bellman action value is measurable in the state-action pair.
theorem measurable_bellmanQ (mdp : MDP State Action) {value : State → Real} (hvalue : Measurable value) : Measurable (Function.uncurry (mdp.bellmanQ value))
theorem
BanditRLProof.FiniteHorizonRL.MDP.bellmanQ_zero
Compiled
With zero continuation value, the Bellman action value is the reward.
theorem bellmanQ_zero (mdp : MDP State Action) (state : State) (action : Action) : mdp.bellmanQ (fun _ => 0) state action = mdp.reward state action