BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterExplicitTailStartExpectedAbsoluteBound

Coefficient of a reciprocal-linear envelope for the exact scheduled realized-regret rate.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretRateLinearCoefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Real

The reciprocal-linear rate coefficient is nonnegative.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretRateLinearCoefficient_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) : 0 <= explicitPolynomialPrefixAverageRealizedBehaviorRegretRateLinearCoefficient mdp varianceProxy

The exact scheduled realized-regret rate is controlled by a reciprocal linear envelope in the fourth-power schedule scale.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretRate_le_linearEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor n <= explicitPolynomialPrefixAverageRealizedBehaviorRegretRateLinearCoefficient mdp varianceProxy / (explicitHighProbabilityScale n : Real)

Explicit checkpoint index that clears the fixed inverse-square-root threshold for every later scheduled regret-rate checkpoint.

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

The explicit ceiling witness is beyond the threshold index and validates the exact scheduled rate comparison at every later checkpoint.

theorem inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart_spec (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart mdp varianceProxy scheduleIndex /\ forall n, inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart mdp varianceProxy scheduleIndex <= n -> explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledNaturalCausalInverseSqrtFirstPassageThreshold scheduleIndex

The accepted least eventual witness is no larger than the explicit ceiling-based tail start.

theorem inverseSqrtThresholdUnboundedHittingAfterTailStart_le_explicitTailStart (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterTailStart mdp varianceProxy baseVisitFloor scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterExplicitTailStart mdp varianceProxy scheduleIndex

ENNReal second-moment budget obtained by replacing the canonical tail start with its explicit ceiling-based upper bound.

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

The explicit-start ENNReal budget is finite under the same horizon-five contract as the accepted canonical budget.

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

Real-valued form of the explicit-start stopping-round second-moment budget.

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

The checkpoint-square plus fixed weighted failure series is monotone in its deterministic checkpoint start.

theorem explicitStoppingRoundSecondMomentENNRealBudgetAt_mono (mdp : MDP State Action) {left right : Nat} (h : left <= right) : (((explicitHighProbabilityRounds left + 1) ^ 2 : Nat) : ENNReal) + ∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * explicitPolynomialPrefixTailModelReturnFailureBudget mdp n <= (((explicitHighProbabilityRounds right + 1) ^ 2 : Nat) : ENNReal) + ∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * explicitPolynomialPrefixTailModelReturnFailureBudget mdp n

Replacing the least eventual witness by the explicit tail start can only increase the deterministic ENNReal second-moment budget.

theorem inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget_le_explicit (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget mdp varianceProxy baseVisitFloor scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentENNRealBudget mdp varianceProxy scheduleIndex

Real-valued canonical second-moment budget is bounded by the explicit tail-start budget.

theorem inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentBudget_le_explicit (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) (hhorizon : 4 < mdp.horizon) : inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentBudget mdp varianceProxy baseVisitFloor scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex

The actual successor stopping-round second moment is bounded by the explicit ceiling-based deterministic budget.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_integral_stoppingRound_sq_le_explicitTailStartBudget (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) <= inverseSqrtThresholdUnboundedHittingAfterExplicitStoppingRoundSecondMomentBudget mdp varianceProxy scheduleIndex

Explicit-tail-start absolute-first-moment budget. Its public parameters contain no canonical `Nat.find` witness and no unevaluated random integral.

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

For each fixed threshold index, the exact stopped average realized behavior regret is integrable and its absolute first moment is controlled by the explicit ceiling-based deterministic second-moment budget.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_integrable_and_integral_abs_le_explicitTailStartDeterministicStoppingRoundSecondMomentBudget (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|) <= selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterExplicitTailStartDeterministicStoppingRoundSecondMomentAbsoluteFirstMomentBudget mdp varianceProxy scheduleIndex