BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretRate

Semantic finiteness and second-moment regularity for a `WithTop Nat` stopping time. Under a finite measure this contract implies `IntegrableFiniteStoppingTime`.

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

An `L2` finite stopping-time contract supplies the earlier `L1` contract.

theorem SquareIntegrableFiniteStoppingTime.toIntegrableFiniteStoppingTime {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (hstop : SquareIntegrableFiniteStoppingTime mu tau) : IntegrableFiniteStoppingTime mu tau

Project-local `L2` indicator bound. This is the nonnegative `2,2` Holder specialization needed by the random-horizon overflow consumer.

theorem integral_indicator_le_sqrt_secondMoment_mul_sqrt_real_measure {Omega : Type v} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf_nonneg : forall omega, 0 <= f omega) (hf : MemLp f 2 mu) (bad : Set Omega) (hbad : MeasurableSet bad) : integral mu (bad.indicator f) <= Real.sqrt (integral mu (fun omega => f omega ^ 2)) * Real.sqrt (mu.real bad)

The bad-event random-horizon gap envelope is controlled by the stopping-time second moment and the square root of the event probability.

theorem integral_badIndicator_standardScalarAllRoundGapEnvelope_at_stoppingTime_le {K : Nat} (mu : Measure (Nat -> Fin K × Real)) [IsFiniteMeasure mu] (S : Real) (hS : 0 <= S) (L2 : Real) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (hstop : SquareIntegrableFiniteStoppingTime mu tau) (roundSecondMoment : Real) (hroundSecondMoment : integral mu (fun trajectory => ((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) <= roundSecondMoment) (bad : Set (Nat -> Fin K × Real)) (hbad : MeasurableSet bad) : integral mu (bad.indicator (fun trajectory => standardScalarAllRoundGapEnvelope S (tau trajectory).untopA L2)) <= standardScalarInitialGapBound S L2 * Real.sqrt roundSecondMoment * Real.sqrt (mu.real bad)

Canonical generated-trajectory unbounded-stopping expected pseudo-regret rate under a round-count second-moment bound. The `sqrt delta` term comes from the compiled stopped-event tail and the `L2` indicator inequality above.

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_integral_stoppedBudget_add_initialGap_mul_sqrt_roundSecondMoment_mul_sqrt_delta_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 := K)) tau) (hstop : SquareIntegrableFiniteStoppingTime (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) tau) (roundSecondMoment : Real) (hroundSecondMoment : integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) (fun trajectory => ((((tau trajectory).untopA + 1 : Nat) : Real)) ^ 2) <= roundSecondMoment) (hbudgetIntegrable : Integrable (stoppedValue (fun horizon (_trajectory : Nat -> Fin K × Real) => telescopingHighProbabilityPseudoRegretBound (Feature := Feature) R delta lambda S horizon L2) tau) (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment)) : let mu := Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment let stoppedRegret := stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau let stoppedBudget := stoppedValue (fun horizon (_trajectory : Nat -> Fin K × Real) => telescopingHighProbabilityPseudoRegretBound (Feature := Feature) R delta lambda S horizon L2) tau let bad := telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau 0 <= integral mu stoppedRegret ∧ integral mu stoppedRegret <= integral mu stoppedBudget + standardScalarInitialGapBound S L2 * Real.sqrt roundSecondMoment * Real.sqrt delta ∧ mu bad <= ENNReal.ofReal delta