BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardBellman

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.

Module map

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.rewardNextStateKernel

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellmanQ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.integrable_reward_add_value

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellmanQ_eq_bellmanQ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellman

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticBellman_eq_bellman

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueRemaining_eq_valueRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticValueAt_eq_valueAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.deterministic

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.meanPlanningTransport

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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