BanditRLProof.OFULScheduledAllTimeConfidence

History-indexed radius using the budget assigned to successor time `n+1`.

noncomputable def finiteHistoryScheduledScalarRidgeRadius {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (lambda S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Real

Scalar-ridge score with the successor-time confidence schedule.

noncomputable def finiteHistoryScheduledScalarRidgeOptimisticScore {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (action : Fin K) : Real

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

theorem finiteHistoryScheduledScalarRidgeOptimisticScore_eq {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (action : Fin K) : finiteHistoryScheduledScalarRidgeOptimisticScore lambda actionFeature R deltaAt S n history action = finiteHistoryScalarRidgeOptimisticScore lambda actionFeature R (deltaAt (n + 1)) S n history action

Every fixed-action scheduled score is measurable in finite history.

theorem measurable_finiteHistoryScheduledScalarRidgeOptimisticScore {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (action : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => finiteHistoryScheduledScalarRidgeOptimisticScore lambda actionFeature R deltaAt S n history action)

Deterministic strict-fold selector for the scheduled scalar-ridge score.

noncomputable def finiteHistoryScheduledScalarRidgeOptimisticAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Fin K

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

theorem finiteHistoryScheduledScalarRidgeOptimisticAction_eq {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : finiteHistoryScheduledScalarRidgeOptimisticAction hK lambda actionFeature R deltaAt S n history = finiteHistoryScalarRidgeOptimisticAction hK lambda actionFeature R (deltaAt (n + 1)) S n history

The scheduled selector maximizes its time-indexed score.

theorem finiteHistoryScheduledScalarRidgeOptimisticAction_score_max {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (action : Fin K) : finiteHistoryScheduledScalarRidgeOptimisticScore lambda actionFeature R deltaAt S n history action <= finiteHistoryScheduledScalarRidgeOptimisticScore lambda actionFeature R deltaAt S n history (finiteHistoryScheduledScalarRidgeOptimisticAction hK lambda actionFeature R deltaAt S n history)

One measurable history algorithm using the supplied all-time schedule.

noncomputable def finiteHistoryScheduledScalarRidgeOptimisticAlgorithm {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) : Thompson.HistoryAlgorithm (Fin K) Real

Scheduled algorithm specialized to the exact telescoping confidence budget.

noncomputable def finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) : Thompson.HistoryAlgorithm (Fin K) Real

The telescoping scheduled policy starts from the fixed canonical arm.

theorem finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm_initialAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) : (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S).initialAction = Measure.dirac ⟨0, hK⟩

The scheduled history-step reward marginal is the environment feedback law at the scheduled selected action.

theorem finiteHistoryScheduledScalarRidge_historyStepKernel_map_snd {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (Thompson.historyStepKernel (finiteHistoryScheduledScalarRidgeOptimisticAlgorithm hK lambda actionFeature R deltaAt S) environment n).map Prod.snd history = environment.feedback n (history, finiteHistoryScheduledScalarRidgeOptimisticAction hK lambda actionFeature R deltaAt S n history)

Feature selected from the scheduled finite-history ridge state.

noncomputable def finiteHistoryScheduledScalarRidgeSelectedFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Feature -> Real

The actual canonical successor feature agrees with the scheduled selector.

theorem canonicalHistoryTrajectory_observedFeature_succ_ae_eq_scheduledSelectedFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScheduledScalarRidgeOptimisticAlgorithm hK lambda actionFeature R deltaAt S) environment, actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)) = finiteHistoryScheduledScalarRidgeSelectedFeature hK lambda actionFeature R deltaAt S n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)

The scheduled selector is measurable in its finite history.

theorem measurable_finiteHistoryScheduledScalarRidgeOptimisticAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (n : Nat) : Measurable (finiteHistoryScheduledScalarRidgeOptimisticAction hK lambda actionFeature R deltaAt S n)

Strict-past scheduled feature process on the canonical trajectory space.

noncomputable def scheduledCanonicalHistoryTrajectoryPredictableFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) : Nat -> (Nat -> Fin K × Real) -> Feature -> Real | 0, _trajectory => actionFeature ⟨0, hK⟩ | n + 1, trajectory => finiteHistoryScheduledScalarRidgeSelectedFeature hK lambda actionFeature R deltaAt S n (Preorder.frestrictLe n trajectory) /-- Every scheduled predictable-feature coordinate is strict-past measurable. -/ theorem scheduledCanonicalHistoryTrajectoryPredictableFeature_stronglyMeasurable {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (t : Nat) (j : Feature) : StronglyMeasurable[ canonicalHistoryTrajectoryBeforeFiltration (K := K) t] (fun trajectory => scheduledCanonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R deltaAt S t trajectory j)

Every scheduled predictable-feature coordinate is strict-past measurable.

theorem scheduledCanonicalHistoryTrajectoryPredictableFeature_stronglyMeasurable {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (t : Nat) (j : Feature) : StronglyMeasurable[ canonicalHistoryTrajectoryBeforeFiltration (K := K) t] (fun trajectory => scheduledCanonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R deltaAt S t trajectory j)

The scheduled algorithm starts from the same deterministic arm.

theorem scheduledCanonicalHistoryTrajectory_action_zero_ae_eq_initialArm {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScheduledScalarRidgeOptimisticAlgorithm hK lambda actionFeature R deltaAt S) environment, Thompson.canonicalHistoryTrajectoryAction trajectory 0 = ⟨0, hK⟩

Actual and scheduled predictable features agree at each time.

theorem canonicalHistoryTrajectoryFeature_ae_eq_scheduledPredictableFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (t : Nat) : canonicalHistoryTrajectoryFeature actionFeature t =ᵐ[ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScheduledScalarRidgeOptimisticAlgorithm hK lambda actionFeature R deltaAt S) environment] scheduledCanonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R deltaAt S t

Actual and scheduled predictable features agree simultaneously.

theorem canonicalHistoryTrajectoryFeature_ae_eq_scheduledPredictableFeature_all {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScheduledScalarRidgeOptimisticAlgorithm hK lambda actionFeature R deltaAt S) environment, ∀ t, canonicalHistoryTrajectoryFeature actionFeature t trajectory = scheduledCanonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R deltaAt S t trajectory

Reward residual around the scheduled strict-past selected feature.

noncomputable def scheduledCanonicalHistoryTrajectoryPredictableResidual {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (i : Nat) (trajectory : Nat -> Fin K × Real) : Real

The zero-initialized scheduled residual process is strongly adapted.

theorem scheduledCanonicalHistoryTrajectoryPredictableResidual_stronglyAdapted {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) : StronglyAdapted (canonicalHistoryTrajectoryBeforeFiltration (K := K)) (fun t trajectory => match t with | 0 => 0 | i + 1 => scheduledCanonicalHistoryTrajectoryPredictableResidual hK lambda thetaStar actionFeature R deltaAt S i trajectory)

Scheduled selected features obey the same finite-action projection cap.

theorem scheduledPredictableFeature_projection_le_finiteActionProjectionBound {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (deltaAt : Nat -> Real) (S : Real) (theta : EuclideanSpace Real Feature) (i : Nat) (trajectory : Nat -> Fin K × Real) : |dotProduct (WithLp.ofLp theta) (scheduledCanonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R deltaAt S i trajectory)| <= finiteActionProjectionBound hK actionFeature theta

All stochastic input needed by scheduled canonical all-time confidence. The field is intentionally all-time and is stated on the one trajectory measure generated by the telescoping-schedule algorithm.

structure CanonicalScheduledPredictableScalarRidgeResidualLaw {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Prop where

The kernel-level linear sub-Gaussian environment contract constructs the all-time predictable residual law for the single telescoping scheduled policy.

noncomputable def canonicalScheduledPredictableScalarRidgeResidualLaw_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : CanonicalScheduledPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R delta S environment where

Pointwise feature equality preserves the countable telescoping event.

theorem mem_allTimeTelescopingScalarRidgeConfidenceFailureSet_iff_of_feature_eq {Omega : Type*} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature feature' : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R delta : Real) (omega : Omega) (hfeature : forall i, feature i omega = feature' i omega) : omega ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R delta ↔ omega ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S feature' response R delta

The scheduled canonical trajectory satisfies all deterministic-horizon scalar-ridge confidence ellipsoids outside one event of probability `delta`.

theorem measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le {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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalScheduledPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R delta S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

The actual successor action agrees with the scheduled strict-fold action.

theorem telescopingCanonicalHistoryTrajectory_action_succ_ae_eq_scheduledAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1) = finiteHistoryScheduledScalarRidgeOptimisticAction hK lambda actionFeature R (allTimeTelescopingDelta delta) S n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)

Outside the scheduled fixed-time confidence failure, the actual successor action satisfies the matching time-indexed optimism-gap certificate.

theorem telescopingCanonicalHistoryTrajectory_action_succ_gap_le_of_not_mem_confidenceFailure {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 delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (comparator : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∉ scalarRidgeConfidenceFailureAt lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R (allTimeTelescopingDelta delta (n + 1)) (n + 1) -> linearValue thetaStar (actionFeature comparator) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1))) <= 2 * finiteHorizonScalarConfidenceRadius (canonicalHistoryTrajectoryFeature actionFeature) R (allTimeTelescopingDelta delta (n + 1)) lambda S (n + 1) trajectory * confidenceWidth (finiteHorizonScalarGram lambda (canonicalHistoryTrajectoryFeature actionFeature) (n + 1) trajectory) (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)))

Event that some successor action violates its scheduled optimism bound.

def telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (comparator : Nat -> Fin K) : Set (Nat -> Fin K × Real)

Any scheduled successor-gap violation forces a confidence failure a.e.

theorem telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet_subset_confidenceFailure_ae {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 delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (comparator : Nat -> Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, trajectory ∈ telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet lambda thetaStar actionFeature R delta S comparator -> trajectory ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta

Generated one-policy all-time successor-gap tail under the explicit scheduled predictable-residual law.

theorem measure_telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet_le {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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (comparator : Nat -> Fin K) (source : CanonicalScheduledPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R delta S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet lambda thetaStar actionFeature R delta S comparator) <= ENNReal.ofReal delta

Generated one-policy all-time confidence tail obtained directly from the linear sub-Gaussian history-environment contract.

theorem measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le_of_linearSubgaussianEnvironment {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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

Generated one-policy all-time successor-gap tail obtained directly from the linear sub-Gaussian history-environment contract.

theorem measure_telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet_le_of_linearSubgaussianEnvironment {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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (comparator : Nat -> Fin K) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalHistoryTrajectoryAllTimeSuccGapViolationSet lambda thetaStar actionFeature R delta S comparator) <= ENNReal.ofReal delta