BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterSquareIntegrableFiniteStoppingTime

Seventh-degree envelope for one consecutive squared fourth-power checkpoint block.

def explicitHighProbabilityQuarticSquareBlockWeight (n : Nat) : Nat

A consecutive squared fourth-power checkpoint gap is bounded by the seventh-degree weight.

theorem explicitHighProbabilityRounds_succ_square_sub_le_quarticSquareBlockWeight (n : Nat) : (explicitHighProbabilityRounds (n + 1) + 1) ^ 2 - (explicitHighProbabilityRounds n + 1) ^ 2 <= explicitHighProbabilityQuarticSquareBlockWeight n

Horizon at least five makes every local confidence share no larger than a shifted inverse tenth power.

theorem selfConsistentScheduledLocalDelta_le_inv_pow_ten (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) (t : Nat) : AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp t <= 1 / (((t + 2 : Nat) : Real) ^ 10)

Inverse-cube pair envelope after a seventh-degree weight cancels seven inverse powers.

noncomputable def quarticSquareBlockShiftedInverseCubePairEnvelope (p : Nat × Nat) : ENNReal

The square-block shifted pair envelope has finite total ENNReal mass.

theorem tsum_quarticSquareBlockShiftedInverseCubePairEnvelope_ne_top : Ne (∑' p : Nat × Nat, quarticSquareBlockShiftedInverseCubePairEnvelope p) ∞

One squared-checkpoint block weight times one shifted coordinate model-failure charge.

noncomputable def quarticSquareBlockShiftedCoordinateModelFailureCharge (mdp : MDP State Action) (p : Nat × Nat) : ENNReal

The inverse-tenth local share puts every seventh-weighted coordinate charge below the pair envelope.

theorem quarticSquareBlockShiftedCoordinateModelFailureCharge_le_pairEnvelope (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) (p : Nat × Nat) : quarticSquareBlockShiftedCoordinateModelFailureCharge mdp p <= quarticSquareBlockShiftedInverseCubePairEnvelope p

The seventh-weighted shifted coordinate charges have finite total ENNReal mass.

theorem tsum_quarticSquareBlockShiftedCoordinateModelFailureCharge_ne_top (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) : Ne (∑' p : Nat × Nat, quarticSquareBlockShiftedCoordinateModelFailureCharge mdp p) ∞

A model tail after `n+1`, charged by one squared-checkpoint block, is the shifted coordinate row.

theorem quarticSquareBlockWeight_mul_tailModelFailureBudget_eq_tsum_shiftedCoordinateCharge (mdp : MDP State Action) (n : Nat) : (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * selfConsistentScheduledCausalTailModelFailureBudget mdp (n + 1) = ∑' j : Nat, quarticSquareBlockShiftedCoordinateModelFailureCharge mdp (n, j)

Squared-checkpoint block weights are summable against the exact infinite model-tail budgets.

theorem tsum_quarticSquareBlockWeight_mul_tailModelFailureBudget_ne_top (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) : Ne (∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * selfConsistentScheduledCausalTailModelFailureBudget mdp (n + 1)) ∞

A seventh-degree squared-checkpoint weight times the exponential return share is summable.

theorem summable_quarticSquareBlockWeight_mul_explicitHighProbabilityReturnDelta : Summable (fun n : Nat => ((explicitHighProbabilityQuarticSquareBlockWeight n : Nat) : Real) * explicitHighProbabilityReturnDelta n)

The exact return shares have finite total mass after squared-checkpoint charging.

theorem tsum_quarticSquareBlockWeight_mul_explicitHighProbabilityReturnDelta_ne_top : Ne (∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * ENNReal.ofReal (explicitHighProbabilityReturnDelta n)) ∞

The exact checkpoint violation budgets remain summable after squared-checkpoint charging.

theorem tsum_quarticSquareBlockWeight_mul_explicitPolynomialPrefixTailModelReturnFailureBudget_ne_top (mdp : MDP State Action) (hhorizon : 4 < mdp.horizon) : Ne (∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * explicitPolynomialPrefixTailModelReturnFailureBudget mdp n) ∞

Seventh-degree weights dominate every finite telescope of squared checkpoint values.

theorem explicitHighProbabilityRounds_add_square_le_add_sum_Ico_quarticSquareBlockWeight (start width : Nat) : (explicitHighProbabilityRounds (start + width) + 1) ^ 2 <= (explicitHighProbabilityRounds start + 1) ^ 2 + (Finset.Ico start (start + width)).sum explicitHighProbabilityQuarticSquareBlockWeight

The square of a finite natural time is paid for by an initial squared checkpoint plus preceding delayed blocks.

theorem natCast_succ_square_le_checkpoint_square_add_tsum_quarticSquareBlockWeight_of_delayed (start time : Nat) : (((time + 1) ^ 2 : Nat) : ENNReal) <= (((explicitHighProbabilityRounds start + 1) ^ 2 : Nat) : ENNReal) + ∑' n : Nat, if start <= n ∧ explicitHighProbabilityRounds n < time then (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) else 0

A deterministic checkpoint after which the scheduled regret envelope is below the fixed inverse-square-root first-passage threshold.

theorem exists_inverseSqrtThresholdUnboundedHittingAfterTailStart (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : ∃ start : Nat, scheduleIndex <= start ∧ ∀ n, start <= n -> explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledNaturalCausalInverseSqrtFirstPassageThreshold scheduleIndex

Canonical deterministic witness for the eventual delayed-checkpoint tail bound at a fixed inverse-square-root threshold index.

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

The canonical tail start is beyond the threshold index and validates the scheduled regret-rate comparison at every later checkpoint.

theorem inverseSqrtThresholdUnboundedHittingAfterTailStart_spec (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : scheduleIndex <= inverseSqrtThresholdUnboundedHittingAfterTailStart mdp varianceProxy baseVisitFloor scheduleIndex ∧ ∀ n, inverseSqrtThresholdUnboundedHittingAfterTailStart mdp varianceProxy baseVisitFloor scheduleIndex <= n -> explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledNaturalCausalInverseSqrtFirstPassageThreshold scheduleIndex

Explicit deterministic ENNReal budget for the second moment of the successor round count at the uncapped inverse-square-root hitting time.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : ENNReal

The deterministic stopping-round second-moment budget is finite whenever the horizon supplies the inverse-tenth confidence exponent.

theorem inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget_ne_top (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) (hhorizon : 4 < mdp.horizon) : inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget mdp varianceProxy baseVisitFloor scheduleIndex ≠ ∞

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

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

A pointwise delayed-checkpoint tail budget gives an explicit ENNReal upper bound for the successor stopping-round second moment.

theorem lintegral_sq_untopA_add_one_le_quarticSquareCheckpointBudget {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (budget : Nat -> ENNReal) (start : Nat) (htailStart : ∀ n, start <= n -> mu {omega | (explicitHighProbabilityRounds n : WithTop Nat) < tau omega} <= budget n) : ∫⁻ omega, ENNReal.ofReal (((((tau omega).untopA + 1 : Nat) : Real)) ^ 2) ∂mu <= (((explicitHighProbabilityRounds start + 1) ^ 2 : Nat) : ENNReal) + ∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * budget n

Eventually summable squared fourth-power checkpoint crossing tails imply a finite second moment.

theorem memLp_two_untopA_add_one_of_eventually_quarticSquareCheckpointTail {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (budget : Nat -> ENNReal) (hbudget : Ne (∑' n : Nat, (explicitHighProbabilityQuarticSquareBlockWeight n : ENNReal) * budget n) ∞) (htail : ∀ᶠ n : Nat in atTop, mu {omega | (explicitHighProbabilityRounds n : WithTop Nat) < tau omega} <= budget n) : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu

From the canonical tail start onward, every delayed uncapped first-passage checkpoint has the exact compiled model/return failure budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_inverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet_le_of_tailStart (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) (scheduleIndex checkpointIndex : Nat) (hcheckpointIndex : inverseSqrtThresholdUnboundedHittingAfterTailStart mdp varianceProxy baseVisitFloor scheduleIndex <= checkpointIndex) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex checkpointIndex) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp checkpointIndex

The actual successor stopping-round square has an explicit deterministic ENNReal upper bound at every fixed inverse-square-root threshold index.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_lintegral_stoppingRound_sq_le_ENNRealBudget (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) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let tau := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex ∫⁻ trajectory, ENNReal.ofReal (((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) ∂source.trajectoryMeasure <= inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentENNRealBudget mdp varianceProxy baseVisitFloor scheduleIndex

Each fixed-index genuine uncapped inverse-square-root first passage has a finite second moment when the finite-horizon confidence exponent is at least ten.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_squareIntegrableFiniteStoppingTime (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 BanditRLProof.OFUL.SquareIntegrableFiniteStoppingTime source.trajectoryMeasure (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex)

The Bochner second moment of the actual successor stopping-round count is bounded by the canonical deterministic checkpoint/failure budget.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_integral_stoppingRound_sq_le_budget (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) <= inverseSqrtThresholdUnboundedHittingAfterStoppingRoundSecondMomentBudget mdp varianceProxy baseVisitFloor scheduleIndex