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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardTrajectory

# Finite-horizon stochastic reward trajectory value identity This module generates finite policy trajectories whose coordinates retain the sampled action, sampled Real reward, and next state. Selected rewards need only the `L1` mean-compatibility contract from the stochastic Bellman layer. The cumulative sampled reward is proved integrable recursively and its expectation is identified with both stochastic and mean policy evaluation.

Module map

Declarations
15
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonStochasticRewardBellman

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardMarginal

Declarations

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

abbrev BanditRLProof.FiniteHorizonRL.RewardStepTrace Compiled

A finite trace of sampled action, reward, and resulting next state.

abbrev RewardStepTrace (Action : Type v) (State : Type u) (n : Nat)
Source line 26 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_cons Compiled

Prepending a sampled action-reward-state coordinate is measurable.

theorem measurable_cons (n : Nat) : Measurable (fun p : Prod (Prod Action (Prod Real State)) (RewardStepTrace Action State n) => @Fin.cons n (fun _ => Prod Action (Prod Real State)) p.1 p.2)
Source line 33 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_tail Compiled

Removing the first sampled coordinate is measurable.

theorem measurable_tail (n : Nat) : Measurable (fun trace : RewardStepTrace Action State (n + 1) => Fin.tail trace)
Source line 45 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.integrable_of_fintype_aestronglyMeasurable Compiled

An a.e. strongly measurable Real function on a finite type is integrable.

theorem integrable_of_fintype_aestronglyMeasurable {Omega : Type*} [Fintype Omega] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf : AEStronglyMeasurable f mu) : Integrable f mu
Source line 55 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardStateKernel Compiled

One policy action followed by its sampled reward and next state.

noncomputable def actionRewardStateKernel (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (Prod Action (Prod Real State))
Source line 72 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining Compiled

Kernel of the next `remaining` sampled action-reward-state coordinates. The first chronological stage is `mdp.horizon - remaining`.

noncomputable def stochasticTrajectoryKernelRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> ProbabilityTheory.Kernel State (RewardStepTrace 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 (Prod Real State))) (RewardStepTrace Action State remaining)
Source line 92 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.sampledCumulativeRewardFrom Compiled

Sum of the actual sampled rewards in a reward-bearing finite trace.

def sampledCumulativeRewardFrom : (remaining : Nat) -> RewardStepTrace Action State remaining -> Real | 0, _ => 0 | remaining + 1, trace => (trace 0).2.1 + sampledCumulativeRewardFrom remaining (Fin.tail trace) omit [Fintype State] [Fintype Action] in /-- The sampled finite cumulative reward is measurable. -/ theorem measurable_sampledCumulativeRewardFrom (remaining : Nat) : Measurable (sampledCumulativeRewardFrom (Action
Source line 134 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_sampledCumulativeRewardFrom Compiled

The sampled finite cumulative reward is measurable.

theorem measurable_sampledCumulativeRewardFrom (remaining : Nat) : Measurable (sampledCumulativeRewardFrom (Action
Source line 142 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integrable_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining Compiled

The sampled cumulative reward is `L1` under every statewise stochastic trajectory law. No boundedness or second-moment hypothesis is used.

theorem integrable_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Integrable (MDP.sampledCumulativeRewardFrom (Action
Source line 165 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integral_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining_eq_stochasticValueRemaining Compiled

Statewise stochastic trajectory identity: expected sampled cumulative reward equals the independently defined stochastic backward policy value.

theorem integral_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining_eq_stochasticValueRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : integral (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state) (MDP.sampledCumulativeRewardFrom (Action
Source line 312 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryMeasure Compiled

Full reward-bearing trajectory law, including the initial state.

noncomputable def stochasticTrajectoryMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) : Measure (Prod State (RewardStepTrace Action State mdp.horizon))
Source line 400 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.sampledCumulativeReward Compiled

Sampled cumulative reward on the full stochastic trajectory.

def sampledCumulativeReward (trajectory : Prod State (RewardStepTrace Action State mdp.horizon)) : Real
Source line 416 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.measurable_sampledCumulativeReward Compiled

The full sampled cumulative reward is measurable.

theorem measurable_sampledCumulativeReward : Measurable (sampledCumulativeReward (mdp
Source line 421 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integrable_sampledCumulativeReward_stochasticTrajectoryMeasure Compiled

The full sampled cumulative reward is integrable under its generated law.

theorem integrable_sampledCumulativeReward_stochasticTrajectoryMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : Integrable (sampledCumulativeReward (mdp
Source line 426 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integral_sampledCumulativeReward_stochasticTrajectoryMeasure_eq_integral_valueAt_zero Compiled

Route endpoint: expected sampled cumulative reward equals the stochastic and existing mean policy values at chronological stage zero.

theorem integral_sampledCumulativeReward_stochasticTrajectoryMeasure_eq_integral_valueAt_zero (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : integral (source.stochasticTrajectoryMeasure policy initialState) (sampledCumulativeReward (mdp
Source line 455 Chapter context: Finite-horizon RL