Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardBellman

# Stochastic reward kernels preserve finite-horizon mean planning This module extends the finite-horizon MDP planning surface with a separate Real reward kernel. The compatibility contract says that every selected reward is integrable and has the deterministic `mdp.reward` field as its mean. The product with the transition kernel models conditional independence of the reward and next state given the current state-action pair. The resulting one-step, policy, and backward stochastic Bellman values equal the existing mean-reward definitions. This is a planning transport theorem; it does not construct a stochastic-reward trajectory law or a concentration bound.

Module map

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

Imports

BanditRLProof.RL.FiniteHorizonTrajectory, BanditRLProof.RewardKernel

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardTrajectory

Declarations

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

structure BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel Compiled

A stochastic Real reward kernel whose selected rewards are integrable and have the mean stored in the finite-horizon MDP reward field.

structure MeanCompatibleRewardKernel (mdp : MDP State Action) where

Source line 39 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.rewardNextStateKernel Compiled

The conditionally independent joint law of reward and next state.

noncomputable def rewardNextStateKernel (source : MeanCompatibleRewardKernel mdp) : ProbabilityTheory.Kernel (Prod State Action) (Prod Real State)

Source line 54 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellmanQ Compiled

Expected sampled reward plus continuation value under the joint kernel.

noncomputable def stochasticBellmanQ (source : MeanCompatibleRewardKernel mdp) (value : State -> Real) (state : State) (action : Action) : Real

Source line 66 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integrable_reward_add_value Compiled

The sampled one-step return is integrable for measurable continuation values.

theorem integrable_reward_add_value (source : MeanCompatibleRewardKernel mdp) {value : State -> Real} (hvalue : Measurable value) (state : State) (action : Action) : Integrable (fun pair : Prod Real State => pair.1 + value pair.2) (source.rewardNextStateKernel (state, action))

Source line 73 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellmanQ_eq_bellmanQ Compiled

Sampling a mean-compatible reward preserves the existing Bellman action value.

theorem stochasticBellmanQ_eq_bellmanQ (source : MeanCompatibleRewardKernel mdp) {value : State -> Real} (hvalue : Measurable value) (state : State) (action : Action) : source.stochasticBellmanQ value state action = mdp.bellmanQ value state action

Source line 92 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellman Compiled

Policy expectation formed from the sampled stochastic Bellman action value.

noncomputable def stochasticBellman (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : Real

Source line 126 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellman_eq_bellman Compiled

The stochastic policy Bellman operator equals the existing mean operator.

theorem stochasticBellman_eq_bellman (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) {value : State -> Real} (hvalue : Measurable value) : source.stochasticBellman policy stage value = policy.bellman stage value

Source line 134 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueRemaining Compiled

Backward policy value computed with sampled stochastic reward laws.

noncomputable def stochasticValueRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _ => 0 | remaining + 1, hremaining => source.stochasticBellman policy ⟨mdp.horizon - (remaining + 1), by omega⟩ (source.stochasticValueRemaining policy remaining (by omega)) /-- Stochastic backward policy evaluation equals mean-reward evaluation. -/ theorem stochasticValueRemaining_eq_valueRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : source.stochasticValueRemaining policy remaining hremaining = policy.valueRemaining remaining hremaining

Source line 147 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueRemaining_eq_valueRemaining Compiled

Stochastic backward policy evaluation equals mean-reward evaluation.

theorem stochasticValueRemaining_eq_valueRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : source.stochasticValueRemaining policy remaining hremaining = policy.valueRemaining remaining hremaining

Source line 158 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueAt Compiled

Stochastic policy value at a chronological stage.

noncomputable def stochasticValueAt (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Nat) (_hstage : stage <= mdp.horizon) : State -> Real

Source line 176 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueAt_eq_valueAt Compiled

Every chronological stochastic value equals the existing policy value.

theorem stochasticValueAt_eq_valueAt (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) : source.stochasticValueAt policy stage hstage = policy.valueAt stage hstage

Source line 184 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.deterministic Compiled

The deterministic MDP reward, viewed as a kernel, is mean-compatible.

noncomputable def deterministic (mdp : MDP State Action) : MeanCompatibleRewardKernel mdp where

Source line 193 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.meanPlanningTransport Compiled

Terminal mean-planning transport: the product kernel is Markov and all sampled Bellman and backward values agree with the existing deterministic-mean model.

theorem meanPlanningTransport (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) : ProbabilityTheory.IsMarkovKernel source.rewardNextStateKernel ∧ (forall (value : State -> Real), Measurable value -> forall state action, source.stochasticBellmanQ value state action = mdp.bellmanQ value state action) ∧ (forall (stage : Fin mdp.horizon) (value : State -> Real), Measurable value -> source.stochasticBellman policy stage value = policy.bellman stage value) ∧ (forall (remaining : Nat) (hremaining : remaining <= mdp.horizon), source.stochasticValueRemaining policy remaining hremaining = policy.valueRemaining remaining hremaining) ∧ (forall (stage : Nat) (hstage : stage <= mdp.horizon), source.stochasticValueAt policy stage hstage = policy.valueAt stage hstage)

Source line 213 Chapter context: Finite-horizon RL