BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterIntegrableFiniteStoppingTime

Cubic envelope for the width of one consecutive fourth-power checkpoint block.

def explicitHighProbabilityQuarticBlockWeight (n : Nat) : Nat

A consecutive fourth-power checkpoint gap is bounded by the cubic block weight.

theorem explicitHighProbabilityRounds_succ_sub_le_quarticBlockWeight (n : Nat) : explicitHighProbabilityRounds (n + 1) - explicitHighProbabilityRounds n <= explicitHighProbabilityQuarticBlockWeight n

Positive horizon makes every local confidence share no larger than a shifted inverse sixth power.

theorem selfConsistentScheduledLocalDelta_le_inv_pow_six (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (t : Nat) : AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp t <= 1 / (((t + 2 : Nat) : Real) ^ 6)

Shifted inverse-cube envelope used after the cubic block width cancels three powers.

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

The shifted inverse-cube envelope is summable over checkpoint/tail-offset pairs.

theorem tsum_quarticBlockShiftedInverseCubePairEnvelope_ne_top : Ne (∑' p : Nat × Nat, quarticBlockShiftedInverseCubePairEnvelope p) ∞

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

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

Positive horizon makes the actual weighted coordinate charge fit the inverse-cube pair envelope.

theorem quarticBlockShiftedCoordinateModelFailureCharge_le_pairEnvelope (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (p : Nat × Nat) : quarticBlockShiftedCoordinateModelFailureCharge mdp p <= quarticBlockShiftedInverseCubePairEnvelope p

The actual weighted shifted coordinate charges have finite total ENNReal mass.

theorem tsum_quarticBlockShiftedCoordinateModelFailureCharge_ne_top (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) : Ne (∑' p : Nat × Nat, quarticBlockShiftedCoordinateModelFailureCharge mdp p) ∞

A model tail after `n+1`, charged by one quartic block weight, is the shifted coordinate row.

theorem quarticBlockWeight_mul_tailModelFailureBudget_eq_tsum_shiftedCoordinateCharge (mdp : MDP State Action) (n : Nat) : (explicitHighProbabilityQuarticBlockWeight n : ENNReal) * selfConsistentScheduledCausalTailModelFailureBudget mdp (n + 1) = ∑' j : Nat, quarticBlockShiftedCoordinateModelFailureCharge mdp (n, j)

The fourth-power block weights are summable against the exact infinite model-tail budgets.

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

A cubic fourth-power block weight times the explicit exponential return share is summable.

theorem summable_quarticBlockWeight_mul_explicitHighProbabilityReturnDelta : Summable (fun n : Nat => ((explicitHighProbabilityQuarticBlockWeight n : Nat) : Real) * explicitHighProbabilityReturnDelta n)

The exact exponential return shares have finite total mass after quartic block charging.

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

The exact checkpoint violation budgets remain summable after paying every quartic block width.

theorem tsum_quarticBlockWeight_mul_explicitPolynomialPrefixTailModelReturnFailureBudget_ne_top (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) : Ne (∑' n : Nat, (explicitHighProbabilityQuarticBlockWeight n : ENNReal) * explicitPolynomialPrefixTailModelReturnFailureBudget mdp n) ∞

Cubic block weights dominate every finite telescope of the fourth-power checkpoint grid.

theorem explicitHighProbabilityRounds_add_le_add_sum_Ico_quarticBlockWeight (start width : Nat) : explicitHighProbabilityRounds (start + width) <= explicitHighProbabilityRounds start + (Finset.Ico start (start + width)).sum explicitHighProbabilityQuarticBlockWeight

A finite natural time is paid for by an initial checkpoint plus all preceding delayed blocks.

theorem natCast_succ_le_checkpoint_add_tsum_quarticBlockWeight_of_delayed (start time : Nat) : (time + 1 : ENNReal) <= (explicitHighProbabilityRounds start + 1 : ENNReal) + ∑' n : Nat, if start <= n ∧ explicitHighProbabilityRounds n < time then (explicitHighProbabilityQuarticBlockWeight n : ENNReal) else 0

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

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

Checkpoint trajectories whose fixed-index uncapped first passage has not yet occurred.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex checkpointIndex : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))

Every fixed delayed-checkpoint event is measurable.

theorem measurableSet_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex checkpointIndex : Nat) : MeasurableSet (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex checkpointIndex)

Once a checkpoint lies beyond the fixed base and its deterministic rate is below the fixed threshold, every delayed first passage violates the compiled checkpoint regret bound.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet_subset_explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) {scheduleIndex checkpointIndex : Nat} (hindex : scheduleIndex <= checkpointIndex) (hrate : explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor checkpointIndex <= selfConsistentScheduledNaturalCausalInverseSqrtFirstPassageThreshold scheduleIndex) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex checkpointIndex ⊆ explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor checkpointIndex

For each fixed threshold index, checkpoint crossing tails are eventually bounded by the explicit summable burn-in-tail/model-return budget.

theorem eventually_selfConsistentScheduledCausalSource_trajectoryMeasure_inverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet_le (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 ∀ᶠ checkpointIndex in atTop, source.trajectoryMeasure (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedCheckpointSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex checkpointIndex) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp checkpointIndex

Each fixed-index genuine uncapped inverse-square-root first passage is finite almost surely and has an integrable random horizon.

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