Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStochasticRewardConcentration
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.headRewardMeanReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardMeanReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardMean_comap_headActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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 := Action) (State := State) remaining) inferInstance) inferInstance (mdp.headRewardMean state remaining)
def
BanditRLProof.FiniteHorizonRL.MDP.headRewardDeviation
Compiled
Actual first sampled reward centered by the mean of its selected action law.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.headRewardDeviationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.measurable_headRewardDeviationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.UniformSubgaussianRewardLawReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.uniformSubgaussianRewardLaw_of_mem_IccReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_hasCondSubgaussianMGFReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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 := Action) (State := State) remaining) inferInstance) (RewardStepTrace.measurable_headAction remaining).comap_le (mdp.headRewardDeviation state remaining) varianceProxy (source.stochasticTrajectoryKernelRemaining policy (remaining + 1) hremaining state)
theorem
BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_hasSubgaussianMGF
Compiled
The conditional head deviation law also gives its unconditional sub-Gaussian MGF.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_hasSubgaussianMGFReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_headRewardDeviation_abs_tail_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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