BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegret

Semantic finiteness and first-moment regularity for a `WithTop Nat` stopping time. The a.e. finiteness field rules out interpreting `untopA` at `top`; the integrability field controls the random all-round gap envelope.

structure IntegrableFiniteStoppingTime {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) (tau : Omega -> WithTop Nat) : Prop where

A stopped pseudo-regret obeys the gap envelope at its random horizon.

theorem abs_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_randomHorizonEnvelope {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (trajectory : Nat -> Fin K × Real) : |stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau trajectory| <= standardScalarAllRoundGapEnvelope S (tau trajectory).untopA L2

A progressively measurable pseudo-regret process remains measurable at an arbitrary stopping time.

theorem measurable_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_of_stoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

The explicit deterministic budget process remains measurable at an arbitrary stopping time.

theorem measurable_stoppedValue_telescopingHighProbabilityPseudoRegretBound_of_stoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] (R delta lambda S L2 : Real) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

First-moment stopping-time regularity makes the random gap envelope integrable.

theorem integrable_standardScalarAllRoundGapEnvelope_at_stoppingTime {K : Nat} (mu : Measure (Nat -> Fin K × Real)) (S L2 : Real) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (hstop : IntegrableFiniteStoppingTime mu tau) : Integrable (fun trajectory => standardScalarAllRoundGapEnvelope S (tau trajectory).untopA L2) mu

The stopped pseudo-regret is integrable under first-moment stopping-time regularity. No deterministic stopping-horizon bound is used.

theorem integrable_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_of_integrableFiniteStoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] (mu : Measure (Nat -> Fin K × Real)) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

The stopped explicit violation event is measurable without a deterministic stopping bound.

theorem measurableSet_telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet_of_stoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (best : Fin K) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

Exact unbounded-stopping expectation decomposition. The bad-event term remains an integral of the random horizon envelope.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_le_integral_stoppedBudget_add_integral_badIndicator_randomHorizonEnvelope {K : Nat} {Feature : Type u} [Fintype Feature] [Nonempty Feature] (mu : Measure (Nat -> Fin K × Real)) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 <= R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K

Canonical generated-trajectory unbounded-stopping theorem. The same stopped violation event has the compiled `delta` tail, while its random-envelope overflow remains explicit in the expectation bound.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_integral_stoppedBudget_add_integral_badIndicator_randomHorizonEnvelope_and_stoppedViolation_measure_le_of_linearSubgaussianEnvironment_of_featureBound_le_regularization {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K