BanditRLProof.RL.FiniteHorizonStochasticRewardTotalReturnConcentration

Sampling from `kappa` and then from a kernel that ignores the sampled value is the same as sampling from the product kernel at the original input.

theorem compProd_prodMkRight_eq_prod (kappa : Kernel Alpha Beta) (eta : Kernel Alpha Gamma) [IsFiniteKernel kappa] [IsFiniteKernel eta] : kappa ⊗ₖ prodMkRight Beta eta = kappa ×ₖ eta

Push a first-coordinate-dependent map through the second stage of `compProd`.

theorem map_compProd_prodMk {Delta : Type*} [MeasurableSpace Delta] (kappa : Kernel Alpha Beta) (eta : Kernel (Alpha × Beta) Gamma) (eta' : Kernel (Alpha × Beta) Delta) [IsSFiniteKernel kappa] [IsSFiniteKernel eta] [IsSFiniteKernel eta'] (g : Beta -> Gamma -> Delta) (hg : Measurable g.uncurry) (hmap : forall a b, (eta (a, b)).map (g b) = eta' (a, b)) : (kappa ⊗ₖ eta).map (fun p => (p.1, g p.1 p.2)) = kappa ⊗ₖ eta'

Retain the current state together with one sampled action/next-state pair.

noncomputable def retainedActionStateKernel {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (State × (Action × State))

Actual sampled cumulative return centered at the recursive policy value.

noncomputable def sampledCumulativeReturnDeviationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (trace : RewardStepTrace Action State remaining) : Real

The sampled-return deviation is jointly measurable in start state and trace.

theorem measurable_sampledCumulativeReturnDeviationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (fun p : State × RewardStepTrace Action State remaining => mdp.sampledCumulativeReturnDeviationFrom policy remaining hremaining p.1 p.2)

The centered sampled return splits pathwise into selected-reward noise and the mean Bellman innovation. No probabilistic independence is used in this identity.

theorem sampledCumulativeReturnDeviationFrom_eq_rewardDeviation_add_meanBellmanInnovation (mdp : MDP State Action) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (trace : RewardStepTrace Action State remaining) : mdp.sampledCumulativeReturnDeviationFrom policy remaining hremaining state trace = mdp.sampledCumulativeRewardDeviationFrom remaining state trace + mdp.sampledCumulativeMeanBellmanInnovationFrom policy remaining hremaining state trace

Center a sampled reward using the retained state/action coordinates.

def rewardDeviationAfterActionState (mdp : MDP State Action) : ((State × (Action × State)) × Real) -> Real

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

theorem measurable_rewardDeviationAfterActionState (mdp : MDP State Action) : Measurable (rewardDeviationAfterActionState mdp)

Raw reward sampled from the retained current-state/action coordinates.

noncomputable def rawRewardKernelAfterActionState (source : MeanCompatibleRewardKernel mdp) : ProbabilityTheory.Kernel (State × (Action × State)) Real

Reward residual sampled after retaining the current state and an already sampled action/next-state pair.

noncomputable def rewardDeviationKernelAfterActionState (source : MeanCompatibleRewardKernel mdp) : ProbabilityTheory.Kernel (State × (Action × State)) Real

Pointwise law of the retained-state centered reward kernel.

theorem rewardDeviationKernelAfterActionState_apply (source : MeanCompatibleRewardKernel mdp) (p : State × (Action × State)) : source.rewardDeviationKernelAfterActionState p = (source.rewardKernel.kernel (p.1, p.2.1)).map (fun reward => reward - mdp.reward p.1 p.2.1)

The retained-state reward residual kernel inherits the uniform reward MGF.

theorem rewardDeviationKernelAfterActionState_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (base : Measure (State × (Action × State))) [IsFiniteMeasure base] : ProbabilityTheory.Kernel.HasSubgaussianMGF id varianceProxy source.rewardDeviationKernelAfterActionState base

Ignore the outer duplicated state and sample the raw retained-coordinate reward.

noncomputable def rawRewardKernelAfterRetainedActionState (source : MeanCompatibleRewardKernel mdp) : ProbabilityTheory.Kernel (State × (State × (Action × State))) Real

Ignore the outer duplicated state and sample the centered reward residual.

noncomputable def rewardDeviationKernelAfterRetainedActionState (source : MeanCompatibleRewardKernel mdp) : ProbabilityTheory.Kernel (State × (State × (Action × State))) Real

Add the retained MDP mean back to a centered reward residual.

def uncenterRewardAfterRetainedActionState (mdp : MDP State Action) : State × (Action × State) -> Real -> Real

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

theorem measurable_uncenterRewardAfterRetainedActionState (mdp : MDP State Action) : Measurable (uncenterRewardAfterRetainedActionState mdp).uncurry

Centering and then restoring the retained MDP mean recovers the raw reward law.

theorem rewardDeviationKernelAfterRetainedActionState_map_uncenter (source : MeanCompatibleRewardKernel mdp) (outer : State) (retained : State × (Action × State)) : (source.rewardDeviationKernelAfterRetainedActionState (outer, retained)).map (uncenterRewardAfterRetainedActionState mdp retained) = source.rawRewardKernelAfterRetainedActionState (outer, retained)

Restore raw rewards throughout the retained action-state product kernel.

theorem retainedActionStateKernel_compProd_rewardDeviation_map_uncenter (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ((policy.retainedActionStateKernel stage) ⊗ₖ source.rewardDeviationKernelAfterRetainedActionState).map (fun p => (p.1, uncenterRewardAfterRetainedActionState mdp p.1 p.2)) = (policy.retainedActionStateKernel stage) ⊗ₖ source.rawRewardKernelAfterRetainedActionState

Arrange retained current/action/next-state coordinates with a raw reward.

def assembleRawRewardAfterRetainedActionState : ((State × (Action × State)) × Real) -> Action × (Real × State)

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

theorem measurable_assembleRawRewardAfterRetainedActionState : Measurable (assembleRawRewardAfterRetainedActionState (State := State) (Action := Action))

The retained raw-reward construction is exactly the existing head kernel.

theorem retainedActionStateKernel_compProd_rawReward_map_assemble (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ((policy.retainedActionStateKernel stage) ⊗ₖ source.rawRewardKernelAfterRetainedActionState).map (assembleRawRewardAfterRetainedActionState (State := State) (Action := Action)) = source.actionRewardStateKernel policy stage

Assemble a reward-bearing head directly from a centered residual.

def assembleRewardDeviationAfterRetainedActionState (mdp : MDP State Action) : ((State × (Action × State)) × Real) -> Action × (Real × State)

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

theorem measurable_assembleRewardDeviationAfterRetainedActionState (mdp : MDP State Action) : Measurable (assembleRewardDeviationAfterRetainedActionState mdp)

The centered residual construction maps exactly to the existing head kernel.

theorem retainedActionStateKernel_compProd_rewardDeviation_map_assemble (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ((policy.retainedActionStateKernel stage) ⊗ₖ source.rewardDeviationKernelAfterRetainedActionState).map (assembleRewardDeviationAfterRetainedActionState mdp) = source.actionRewardStateKernel policy stage

Retaining the current state preserves the one-step Bellman innovation MGF.

theorem retainedActionStateKernel_meanBellmanInnovation_hasSubgaussianMGF (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (fun retained : State × (Action × State) => mdp.reward retained.1 retained.2.1 + policy.valueRemaining remaining (by omega) retained.2.2 - policy.valueRemaining (remaining + 1) hremaining state) (meanBellmanInnovationStepVarianceProxy rewardBound (remaining + 1)) (policy.retainedActionStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state)

One sampled reward plus the sampled next policy value is sub-Gaussian around the current policy value with the sum of reward and Bellman innovation proxies.

theorem actionRewardStateKernel_sampledReturnBellmanInnovation_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (fun head : Action × (Real × State) => head.2.1 + policy.valueRemaining remaining (by omega) head.2.2 - policy.valueRemaining (remaining + 1) hremaining state) (meanBellmanInnovationStepVarianceProxy rewardBound (remaining + 1) + rewardVarianceProxy) (source.actionRewardStateKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state)

The full sampled return is sub-Gaussian around the recursive policy value, with the reward-noise proxy plus the mean Bellman innovation proxy.

theorem stochasticTrajectoryKernelRemaining_sampledCumulativeReturnDeviationFrom_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeReturnDeviationFrom policy remaining hremaining state) ((remaining : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound remaining) (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state)

Fixed-horizon two-sided delta tail for sampled return around policy value.

theorem stochasticTrajectoryKernelRemaining_sampledCumulativeReturnDeviationFrom_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (htotal : 0 < ((((remaining : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound remaining : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state) {trace | Concentration.subGaussianSumConfidenceRadius ((remaining : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound remaining) delta <= |mdp.sampledCumulativeReturnDeviationFrom policy remaining hremaining state trace|} <= ENNReal.ofReal delta