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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialSecondMomentExpectedAbsoluteAsymptotics

# Degree-eight asymptotics for the uncapped inverse-sqrt hitting time This module transports the explicit polynomial moment envelope to the actual stopping-round second moment and stopped-regret expected absolute value. All model and source parameters are fixed while the threshold index varies. The resulting `IsBigO` statements are growth bounds. They do not establish uniform integrability, L1 convergence, or an optional-stopping identity.

Module map

Declarations
25
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialSecondMomentExpectedAbsoluteBound

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzExpectedAbsoluteAsymptotics, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterL1Consistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale Compiled

Real degree-eight comparison scale for the threshold schedule.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale (scheduleIndex : Nat) : Real
Source line 32 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale_nonneg (scheduleIndex : Nat) : 0 <= inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale scheduleIndex
Source line 40 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale_one_le Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale_one_le (scheduleIndex : Nat) : 1 <= inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale scheduleIndex
Source line 50 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointAsymptoticCoefficient Compiled

Fixed natural coefficient for the degree-eight checkpoint envelope.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointAsymptoticCoefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Nat
Source line 60 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointSquare_le_asymptoticCoefficient_mul_scale_pow_eight Compiled

The explicit checkpoint polynomial is bounded by one fixed coefficient times the degree-eight scale.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointSquare_le_asymptoticCoefficient_mul_scale_pow_eight (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointSquare mdp varianceProxy scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointAsymptoticCoefficient mdp varianceProxy * explicitHighProbabilityScale scheduleIndex ^ 8
Source line 71 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient Compiled

Fixed real coefficient for the polynomial stopping-round second-moment budget.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Real
Source line 108 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) : 0 <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient mdp varianceProxy
Source line 119 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_le_asymptoticCoefficient_mul_degreeEightScale Compiled

Pointwise degree-eight bound for the real deterministic moment budget.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_le_asymptoticCoefficient_mul_degreeEightScale (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAsymptoticCoefficient mdp varianceProxy * inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale scheduleIndex
Source line 134 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : 0 <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex
Source line 219 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_isBigO_degreeEight Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_isBigO_degreeEight (mdp : MDP State Action) (varianceProxy : NNReal) : (fun scheduleIndex : Nat => inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale
Source line 234 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment Compiled

Actual successor stopping-round second moment as a function of the threshold schedule index.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Real
Source line 260 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex
Source line 277 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppingRoundSecondMoment_le_polynomialBudget Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppingRoundSecondMoment_le_polynomialBudget (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex
Source line 295 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_integral_stoppingRound_sq_isBigO_degreeEight Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_integral_stoppingRound_sq_isBigO_degreeEight (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale
Source line 323 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterShiftedInverseSquareSeriesConstant Compiled

Universal shifted inverse-square series appearing in the stopped-value absolute-first-moment bridge.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterShiftedInverseSquareSeriesConstant : Real
Source line 363 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterShiftedInverseSquareSeriesConstant_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverseSqrtThresholdUnboundedHittingAfterShiftedInverseSquareSeriesConstant_nonneg : 0 <= inverseSqrtThresholdUnboundedHittingAfterShiftedInverseSquareSeriesConstant
Source line 371 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient Compiled

Fixed coefficient for the polynomial absolute-first-moment budget.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Real
Source line 379 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) : 0 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient mdp varianceProxy
Source line 393 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_le_asymptoticCoefficient_mul_degreeEightScale Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_le_asymptoticCoefficient_mul_degreeEightScale (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialAbsoluteFirstMomentAsymptoticCoefficient mdp varianceProxy * inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale scheduleIndex
Source line 411 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex
Source line 515 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_isBigO_degreeEight Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget_isBigO_degreeEight (mdp : MDP State Action) (varianceProxy : NNReal) : (fun scheduleIndex : Nat => selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale
Source line 542 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute Compiled

Expected absolute stopped average realized behavior regret as a function of the threshold schedule index.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Real
Source line 568 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute_nonneg Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex
Source line 589 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_le_polynomialBudget Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_le_polynomialBudget (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex
Source line 607 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_isBigO_degreeEight Compiled

With all model/source parameters fixed, the actual expected absolute stopped regret grows at most at the compiled degree-eight rate.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_isBigO_degreeEight (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale
Source line 637 Chapter context: Finite-horizon RL