BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretUpperTailInProbability

This module consumes the explicit fourth-power prefix high-probability terminal. For every fixed positive threshold, the deterministic regret envelope is eventually below that threshold, so the threshold violation is contained in the compiled envelope violation and inherits its vanishing exact failure budget.

Module map

Declarations
8
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityExplicitSchedule

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretInMeasureExplicitSchedule

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet Compiled

Fixed-threshold upper-tail event for the scheduled average realized regret.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 34 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability Compiled

Trajectory probability of the fixed-threshold scheduled upper tail.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : ENNReal
Source line 53 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet Compiled

Every fixed-threshold scheduled upper-tail event is measurable.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : MeasurableSet (explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n)
Source line 69 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet_subset_violationSet Compiled

Once the deterministic envelope is below a positive fixed threshold, the fixed-threshold upper tail is contained in the compiled envelope violation.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet_subset_violationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet_subset_violationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (hepsilon : 0 < epsilon) : ∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n ⊆ explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n
Source line 92 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet_le Compiled

Direct projection of the compiled scheduled violation probability bound.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n
Source line 124 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_le_failureBudget Compiled

Eventually every fixed positive upper tail is bounded by the exact budget.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_le_failureBudget

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_le_failureBudget (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (epsilon : Real) (hepsilon : 0 < epsilon) : ∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n
Source line 157 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_tendsto_zero Compiled

The fixed-positive-threshold scheduled upper-tail probability vanishes.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_tendsto_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (epsilon : Real) (hepsilon : 0 < epsilon) : Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon) atTop (nhds 0)
Source line 192 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailInProbability Compiled

All fixed positive one-sided upper-tail probabilities vanish on the same explicit fourth-power prefix subsequence.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailInProbability

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailInProbability (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : forall epsilon, 0 < epsilon -> (forall n, MeasurableSet (explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n)) /\ (∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n ⊆ explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n /\ explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n) /\ Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretUpperTailProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon) atTop (nhds 0)
Source line 225 Chapter context: Finite-horizon RL