Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStochasticRewardInitialLawTotalReturnConcentration
# Initial-law finite-horizon sampled-return concentration This module lifts the statewise sampled-return concentration theorem to the full stochastic trajectory measure generated from a finite initial-state law. The random variable remains centered by the recursive value of its own initial state; no concentration claim is made for mixing those state-dependent values.
Module map
Imports
BanditRLProof.RL.FiniteHorizonStochasticRewardTotalReturnConcentration
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardIIDEmpiricalRewardConfidence, BanditRLProof.RL.FiniteHorizonStochasticRewardIIDTotalReturnConcentration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.hasSubgaussianMGF_compProd_of_forall_fintype
Compiled
A common sub-Gaussian proxy on every fiber of a Markov kernel is preserved by mixing the fibers with a probability measure on a finite index type.
theorem hasSubgaussianMGF_compProd_of_forall_fintype {Index Omega : Type*} [MeasurableSpace Index] [MeasurableSpace Omega] [Fintype Index] (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)
def
BanditRLProof.FiniteHorizonRL.MDP.sampledCumulativeReturnDeviation
Compiled
Sampled cumulative return centered by the policy value at the trajectory's own initial state.
noncomputable def sampledCumulativeReturnDeviation (mdp : MDP State Action) (policy : MarkovPolicy mdp) (trajectory : State × RewardStepTrace Action State mdp.horizon) : Real
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_sampledCumulativeReturnDeviation
Compiled
The full initial-state-dependent sampled-return deviation is measurable.
theorem measurable_sampledCumulativeReturnDeviation (mdp : MDP State Action) (policy : MarkovPolicy mdp) : Measurable (mdp.sampledCumulativeReturnDeviation policy)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryMeasure_sampledCumulativeReturnDeviation_hasSubgaussianMGF
Compiled
Initial-law sampled-return MGF bound. The centering is state dependent, so the common statewise proxy passes unchanged through the finite initial-state mix.
theorem stochasticTrajectoryMeasure_sampledCumulativeReturnDeviation_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) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeReturnDeviation policy) ((mdp.horizon : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound mdp.horizon) (source.stochasticTrajectoryMeasure policy initialState)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryMeasure_sampledCumulativeReturnDeviation_abs_tail_le
Compiled
Fixed-horizon two-sided delta tail under an arbitrary finite initial-state law.
theorem stochasticTrajectoryMeasure_sampledCumulativeReturnDeviation_abs_tail_le [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) (htotal : 0 < ((((mdp.horizon : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound mdp.horizon : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.stochasticTrajectoryMeasure policy initialState) {trajectory | Concentration.subGaussianSumConfidenceRadius ((mdp.horizon : NNReal) * rewardVarianceProxy + meanBellmanInnovationVarianceProxy rewardBound mdp.horizon) delta <= |mdp.sampledCumulativeReturnDeviation policy trajectory|} <= ENNReal.ofReal delta