BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterL1Consistency

Exact one-step recursion for the natural round-average realized regret.

theorem naturalAverageRealizedBehaviorRegret_succ_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) : source.naturalAverageRealizedBehaviorRegret trajectory (n + 1) = ((n : Real) * source.naturalAverageRealizedBehaviorRegret trajectory n + source.naturalSuccessorBatchAverageRealizedRegret trajectory n) / ((n + 1 : Nat) : Real)

A conditional successor-average return MGF also gives its unconditional sub-Gaussian MGF on the trajectory measure.

theorem trajectoryMeasure_naturalSuccessorAverageReturnDeviationIncrement_succ_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasSubgaussianMGF (source.naturalSuccessorAverageReturnDeviationIncrement (n + 1)) (naturalSuccessorAverageReturnVarianceProxyAt mdp episodes (n + 1) rewardBound rewardVarianceProxy) source.trajectoryMeasure

A positive successor batch contributes at most one one-episode return variance proxy after normalization by its batch size.

theorem naturalSuccessorAverageReturnVarianceProxyAt_succ_le_globalReturnDeviationPerEpisodeVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (n : Nat) (rewardBound rewardVarianceProxy : NNReal) (hepisodes : 0 < episodes (n + 1)) : naturalSuccessorAverageReturnVarianceProxyAt mdp episodes (n + 1) rewardBound rewardVarianceProxy <= mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy

Uniform deterministic second-moment envelope for one successor-batch average realized-regret coordinate.

noncomputable def naturalSuccessorBatchAverageRealizedRegretSecondMomentEnvelope (mdp : MDP State Action) (rewardVarianceProxy : NNReal) : Real

Every positive-count successor-batch average realized-regret coordinate belongs to `L2`.

theorem memLp_two_naturalSuccessorBatchAverageRealizedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (n : Nat) (hepisodes : 0 < episodes (n + 1)) : MemLp (fun trajectory => source.naturalSuccessorBatchAverageRealizedRegret trajectory n) 2 source.trajectoryMeasure

The second moment of every positive-count successor-batch average realized-regret coordinate is bounded by the uniform envelope.

theorem integral_sq_naturalSuccessorBatchAverageRealizedRegret_le_secondMomentEnvelope {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (n : Nat) (hepisodes : 0 < episodes (n + 1)) : integral source.trajectoryMeasure (fun trajectory => source.naturalSuccessorBatchAverageRealizedRegret trajectory n ^ 2) <= naturalSuccessorBatchAverageRealizedRegretSecondMomentEnvelope mdp rewardVarianceProxy

If the previous average is nonnegative, one new coordinate can create at most its absolute value divided by the new sample count as negative overshoot.

theorem max_neg_natWeightedAverage_succ_le_abs_increment_div (n : Nat) (previous increment : Real) (hprevious : 0 <= previous) : max (-(((n : Real) * previous + increment) / ((n + 1 : Nat) : Real))) 0 <= |increment| / ((n + 1 : Nat) : Real)

A delayed finite `hittingAfter` has a predecessor outside the target lower interval.

theorem hittingAfter_predecessor_gt_of_untopA_gt_base {Omega : Type*} (process : Nat -> Omega -> Real) (threshold : Real) (base : Nat) (omega : Omega) (hfinite : MeasureTheory.hittingAfter process (Set.Iic threshold) base omega ≠ ⊤) (hdelayed : base < (MeasureTheory.hittingAfter process (Set.Iic threshold) base omega).untopA) : threshold < process ((MeasureTheory.hittingAfter process (Set.Iic threshold) base omega).untopA - 1) omega

Reciprocal overshoot weight, active only strictly after the scheduled base.

noncomputable def inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight (base n : Nat) : Real

At a finite first hit of a positive lower threshold, the negative part is bounded by the base absolute value plus the reciprocal-weighted final increment.

theorem max_neg_hittingAfter_untopA_le_base_abs_add_abs_stoppedValue_delayedReciprocalIncrement {Omega : Type*} (average increment : Nat -> Omega -> Real) (threshold : Real) (hthreshold : 0 < threshold) (base : Nat) (omega : Omega) (hrecursion : forall n, average (n + 1) omega = ((n : Real) * average n omega + increment n omega) / ((n + 1 : Nat) : Real)) (hfinite : MeasureTheory.hittingAfter average (Set.Iic threshold) base omega ≠ ⊤) : max (-average (MeasureTheory.hittingAfter average (Set.Iic threshold) base omega).untopA omega) 0 <= |average base omega| + |stoppedValue (fun hit trajectory => inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight base hit * increment (hit - 1) trajectory) (MeasureTheory.hittingAfter average (Set.Iic threshold) base) omega|

The square of the delayed reciprocal weight is dominated by the classical inverse-square series.

theorem summable_inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight_sq (base : Nat) : Summable (fun n => inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight base n ^ 2)

The squared reciprocal tail after a growing base tends to zero.

theorem inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight_sq_tsum_tendsto_zero : Tendsto (fun base => ∑' n : Nat, inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight base n ^ 2) atTop (nhds 0)

The square root of the squared reciprocal tail also vanishes.

theorem inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight_sq_tsum_sqrt_tendsto_zero : Tendsto (fun base => Real.sqrt (∑' n : Nat, inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight base n ^ 2)) atTop (nhds 0)

Reciprocal-weighted final successor-batch coordinate at the uncapped inverse-square-root hitting time.

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

Pathwise negative-part decomposition at a finite uncapped hit: the base absolute average pays for an immediate hit, while the reciprocal-weighted successor coordinate pays for a delayed hit.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfter_stoppedNegativePart_le_baseAbsolute_add_delayedReciprocalSuccessorRegretAbsolute (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (hfinite : selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory ≠ ⊤) : let stoppedProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) scheduleIndex max (-stoppedProcess trajectory) 0 <= |selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityRounds scheduleIndex) trajectory| + |selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalSuccessorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory|

The reciprocal-weighted final successor coordinate is integrable and its absolute first moment is controlled by the square root of the reciprocal square tail.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_delayedReciprocalSuccessorRegret_integrable_and_integral_abs_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 delayedRegret := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalSuccessorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex let mu := (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure Integrable delayedRegret mu /\ integral mu (fun trajectory => |delayedRegret trajectory|) <= Real.sqrt (HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorBatchAverageRealizedRegretSecondMomentEnvelope mdp varianceProxy) * Real.sqrt (∑' hit : Nat, inverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalWeight (explicitHighProbabilityRounds scheduleIndex) hit ^ 2)

Expected absolute reciprocal-weighted final successor coordinate.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalSuccessorRegretExpectedAbsolute (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Real

The expected absolute reciprocal-weighted overshoot coordinate vanishes as the scheduled base tends to infinity.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_delayedReciprocalSuccessorRegretExpectedAbsolute_tendsto_zero (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) : Tendsto (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedReciprocalSuccessorRegretExpectedAbsolute mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)

Expected negative part of the exact stopped average realized behavior regret.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedNegativePart (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Real

The expected negative part vanishes: immediate hits are paid by the summable base-prefix L1 term, and delayed hits by the reciprocal-weighted L2 overshoot term.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedNegativePart_tendsto_zero (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) : Tendsto (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedNegativePart mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)

The exact stopped average realized behavior regret at the uncapped inverse-square-root `hittingAfter` converges to zero in expected absolute value.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegretExpectedAbsolute_tendsto_zero (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) : Tendsto (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageRealizedBehaviorRegretExpectedAbsolute mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)