Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterUniformAbsoluteContinuity
# Uniform absolute continuity at the uncapped inverse-sqrt hitting time This module consumes the accepted probability-theory uniform-integrability interface. Uniformly over the exact stopped-process schedule index, sufficiently small measurable trajectory events have small absolute stopped-regret integrals. This is an epsilon-delta consequence of uniform integrability, not an optional-stopping or quantitative tail theorem.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterDelayedEventExpectedContribution
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integral_abs_restrict_le_of_uniformIntegrable_one
Compiled
Probability-theory uniform integrability at exponent one gives uniform absolute continuity of the expected norm over measurable events. This is a thin real-valued wrapper around Mathlib's `UnifIntegrable` epsilon-delta interface.
theorem integral_abs_restrict_le_of_uniformIntegrable_one {Omega : Type w} [MeasurableSpace Omega] {mu : Measure Omega} {f : Nat -> Omega -> Real} (hui : UniformIntegrable f 1 mu) : forall epsilon : Real, 0 < epsilon -> exists delta : Real, 0 < delta /\ forall i event, MeasurableSet event -> mu event <= ENNReal.ofReal delta -> integral (mu.restrict event) (fun omega => |f i omega|) <= epsilon
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_uniformAbsoluteContinuity
Compiled
Uniform absolute continuity of the exact uncapped stopped average realized behavior-regret family. One delta works for every schedule index and controls both the absolute signed set integral and the set integral of the absolute stopped regret.
theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_uniformAbsoluteContinuity (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 forall epsilon : Real, 0 < epsilon -> exists delta : Real, 0 < delta /\ forall scheduleIndex event, MeasurableSet event -> source.trajectoryMeasure event <= ENNReal.ofReal delta -> |integral (source.trajectoryMeasure.restrict event) (stoppedProcess scheduleIndex)| <= epsilon /\ integral (source.trajectoryMeasure.restrict event) (fun trajectory => |stoppedProcess scheduleIndex trajectory|) <= epsilon