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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.RewardStepTrace.headActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headActionReading 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)
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.selectedRewardKernelAtReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_eq_compProd_selectedRewardKernelAtReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_map_fstReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_headActionReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_condDistrib_reward_given_actionReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_condDistrib_headReward_given_headActionReading 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
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 identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_condExpKernel_map_headReward_given_headActionReading 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)