Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStochasticRewardConcentration
# Finite-horizon stochastic reward head concentration This module transports a selected reward-kernel sub-Gaussian law through the compiled generated-head conditional distribution. It exposes the centered head reward as a conditional and unconditional sub-Gaussian random variable, then specializes the existing finite-sum concentration route to a one-step two-sided tail.
Module map
Imports
BanditRLProof.RL.FiniteHorizonStochasticRewardConditionalLaw, BanditRLProof.ConcentrationSubGaussian
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardCumulativeConcentration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.MDP.headRewardMean
Compiled
The selected mean reward at the first coordinate of a positive trace.
def headRewardMean (mdp : MDP State Action) (state : State) (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Real
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardMean
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_headRewardMean (mdp : MDP State Action) (state : State) (remaining : Nat) : Measurable (mdp.headRewardMean state remaining)
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardMean_comap_headAction
Compiled
The selected head mean is measurable in the sigma-algebra generated by the head action.
theorem measurable_headRewardMean_comap_headAction (mdp : MDP State Action) (state : State) (remaining : Nat) : @Measurable (RewardStepTrace Action State (remaining + 1)) Real (MeasurableSpace.comap (RewardStepTrace.headAction (Action
def
BanditRLProof.FiniteHorizonRL.MDP.headRewardDeviation
Compiled
Actual first sampled reward centered by the mean of its selected action law.
def headRewardDeviation (mdp : MDP State Action) (state : State) (remaining : Nat) : RewardStepTrace Action State (remaining + 1) -> Real
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardDeviation
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_headRewardDeviation (mdp : MDP State Action) (state : State) (remaining : Nat) : Measurable (mdp.headRewardDeviation state remaining)
structure
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.UniformSubgaussianRewardLaw
Compiled
Every selected reward law is sub-Gaussian around its stored MDP mean with one common proxy.
structure UniformSubgaussianRewardLaw (source : MeanCompatibleRewardKernel mdp) (varianceProxy : NNReal) : Prop where
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.uniformSubgaussianRewardLaw_of_mem_Icc
Compiled
A common selected-reward interval constructs a uniform Hoeffding proxy.
theorem uniformSubgaussianRewardLaw_of_mem_Icc (source : MeanCompatibleRewardKernel mdp) (lo hi : Real) (hbound : forall state action, ∀ᵐ reward ∂ source.rewardKernel.kernel (state, action), reward ∈ Set.Icc lo hi) : source.UniformSubgaussianRewardLaw (Concentration.intervalVarianceProxy lo hi)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_hasCondSubgaussianMGF
Compiled
The first generated reward deviation is conditionally sub-Gaussian given its sampled action.
theorem stochasticTrajectoryKernelRemaining_headRewardDeviation_hasCondSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasCondSubgaussianMGF (MeasurableSpace.comap (RewardStepTrace.headAction (Action
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_hasSubgaussianMGF
Compiled
The conditional head deviation law also gives its unconditional sub-Gaussian MGF.
theorem stochasticTrajectoryKernelRemaining_headRewardDeviation_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (mdp.headRewardDeviation state remaining) varianceProxy (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_abs_tail_le
Compiled
One-step two-sided delta tail for the generated head reward deviation.
theorem stochasticTrajectoryKernelRemaining_headRewardDeviation_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (hvariance : 0 < (varianceProxy : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state) {trace | Concentration.subGaussianSumConfidenceRadius varianceProxy delta <= |mdp.headRewardDeviation state remaining trace|} <= ENNReal.ofReal delta