BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretUpperTailInProbability

# Scheduled one-sided upper-tail consistency in probability 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. The result is one-sided and only follows the deterministic fourth-power prefix subsequence. It is not absolute TendstoInMeasure, all-prefix, or anytime control.

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.

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.

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.

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.

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.

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.

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.

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.

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