Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStochasticRewardCumulativeConcentration
# Finite-horizon stochastic reward cumulative concentration This module centers every sampled reward at the mean of its actual pre-step state and sampled action. A recursive kernel composition proof combines the common one-step sub-Gaussian proxy additively, yielding a total proxy linear in the remaining horizon and a fixed-horizon two-sided delta tail.
Module map
Imports
BanditRLProof.RL.FiniteHorizonStochasticRewardConcentration
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonStochasticRewardBellmanInnovationConcentration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.kernel_hasSubgaussianMGF_of_ae
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem kernel_hasSubgaussianMGF_of_ae {Alpha : Type u} {Omega : Type v} [MeasurableSpace Alpha] [MeasurableSpace Omega] (mu : Measure Alpha) [IsFiniteMeasure mu] (kernel : ProbabilityTheory.Kernel Alpha Omega) (X : Omega -> Real) (varianceProxy : NNReal) (hX : Measurable X) (hfiber : ∀ᵐ alpha ∂mu, ProbabilityTheory.HasSubgaussianMGF X varianceProxy (kernel alpha)) : ProbabilityTheory.Kernel.HasSubgaussianMGF X varianceProxy kernel mu
theorem
BanditRLProof.Concentration.hasSubgaussianMGF_apply_of_kernel_dirac
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem hasSubgaussianMGF_apply_of_kernel_dirac {Alpha : Type u} {Omega : Type v} [MeasurableSpace Alpha] [MeasurableSpace Omega] [MeasurableSingletonClass Alpha] (kernel : ProbabilityTheory.Kernel Alpha Omega) (alpha : Alpha) (X : Omega -> Real) (varianceProxy : NNReal) (hkernel : ProbabilityTheory.Kernel.HasSubgaussianMGF X varianceProxy kernel (Measure.dirac alpha)) : ProbabilityTheory.HasSubgaussianMGF X varianceProxy (kernel alpha)
def
BanditRLProof.FiniteHorizonRL.MDP.sampledCumulativeRewardDeviationFrom
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def sampledCumulativeRewardDeviationFrom (mdp : MDP State Action) : (remaining : Nat) -> State -> RewardStepTrace Action State remaining -> Real | 0, _, _ => 0 | remaining + 1, state, trace => (trace 0).2.1 - mdp.reward state (trace 0).1 + sampledCumulativeRewardDeviationFrom mdp remaining (trace 0).2.2 (Fin.tail trace) theorem measurable_sampledCumulativeRewardDeviationFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : State × RewardStepTrace Action State remaining => mdp.sampledCumulativeRewardDeviationFrom remaining p.1 p.2)
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_sampledCumulativeRewardDeviationFrom
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_sampledCumulativeRewardDeviationFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : State × RewardStepTrace Action State remaining => mdp.sampledCumulativeRewardDeviationFrom remaining p.1 p.2)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.actionRewardStateKernel_rewardDeviation_hasSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem actionRewardStateKernel_rewardDeviation_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 (fun head : Action × (Real × State) => head.2.1 - mdp.reward state head.1) varianceProxy (source.actionRewardStateKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_sampledCumulativeRewardDeviationFrom_hasSubgaussianMGF
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stochasticTrajectoryKernelRemaining_sampledCumulativeRewardDeviationFrom_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeRewardDeviationFrom remaining state) ((remaining : NNReal) * varianceProxy) (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_sampledCumulativeRewardDeviationFrom_abs_tail_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stochasticTrajectoryKernelRemaining_sampledCumulativeRewardDeviationFrom_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((remaining : NNReal) * varianceProxy : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state) {trace | Concentration.subGaussianSumConfidenceRadius ((remaining : NNReal) * varianceProxy) delta <= |mdp.sampledCumulativeRewardDeviationFrom remaining state trace|} <= ENNReal.ofReal delta