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.FiniteHorizonStochasticRewardConditionalLaw

This module identifies the selected reward kernel as the conditional law of the first sampled reward given the first sampled action. The result is first proved for the one-step action/reward marginal, then transported to every positive generated stochastic trajectory and to the corresponding trimmed condExpKernel.map surface.

Module map

Declarations
9
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonStochasticRewardMarginal, BanditRLProof.ConditionalExpectationReward

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardConcentration

Declarations

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

def BanditRLProof.FiniteHorizonRL.RewardStepTrace.headAction Compiled

The first sampled action of a positive reward-bearing trace.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.RewardStepTrace.headAction

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

def headAction (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Action
Source line 30 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headAction Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headAction

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

theorem measurable_headAction (remaining : Nat) : Measurable (headAction (Action := Action) (State := State) remaining)
Source line 35 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.selectedRewardKernelAt Compiled

The reward kernel selected after freezing the current state.

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

9. Finite-horizon reinforcement learning

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

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

noncomputable def selectedRewardKernelAt (source : MeanCompatibleRewardKernel mdp) (state : State) : ProbabilityTheory.Kernel Action Real
Source line 46 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_eq_compProd_selectedRewardKernelAt Compiled

The one-step action/reward marginal is the policy law composed with the selected reward law.

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

9. Finite-horizon reinforcement learning

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

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

theorem actionRewardKernel_eq_compProd_selectedRewardKernelAt (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) : source.actionRewardKernel policy stage state = policy.actionKernel stage state ⊗ₘ source.selectedRewardKernelAt state
Source line 59 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_map_fst Compiled

The action marginal of the one-step action/reward law is the policy action law.

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

9. Finite-horizon reinforcement learning

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

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

theorem actionRewardKernel_map_fst (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) : (source.actionRewardKernel policy stage state).map Prod.fst = policy.actionKernel stage state
Source line 73 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_headAction Compiled

Mapping a generated trace to its first action recovers the policy action law.

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

9. Finite-horizon reinforcement learning

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

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

theorem stochasticTrajectoryKernelRemaining_map_headAction (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).map (RewardStepTrace.headAction (Action := Action) (State := State) remaining) = policy.actionKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state
Source line 86 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_condDistrib_reward_given_action Compiled

Under the one-step joint law, reward conditioned on action is the selected reward kernel.

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

9. Finite-horizon reinforcement learning

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

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

theorem actionRewardKernel_condDistrib_reward_given_action (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) : ProbabilityTheory.condDistrib Prod.snd Prod.fst (source.actionRewardKernel policy stage state) =ᵐ[ (source.actionRewardKernel policy stage state).map Prod.fst] source.selectedRewardKernelAt state
Source line 115 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_condDistrib_headReward_given_headAction Compiled

On a generated positive trace, reward conditioned on the sampled head action has its selected law.

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

9. Finite-horizon reinforcement learning

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

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

theorem stochasticTrajectoryKernelRemaining_condDistrib_headReward_given_headAction (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : ProbabilityTheory.condDistrib (RewardStepTrace.headReward (Action := Action) (State := State) remaining) (RewardStepTrace.headAction (Action := Action) (State := State) remaining) (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state) =ᵐ[ (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).map (RewardStepTrace.headAction (Action := Action) (State := State) remaining)] source.selectedRewardKernelAt state
Source line 136 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_condExpKernel_map_headReward_given_headAction Compiled

The generated head conditional law on `Real` is also the mapped conditional expectation kernel on the sigma-algebra generated by the sampled head action.

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

9. Finite-horizon reinforcement learning

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

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

theorem stochasticTrajectoryKernelRemaining_condExpKernel_map_headReward_given_headAction [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : ∀ᵐ trace ∂ (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).trim (RewardStepTrace.measurable_headAction remaining).comap_le, Measure.map (RewardStepTrace.headReward (Action := Action) (State := State) remaining) (ProbabilityTheory.condExpKernel (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state) (MeasurableSpace.comap (RewardStepTrace.headAction (Action := Action) (State := State) remaining) inferInstance) trace) = source.selectedRewardKernelAt state (RewardStepTrace.headAction (Action := Action) (State := State) remaining trace)
Source line 179 Chapter context: Finite-horizon RL