Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterUniformAbsoluteContinuity
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integral_abs_restrict_le_of_uniformIntegrable_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_uniformAbsoluteContinuityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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