Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonTrajectory

# Finite-horizon policy trajectory value identity This module constructs the genuine finite trajectory generated by a Markov policy. A trace with `n` decisions records the sampled action and resulting next state at each coordinate. The recursive trajectory kernel is then used to identify expected cumulative reward with the backward policy value.

Module map

Source: BanditRLProof/RL/FiniteHorizonTrajectory.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 15
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonPolicy

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonOptimality, BanditRLProof.RL.FiniteHorizonStochasticRewardBellman

Declarations

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

abbrev BanditRLProof.FiniteHorizonRL.StepTrace Compiled

The finite sequence of sampled actions and their resulting next states.

abbrev StepTrace (Action : Type v) (State : Type u) (n : Nat)

Source line 25 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.StepTrace.measurable_cons Compiled

Prepending one action-state step is measurable for the product Pi-space.

theorem measurable_cons (n : Nat) : Measurable (fun p : Prod (Prod Action State) (StepTrace Action State n) => @Fin.cons n (fun _ => Prod Action State) p.1 p.2)

Source line 32 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.StepTrace.measurable_tail Compiled

Removing the first action-state step is measurable.

theorem measurable_tail (n : Nat) : Measurable (fun trace : StepTrace Action State (n + 1) => Fin.tail trace)

Source line 43 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.integrable_of_fintype Compiled

A measurable Real function on a finite type is integrable under every finite measure.

theorem integrable_of_fintype {Omega : Type*} [Fintype Omega] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf : Measurable f) : Integrable f mu

Source line 53 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.actionStateKernel Compiled

One chronological policy step, retaining both the action and next state.

noncomputable def actionStateKernel {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (Prod Action State)

Source line 67 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryKernelRemaining Compiled

Kernel of the next `remaining` action-state steps. Its first chronological stage is `mdp.horizon - remaining`.

noncomputable def trajectoryKernelRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> ProbabilityTheory.Kernel State (StepTrace Action State remaining) | 0, _ => ProbabilityTheory.Kernel.deterministic (fun _ => fun i => Fin.elim0 i) measurable_const | remaining + 1, hremaining => let stage : Fin mdp.horizon := ⟨mdp.horizon - (remaining + 1), by omega⟩ let tailKernel : ProbabilityTheory.Kernel (Prod State (Prod Action State)) (StepTrace Action State remaining)

Source line 85 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.cumulativeRewardFrom Compiled

Total reward of a finite trace, starting from the supplied current state.

def cumulativeRewardFrom (mdp : MDP State Action) : (remaining : Nat) -> State -> StepTrace Action State remaining -> Real | 0, _, _ => 0 | remaining + 1, state, trace => mdp.reward state (trace 0).1 + mdp.cumulativeRewardFrom remaining (trace 0).2 (Fin.tail trace) /-- The finite cumulative reward is measurable jointly in its initial state and trace. -/ theorem measurable_cumulativeRewardFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : Prod State (StepTrace Action State remaining) => mdp.cumulativeRewardFrom remaining p.1 p.2)

Source line 125 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_cumulativeRewardFrom Compiled

The finite cumulative reward is measurable jointly in its initial state and trace.

theorem measurable_cumulativeRewardFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : Prod State (StepTrace Action State remaining) => mdp.cumulativeRewardFrom remaining p.1 p.2)

Source line 133 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integrable_cumulativeRewardFrom_trajectoryKernelRemaining Compiled

Every statewise finite-trace cumulative reward is integrable under its trajectory law.

theorem integrable_cumulativeRewardFrom_trajectoryKernelRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Integrable (mdp.cumulativeRewardFrom remaining state) (policy.trajectoryKernelRemaining remaining hremaining state)

Source line 157 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_cumulativeRewardFrom_trajectoryKernelRemaining_eq_valueRemaining Compiled

Statewise policy-evaluation identity: integrating the finite generated return over the remaining trajectory gives the backward policy value.

theorem integral_cumulativeRewardFrom_trajectoryKernelRemaining_eq_valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : (∫ trace, mdp.cumulativeRewardFrom remaining state trace ∂policy.trajectoryKernelRemaining remaining hremaining state) = policy.valueRemaining remaining hremaining state

Source line 171 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryMeasure Compiled

Joint law of the initial state and all finite action-state steps.

noncomputable def trajectoryMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) : Measure (Prod State (StepTrace Action State mdp.horizon))

Source line 263 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.cumulativeReward Compiled

Cumulative reward on the full finite policy trajectory.

def cumulativeReward (mdp : MDP State Action) (trajectory : Prod State (StepTrace Action State mdp.horizon)) : Real

Source line 282 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_cumulativeReward Compiled

The full finite-trajectory cumulative reward is measurable.

theorem measurable_cumulativeReward (mdp : MDP State Action) : Measurable mdp.cumulativeReward

Source line 287 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integrable_cumulativeReward_trajectoryMeasure Compiled

The cumulative reward is automatically integrable under the finite trajectory law.

theorem integrable_cumulativeReward_trajectoryMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : Integrable mdp.cumulativeReward (policy.trajectoryMeasure initialState)

Source line 296 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_cumulativeReward_trajectoryMeasure_eq_integral_valueAt_zero Compiled

Route endpoint: expected cumulative reward under the generated finite policy trajectory equals the initial-state expectation of the stage-zero policy value.

theorem integral_cumulativeReward_trajectoryMeasure_eq_integral_valueAt_zero {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : (∫ trajectory, mdp.cumulativeReward trajectory ∂policy.trajectoryMeasure initialState) = ∫ state, policy.valueAt 0 (Nat.zero_le mdp.horizon) state ∂initialState

Source line 307 Chapter context: Finite-horizon RL