BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialSecondMomentExpectedAbsoluteBound

Natural model coefficient used by the polynomial tail-start envelope.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialScaleCoefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Nat

The explicit ceiling start grows at most linearly in the schedule scale.

theorem inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart_succ_le_polynomialScale (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart mdp varianceProxy scheduleIndex + 1 <= inverseSqrtThresholdUnboundedHittingAfterPolynomialScaleCoefficient mdp varianceProxy * explicitHighProbabilityScale scheduleIndex

Explicit degree-eight natural checkpoint-square envelope.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointSquare (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Nat

The exact explicit-start checkpoint square is bounded by the polynomial envelope.

theorem inverseSqrtThresholdUnboundedHittingAfterExplicitCheckpointSquare_le_polynomial (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : (explicitHighProbabilityRounds (inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart mdp varianceProxy scheduleIndex) + 1) ^ 2 <= inverseSqrtThresholdUnboundedHittingAfterPolynomialCheckpointSquare mdp varianceProxy scheduleIndex

The weighted model/return failure contribution to the stopping-round second moment. It depends only on the MDP.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterWeightedFailureSecondMomentENNRealConstant (mdp : MDP State Action) : ENNReal

The weighted failure constant is finite under the horizon-five contract.

theorem inverseSqrtThresholdUnboundedHittingAfterWeightedFailureSecondMomentENNRealConstant_ne_top (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) : inverseSqrtThresholdUnboundedHittingAfterWeightedFailureSecondMomentENNRealConstant mdp ≠ ∞

Real-valued form of the weighted model/return failure constant.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterWeightedFailureSecondMomentConstant (mdp : MDP State Action) : Real

ENNReal polynomial stopping-round second-moment budget.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : ENNReal

The polynomial ENNReal budget is finite under the same horizon contract.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget_ne_top (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) (hhorizon : 4 < mdp.horizon) : inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget mdp varianceProxy scheduleIndex ≠ ∞

Real polynomial stopping-round second-moment budget, displayed as a degree-eight checkpoint term plus the named MDP failure constant.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Real

Taking `toReal` of the polynomial ENNReal budget gives its displayed real polynomial-plus-constant form.

theorem inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget_toReal (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) (hhorizon : 4 < mdp.horizon) : (inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget mdp varianceProxy scheduleIndex).toReal = inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex

The ceiling-start ENNReal budget is bounded by the polynomial budget.

theorem inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentENNRealBudget_le_polynomial (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentENNRealBudget mdp varianceProxy scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentENNRealBudget mdp varianceProxy scheduleIndex

The real ceiling-start second-moment budget is bounded by its displayed polynomial-plus-constant envelope.

theorem inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentBudget_le_polynomial (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) (hhorizon : 4 < mdp.horizon) : inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex

The actual successor stopping-round second moment is bounded by the polynomial-plus-model-constant budget.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_integral_stoppingRound_sq_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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let tau := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex integral source.trajectoryMeasure (fun trajectory => ((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) <= inverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex

Polynomial-envelope absolute-first-moment budget.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Real

For each fixed threshold index, the stopped average realized behavior regret has a polynomial-plus-model-constant absolute first-moment bound.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_integrable_and_integral_abs_le_polynomialStoppingRoundSecondMomentBudget (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|) <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterPolynomialStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex