BanditRLProof.RL.FiniteHorizonStochasticRewardMarginal

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)

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

theorem measurable_head (remaining : Nat) : Measurable (head (Action := Action) (State := State) remaining)

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

def headActionReward (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Prod Action Real

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

theorem measurable_headActionReward (remaining : Nat) : Measurable (headActionReward (Action := Action) (State := State) remaining)

The first actual sampled Real reward of a positive trace.

def headReward (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Real

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

theorem measurable_headReward (remaining : Nat) : Measurable (headReward (Action := Action) (State := State) remaining)

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)

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

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 := Action) (State := State) remaining) = source.actionRewardStateKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state

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 := Action) (State := State) remaining) = source.actionRewardKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state

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 := Action) (State := State) remaining) = source.rewardMarginalKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state

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)

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)

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 := Action) (State := State) remaining) ⁻¹' (actionSet ×ˢ rewardSet)) = ∫⁻ action in actionSet, source.rewardKernel.kernel (state, action) rewardSet ∂(policy.actionKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state) ∧ (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state) ((RewardStepTrace.headReward (Action := Action) (State := State) remaining) ⁻¹' rewardSet) = ∫⁻ action, source.rewardKernel.kernel (state, action) rewardSet ∂(policy.actionKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state)