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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzExpectedAbsoluteAsymptotics

# Cauchy--Schwarz degree-four expected-absolute asymptotics This module replaces the Young-inequality absolute-first-moment envelope by a Cauchy--Schwarz estimate on the stopping fibers. The actual stopping-round second moment still uses the accepted degree-eight polynomial envelope, while its square root yields a degree-four expected-absolute growth bound. All model and source parameters are fixed as the threshold index varies. The result is not optional stopping, uniform integrability, L1 convergence, or a claim that the polynomial exponent is sharp.

Module map

Declarations
10
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialSecondMomentExpectedAbsoluteAsymptotics

Imported by

BanditRLProof

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale Compiled

Real degree-four comparison scale for the threshold schedule.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale (scheduleIndex : Nat) : Real
Source line 34 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale_nonneg Compiled

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

theorem inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale_nonneg (scheduleIndex : Nat) : 0 <= inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale scheduleIndex
Source line 42 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.sqrt_inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale Compiled

The square root of the degree-eight scale is exactly the degree-four scale, with no asymptotic slack.

theorem sqrt_inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale (scheduleIndex : Nat) : Real.sqrt (inverseSqrtThresholdUnboundedHittingAfterDegreeEightScale scheduleIndex) = inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale scheduleIndex
Source line 54 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.sqrt_inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_isBigO_degreeFour Compiled

Taking square roots of the accepted degree-eight polynomial moment budget yields a degree-four asymptotic envelope.

theorem sqrt_inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget_isBigO_degreeFour (mdp : MDP State Action) (varianceProxy : NNReal) : (fun scheduleIndex : Nat => Real.sqrt (inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex)) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale
Source line 73 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget Compiled

Cauchy--Schwarz polynomial absolute-first-moment budget. Its only varying factor is the square root of the accepted stopping-round second-moment budget.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Real
Source line 92 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget_nonneg Compiled

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

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex
Source line 108 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget_isBigO_degreeFour Compiled

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

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget_isBigO_degreeFour (mdp : MDP State Action) (varianceProxy : NNReal) : (fun scheduleIndex : Nat => selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex) =O[atTop] inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale
Source line 122 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_integrable_and_integral_abs_le_cauchySchwarzPolynomialBudget Compiled

For each fixed threshold index, Cauchy--Schwarz controls the actual stopped average realized behavior regret by the square root of the accepted polynomial stopping-round second-moment budget.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_integrable_and_integral_abs_le_cauchySchwarzPolynomialBudget (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppedProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex Integrable stoppedProcess source.trajectoryMeasure /\ integral source.trajectoryMeasure (fun trajectory => |stoppedProcess trajectory|) <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex
Source line 145 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_le_cauchySchwarzPolynomialBudget Compiled

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

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_le_cauchySchwarzPolynomialBudget (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 <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterCauchySchwarzPolynomialAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex
Source line 248 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_isBigO_degreeFour Compiled

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

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_isBigO_degreeFour (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] inverseSqrtThresholdUnboundedHittingAfterDegreeFourScale
Source line 278 Chapter context: Finite-horizon RL