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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardIIDTotalReturnConcentration

# IID finite-horizon stochastic sampled-return concentration This module takes finite products of complete reward-bearing trajectories. Independence is only asserted across episodes. Each episode deviation remains centered by the policy value at that trajectory's own sampled initial state.

Module map

Declarations
11
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonStochasticRewardInitialLawTotalReturnConcentration

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardTotalReturnConcentration, BanditRLProof.RL.FiniteHorizonStochasticRewardErasureLaw

Declarations

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

def BanditRLProof.FiniteHorizonRL.MDP.sampledCumulativeReturnDeviationAtEpisode Compiled

The sampled-return deviation in one coordinate of a finite episode family.

noncomputable def sampledCumulativeReturnDeviationAtEpisode (mdp : MDP State Action) (policy : MarkovPolicy mdp) {episodes : Nat} (episode : Fin episodes) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : Real
Source line 28 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_sampledCumulativeReturnDeviationAtEpisode Compiled

One episode-coordinate deviation is measurable on the finite product space.

theorem measurable_sampledCumulativeReturnDeviationAtEpisode (mdp : MDP State Action) (policy : MarkovPolicy mdp) {episodes : Nat} (episode : Fin episodes) : Measurable (mdp.sampledCumulativeReturnDeviationAtEpisode policy episode)
Source line 36 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.sampledCumulativeReturnDeviationSum Compiled

Sum of sampled-return deviations over complete iid episode coordinates.

noncomputable def sampledCumulativeReturnDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : Real
Source line 44 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_sampledCumulativeReturnDeviationSum Compiled

The finite-episode deviation sum is measurable.

theorem measurable_sampledCumulativeReturnDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (episodes : Nat) : Measurable (mdp.sampledCumulativeReturnDeviationSum policy episodes)
Source line 53 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.iidSampledCumulativeReturnDeviationVarianceProxy Compiled

Episode-linear variance proxy for the iid sampled-return deviation sum.

noncomputable def iidSampledCumulativeReturnDeviationVarianceProxy (mdp : MDP State Action) (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal
Source line 61 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure Compiled

Finite iid product of the complete reward-bearing stochastic trajectory law.

noncomputable def iidStochasticTrajectoryFamilyMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : Measure (Fin episodes -> State × RewardStepTrace Action State mdp.horizon)
Source line 76 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure_map_eval Compiled

Every iid product coordinate has the exact complete stochastic trajectory law.

theorem iidStochasticTrajectoryFamilyMeasure_map_eval (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes).map (Function.eval episode) = source.stochasticTrajectoryMeasure policy initialState
Source line 96 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iIndepFun_sampledCumulativeReturnDeviationAtEpisode Compiled

Complete sampled-return deviations are independent across iid episodes.

theorem iIndepFun_sampledCumulativeReturnDeviationAtEpisode (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.sampledCumulativeReturnDeviationAtEpisode policy episode trajectories) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)
Source line 111 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.sampledCumulativeReturnDeviationAtEpisode_hasSubgaussianMGF Compiled

Each iid episode coordinate inherits the compiled initial-law MGF.

theorem sampledCumulativeReturnDeviationAtEpisode_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) {episodes : Nat} (episode : Fin episodes) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeReturnDeviationAtEpisode policy episode) ((mdp.horizon : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound mdp.horizon) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)
Source line 126 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure_sampledCumulativeReturnDeviationSum_hasSubgaussianMGF Compiled

The finite iid episode deviation sum has the episode-linear proxy.

theorem iidStochasticTrajectoryFamilyMeasure_sampledCumulativeReturnDeviationSum_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeReturnDeviationSum policy episodes) (mdp.iidSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)
Source line 160 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure_sampledCumulativeReturnDeviationSum_abs_tail_le Compiled

Fixed-sample two-sided delta tail for the iid episode deviation sum.

theorem iidStochasticTrajectoryFamilyMeasure_sampledCumulativeReturnDeviationSum_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((mdp.iidSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) {trajectories | Concentration.subGaussianSumConfidenceRadius (mdp.iidSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy) delta <= |mdp.sampledCumulativeReturnDeviationSum policy episodes trajectories|} <= ENNReal.ofReal delta
Source line 193 Chapter context: Finite-horizon RL