BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardMarginal

# Finite-horizon stochastic reward trajectory head marginals This module identifies the first generated stochastic-reward coordinate at every positive recursive horizon. It exposes the exact action/reward joint law and reward-only policy mixture needed before adding conditional-law or concentration assumptions.

Module map

Declarations
14
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonStochasticRewardTrajectory

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardConditionalLaw

Declarations

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

def BanditRLProof.FiniteHorizonRL.RewardStepTrace.head Compiled

The first sampled action, reward, and next state of a positive trace.

def head (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Prod Action (Prod Real State)
Source line 27 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_head Compiled

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

theorem measurable_head (remaining : Nat) : Measurable (head (Action
Source line 33 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.RewardStepTrace.headActionReward Compiled

The first sampled action/reward pair, with next state discarded.

def headActionReward (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Prod Action Real
Source line 39 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headActionReward Compiled

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

theorem measurable_headActionReward (remaining : Nat) : Measurable (headActionReward (Action
Source line 44 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.RewardStepTrace.headReward Compiled

The first actual sampled Real reward of a positive trace.

def headReward (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Real
Source line 53 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_headReward Compiled

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

theorem measurable_headReward (remaining : Nat) : Measurable (headReward (Action
Source line 58 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel Compiled

The action/reward marginal of one generated stochastic MDP step.

noncomputable def actionRewardKernel (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (Prod Action Real)
Source line 69 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.rewardMarginalKernel Compiled

The reward-only marginal after mixing the selected laws over policy actions.

noncomputable def rewardMarginalKernel (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State Real
Source line 86 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_head Compiled

The first generated coordinate has exactly the compiled one-step law.

theorem stochasticTrajectoryKernelRemaining_map_head (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).map (RewardStepTrace.head (Action
Source line 102 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_headActionReward Compiled

Mapping a generated trace to its first action/reward pair gives the joint marginal.

theorem stochasticTrajectoryKernelRemaining_map_headActionReward (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).map (RewardStepTrace.headActionReward (Action
Source line 124 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_headReward Compiled

Mapping a generated trace to its first reward gives the policy reward mixture.

theorem stochasticTrajectoryKernelRemaining_map_headReward (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state).map (RewardStepTrace.headReward (Action
Source line 157 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardKernel_apply_prod Compiled

Exact action/reward rectangle law for a policy-mixed stochastic step.

theorem actionRewardKernel_apply_prod (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) {actionSet : Set Action} {rewardSet : Set Real} (hactionSet : MeasurableSet actionSet) (hrewardSet : MeasurableSet rewardSet) : source.actionRewardKernel policy stage state (actionSet ×ˢ rewardSet) = ∫⁻ action in actionSet, source.rewardKernel.kernel (state, action) rewardSet ∂(policy.actionKernel stage state)
Source line 187 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.rewardMarginalKernel_apply Compiled

Reward-event probability is the selected reward law mixed over policy actions.

theorem rewardMarginalKernel_apply (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) {rewardSet : Set Real} (hrewardSet : MeasurableSet rewardSet) : source.rewardMarginalKernel policy stage state rewardSet = ∫⁻ action, source.rewardKernel.kernel (state, action) rewardSet ∂(policy.actionKernel stage state)
Source line 217 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headMarginalFactorization Compiled

Route endpoint: the generated first reward event has the exact randomized policy mixture law, while the joint action/reward rectangle retains the selected-law factorization.

theorem stochasticTrajectoryKernelRemaining_headMarginalFactorization (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) {actionSet : Set Action} {rewardSet : Set Real} (hactionSet : MeasurableSet actionSet) (hrewardSet : MeasurableSet rewardSet) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state) ((RewardStepTrace.headActionReward (Action
Source line 243 Chapter context: Finite-horizon RL