Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStochasticRewardConditionalLaw
# Finite-horizon stochastic reward trajectory head conditional law 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
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.
def headAction (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Action
theorem
BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headAction
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_headAction (remaining : Nat) : Measurable (headAction (Action
def
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.selectedRewardKernelAt
Compiled
The reward kernel selected after freezing the current state.
noncomputable def selectedRewardKernelAt (source : MeanCompatibleRewardKernel mdp) (state : State) : ProbabilityTheory.Kernel Action Real
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.
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
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_map_fst
Compiled
The action marginal of the one-step action/reward law is the policy action law.
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
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_headAction
Compiled
Mapping a generated trace to its first action recovers the policy action law.
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
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.
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
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.
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
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.
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