BanditRLProof.OFULScheduledBoundedStoppingTimeHighProbabilityRegretRate

The canonical trajectory filtration through the current round. At level `T` it contains exactly the coordinates `0, ..., T`.

def canonicalHistoryTrajectoryAllRoundFiltration {K : Nat} : Filtration Nat (inferInstance : MeasurableSpace (Nat -> Fin K × Real))

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistoryTrajectoryAllRoundFiltration_apply {K : Nat} (horizon : Nat) : (canonicalHistoryTrajectoryAllRoundFiltration (K

Every coordinate `t <= T` is measurable at all-round level `T`.

theorem measurable_canonicalHistoryTrajectory_coordinate_allRound {K : Nat} {t horizon : Nat} (ht : t <= horizon) : @Measurable (Nat -> Fin K × Real) (Fin K × Real) (canonicalHistoryTrajectoryAllRoundFiltration (K

A trajectory time below a finite deterministic horizon cannot be `top`.

theorem boundedTrajectoryTime_ne_top {K : Nat} (tau : (Nat -> Fin K × Real) -> WithTop Nat) (maxHorizon : Nat) (htau_le : forall trajectory, tau trajectory <= (maxHorizon : WithTop Nat)) : forall trajectory, tau trajectory ≠ (⊤ : WithTop Nat)

Under a finite bound, `untopA` recovers the actual stopping-time value.

theorem coe_untopA_boundedTrajectoryTime {K : Nat} (tau : (Nat -> Fin K × Real) -> WithTop Nat) (maxHorizon : Nat) (htau_le : forall trajectory, tau trajectory <= (maxHorizon : WithTop Nat)) (trajectory : Nat -> Fin K × Real) : ((tau trajectory).untopA : WithTop Nat) = tau trajectory

Complete fixed-best pseudo-regret through horizon `T` is measurable using only trajectory coordinates `0, ..., T`.

theorem measurable_canonicalStandardHighProbabilityPseudoRegret_allRound {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (horizon : Nat) : @Measurable (Nat -> Fin K × Real) Real (canonicalHistoryTrajectoryAllRoundFiltration (K

The complete fixed-best pseudo-regret process is strongly adapted to the canonical all-round trajectory filtration.

theorem canonicalStandardHighProbabilityPseudoRegret_stronglyAdapted_allRound {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) : StronglyAdapted (canonicalHistoryTrajectoryAllRoundFiltration (K

The deterministic explicit rate process is strongly adapted.

theorem telescopingHighProbabilityPseudoRegretBound_stronglyAdapted_allRound {K : Nat} {Feature : Type u} [Fintype Feature] (R delta lambda S L2 : Real) : StronglyAdapted (canonicalHistoryTrajectoryAllRoundFiltration (K

Violation of the explicit scheduled pseudo-regret rate after evaluating both the deterministic budget and pseudo-regret process at a Mathlib stopped value.

noncomputable def telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet {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) : Set (Nat -> Fin K × Real)

Every stopped-value violation is already an all-horizon violation, with the same trajectory and witness horizon.

theorem telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet_subset_allHorizon {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) : telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau ⊆ telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best

For a bounded stopping time, the stopped explicit violation event is measurable at the deterministic bound.

theorem measurableSet_telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet_of_boundedStoppingTime {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

The stopped-value violation event inherits the all-horizon `delta` tail. This pathwise transport does not require the index to be a stopping time.

theorem measure_telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet_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) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau) <= ENNReal.ofReal delta

Complete bounded-stopping-time high-probability pseudo-regret theorem for the single telescoping-schedule OFUL policy.

theorem telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_boundedStoppingTime_tail_le_explicitBound_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