Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedEventExpectedContribution
# Delayed-event contribution at the uncapped inverse-sqrt hitting time This module combines the accepted uniform-integrability interface for the exact uncapped stopped-regret process with the compiled vanishing probability of the capped first-passage delayed event. The absolute and signed expected contributions on that concrete rare event both vanish.
Module map
Imports
BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterUniformAbsoluteContinuity, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageSummableDelayAndEventualImmediateStoppingL1Consistency
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tendsto_integral_abs_restrict_of_uniformIntegrable_one_of_measure_tendsto_zero
Compiled
A uniformly integrable Real family has vanishing restricted L1 mass on a measurable sequence of events whose measures tend to zero.
theorem tendsto_integral_abs_restrict_of_uniformIntegrable_one_of_measure_tendsto_zero {Omega : Type w} [MeasurableSpace Omega] {mu : Measure Omega} {f : Nat -> Omega -> Real} {event : Nat -> Set Omega} (hui : UniformIntegrable f 1 mu) (hevent : forall n, MeasurableSet (event n)) (hmeasure : Tendsto (fun n => mu (event n)) atTop (nhds 0)) : Tendsto (fun n => integral (mu.restrict (event n)) (fun omega => |f n omega|)) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tendsto_abs_integral_restrict_of_uniformIntegrable_one_of_measure_tendsto_zero
Compiled
The signed restricted integrals also vanish, by domination with the restricted integral of the absolute value.
theorem tendsto_abs_integral_restrict_of_uniformIntegrable_one_of_measure_tendsto_zero {Omega : Type w} [MeasurableSpace Omega] {mu : Measure Omega} {f : Nat -> Omega -> Real} {event : Nat -> Set Omega} (hui : UniformIntegrable f 1 mu) (hevent : forall n, MeasurableSet (event n)) (hmeasure : Tendsto (fun n => mu (event n)) atTop (nhds 0)) : Tendsto (fun n => |integral (mu.restrict (event n)) (f n)|) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_delayedEvent_expectedContribution_tendsto_zero
Compiled
The existing inverse-square-root delayed event has vanishing expected contribution for the exact uncapped `hittingAfter` stopped average realized behavior-regret process. The event comes from the capped first-passage route, but the integrated process and stopping prefix remain genuinely uncapped.
theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_delayedEvent_expectedContribution_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) : 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 let delayedSet := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall scheduleIndex, MeasurableSet (delayedSet scheduleIndex)) /\ Tendsto (fun scheduleIndex => source.trajectoryMeasure (delayedSet scheduleIndex)) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => integral (source.trajectoryMeasure.restrict (delayedSet scheduleIndex)) (fun trajectory => |stoppedProcess scheduleIndex trajectory|)) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => |integral (source.trajectoryMeasure.restrict (delayedSet scheduleIndex)) (stoppedProcess scheduleIndex)|) atTop (nhds 0)