BanditRLProof.RL.FiniteHorizonStochasticRewardIIDEmpiricalRewardConfidence

A uniform fiberwise sub-Gaussian proxy survives an arbitrary probability mixture.

theorem hasSubgaussianMGF_compProd_of_forall {Index : Type u} {Omega : Type v} [MeasurableSpace Index] [MeasurableSpace Omega] (mu : Measure Index) [IsProbabilityMeasure mu] (kappa : ProbabilityTheory.Kernel Index Omega) [ProbabilityTheory.IsMarkovKernel kappa] (X : Index × Omega -> Real) (hX : Measurable X) (c : NNReal) (hfiber : forall index, ProbabilityTheory.HasSubgaussianMGF (fun omega => X (index, omega)) c (kappa index)) : ProbabilityTheory.HasSubgaussianMGF X c (mu.compProd kappa)

The zero random variable admits every nonnegative sub-Gaussian proxy.

theorem hasSubgaussianMGF_zero_of_proxy {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (c : NNReal) : ProbabilityTheory.HasSubgaussianMGF (fun _ : Omega => 0) c mu

State immediately before a reward-bearing trajectory coordinate.

def stateAt (initialState : State) {remaining : Nat} (trace : RewardStepTrace Action State remaining) (coordinate : Fin remaining) : State

The pre-coordinate state is measurable as a function of the full trace.

theorem measurable_stateAt (initialState : State) {remaining : Nat} (coordinate : Fin remaining) : Measurable (fun trace : RewardStepTrace Action State remaining => stateAt initialState trace coordinate)

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

theorem stateAt_cons_zero (initialState : State) (remaining : Nat) (head : Action × (Real × State)) (tail : RewardStepTrace Action State remaining) : stateAt initialState (@Fin.cons remaining (fun _ => Action × (Real × State)) head tail) 0 = initialState

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

theorem stateAt_cons_succ (initialState : State) (remaining : Nat) (head : Action × (Real × State)) (tail : RewardStepTrace Action State remaining) (coordinate : Fin remaining) : stateAt initialState (@Fin.cons remaining (fun _ => Action × (Real × State)) head tail) coordinate.succ = stateAt head.2.2 tail coordinate

The pre-coordinate state is measurable when the initial state is also an input.

theorem measurable_stateAt_prod {remaining : Nat} (coordinate : Fin remaining) : Measurable (fun p : State × RewardStepTrace Action State remaining => stateAt p.1 p.2 coordinate)

A sampled reward centered at one target coordinate and masked by its visit event.

def maskedRewardDeviationAt (mdp : MDP State Action) (initialState : State) {remaining : Nat} (trace : RewardStepTrace Action State remaining) (coordinate : Fin remaining) (state : State) (action : Action) : Real

A fixed visit-masked reward deviation is measurable on reward-bearing traces.

theorem measurable_maskedRewardDeviationAt (mdp : MDP State Action) (initialState : State) {remaining : Nat} (coordinate : Fin remaining) (state : State) (action : Action) : Measurable (fun trace => mdp.maskedRewardDeviationAt initialState trace coordinate state action)

The masked deviation is measurable when the initial state is part of the input.

theorem measurable_maskedRewardDeviationAt_trajectory (mdp : MDP State Action) {remaining : Nat} (coordinate : Fin remaining) (state : State) (action : Action) : Measurable (fun trajectory : State × RewardStepTrace Action State remaining => mdp.maskedRewardDeviationAt trajectory.1 trajectory.2 coordinate state action)

One sampled reward-bearing trajectory converted to an empirical record.

def sampledEpisodeStepOfStochasticTrajectory (mdp : MDP State Action) (trajectory : State × RewardStepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : EpisodeStep State Action where

Extracting a sampled empirical record from a stochastic trajectory is measurable.

theorem measurable_sampledEpisodeStepOfStochasticTrajectory (mdp : MDP State Action) (stage : Fin mdp.horizon) : Measurable (fun trajectory => mdp.sampledEpisodeStepOfStochasticTrajectory trajectory stage)

A finite iid family of stochastic trajectories mapped to sampled-reward records.

def sampledEpisodeBatchOfStochasticTrajectories (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : EpisodeBatch mdp episodes

Mapping a finite stochastic trajectory family to sampled episode records is measurable.

theorem measurable_sampledEpisodeBatchOfStochasticTrajectories (mdp : MDP State Action) (episodes : Nat) : Measurable (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes)

A visit-masked one-step reward deviation retains the common reward proxy.

theorem actionRewardStateKernel_maskedRewardDeviation_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (initialState state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (fun head : Action × (Real × State) => if initialState = state /\ head.1 = action then head.2.1 - mdp.reward state action else 0) varianceProxy (source.actionRewardStateKernel policy stage initialState)

Every coordinate of a generated reward-bearing trace has the masked reward MGF.

theorem stochasticTrajectoryKernelRemaining_maskedRewardDeviationAt_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (initialState : State) (coordinate : Fin remaining) (state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (fun trace => mdp.maskedRewardDeviationAt initialState trace coordinate state action) varianceProxy (source.stochasticTrajectoryKernelRemaining policy remaining hremaining initialState)

The same fixed coordinate MGF holds after mixing over the initial-state law.

theorem stochasticTrajectoryMeasure_maskedRewardDeviationAt_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (fun trajectory : State × RewardStepTrace Action State mdp.horizon => mdp.maskedRewardDeviationAt trajectory.1 trajectory.2 stage state action) varianceProxy (source.stochasticTrajectoryMeasure policy initialState)

One iid episode's fixed-coordinate masked reward deviation. The receiver keeps this structural coordinate on the same source-indexed API as its law theorems; the pointwise value itself depends only on the sampled trajectory and the MDP.

def maskedRewardDeviationAtEpisode (source : MeanCompatibleRewardKernel mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) {episodes : Nat} (episode : Fin episodes) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : Real

Fixed-coordinate masked reward deviations are independent across iid episodes.

theorem iIndepFun_maskedRewardDeviationAtEpisode (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.iIndepFun (source.maskedRewardDeviationAtEpisode stage state action) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

Every iid episode coordinate inherits the complete-trajectory masked reward MGF.

theorem maskedRewardDeviationAtEpisode_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) {episodes : Nat} (episode : Fin episodes) : ProbabilityTheory.HasSubgaussianMGF (source.maskedRewardDeviationAtEpisode stage state action episode) varianceProxy (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

The iid fixed-coordinate reward-deviation sum has the episode-linear proxy.

theorem iidStochasticTrajectoryFamilyMeasure_maskedRewardDeviation_sum_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (fun trajectories => ∑ episode : Fin episodes, source.maskedRewardDeviationAtEpisode stage state action episode trajectories) ((episodes : NNReal) * varianceProxy) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

Fixed-coordinate two-sided reward-sum tail under the iid stochastic family law.

theorem iidStochasticTrajectoryFamilyMeasure_maskedRewardDeviation_sum_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) {trajectories | Concentration.subGaussianSumConfidenceRadius ((episodes : NNReal) * varianceProxy) delta <= |∑ episode : Fin episodes, source.maskedRewardDeviationAtEpisode stage state action episode trajectories|} <= ENNReal.ofReal delta