BanditRLProof.OFULScheduledBlockStartForcedAllTimeConfidence

Strict-past feature process generated by a measurable deterministic selector.

noncomputable def deterministicHistoryCanonicalPredictableFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) : Nat -> (Nat -> Fin K × Real) -> Feature -> Real | 0, _trajectory => actionFeature ⟨0, hK⟩ | n + 1, trajectory => actionFeature (selector n (Preorder.frestrictLe n trajectory)) /-- Every coordinate of the deterministic-selector feature is strict-past measurable. -/ theorem deterministicHistoryCanonicalPredictableFeature_stronglyMeasurable {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (t : Nat) (j : Feature) : StronglyMeasurable[ canonicalHistoryTrajectoryBeforeFiltration (K

Every coordinate of the deterministic-selector feature is strict-past measurable.

theorem deterministicHistoryCanonicalPredictableFeature_stronglyMeasurable {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (t : Nat) (j : Feature) : StronglyMeasurable[ canonicalHistoryTrajectoryBeforeFiltration (K

A deterministic history algorithm starts from its prescribed fixed arm.

theorem deterministicHistoryCanonical_action_zero_ae_eq_initialArm {K : Nat} (hK : 0 < K) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (Thompson.deterministicHistoryAlgorithm (Fin.mk 0 hK) selector hselector) environment, Thompson.canonicalHistoryTrajectoryAction trajectory 0 = Fin.mk 0 hK

Actual and predictable features agree at every fixed time.

theorem canonicalHistoryTrajectoryFeature_ae_eq_deterministicHistoryPredictableFeature {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) (t : Nat) : canonicalHistoryTrajectoryFeature actionFeature t =ᵐ[ Thompson.canonicalHistoryTrajectoryMeasure (Thompson.deterministicHistoryAlgorithm (Fin.mk 0 hK) selector hselector) environment] deterministicHistoryCanonicalPredictableFeature hK actionFeature selector t

Actual and predictable features agree simultaneously at all times.

theorem canonicalHistoryTrajectoryFeature_ae_eq_deterministicHistoryPredictableFeature_all {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (Thompson.deterministicHistoryAlgorithm (Fin.mk 0 hK) selector hselector) environment, forall t, canonicalHistoryTrajectoryFeature actionFeature t trajectory = deterministicHistoryCanonicalPredictableFeature hK actionFeature selector t trajectory

Reward residual centered at the deterministic selector's strict-past feature.

noncomputable def deterministicHistoryCanonicalPredictableResidual {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (i : Nat) (trajectory : Nat -> Fin K × Real) : Real

The zero-initialized deterministic-selector residual is strongly adapted.

theorem deterministicHistoryCanonicalPredictableResidual_stronglyAdapted {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) : StronglyAdapted (canonicalHistoryTrajectoryBeforeFiltration (K

Deterministic-selector features obey the finite-action projection cap.

theorem deterministicHistoryPredictableFeature_projection_le_finiteActionProjectionBound {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (theta : EuclideanSpace Real Feature) (i : Nat) (trajectory : Nat -> Fin K × Real) : |dotProduct (WithLp.ofLp theta) (deterministicHistoryCanonicalPredictableFeature hK actionFeature selector i trajectory)| <= finiteActionProjectionBound hK actionFeature theta

The reward marginal of a deterministic history step is its selected feedback law.

theorem deterministicHistory_historyStepKernel_map_snd {K : Nat} (initialAction : Fin K) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (Thompson.historyStepKernel (Thompson.deterministicHistoryAlgorithm initialAction selector hselector) environment n).map Prod.snd history = environment.feedback n (history, selector n history)

Stochastic law required by the deterministic-selector all-time confidence layer.

structure CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Prop where

The kernel-level linear sub-Gaussian environment law constructs the predictable residual law for any measurable deterministic history selector.

noncomputable def canonicalDeterministicHistoryPredictableScalarRidgeResidualLaw_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S selector hselector environment where

All-time scalar-ridge confidence for any measurable deterministic history selector, under that selector's own canonical trajectory measure.

theorem measure_deterministicHistoryCanonical_allTimeTelescopingScalarRidgeConfidenceFailureSet_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) (selector : (n : Nat) -> History.FinitePairHistory (Fin K) Real n -> Fin K) (hselector : forall n, Measurable (selector n)) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S selector hselector environment) : Thompson.canonicalHistoryTrajectoryMeasure (Thompson.deterministicHistoryAlgorithm (Fin.mk 0 hK) selector hselector) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

The linear environment law supplies the residual law for the forced selector.

noncomputable def canonicalBlockStartForcedPredictableScalarRidgeResidualLaw_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) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S (finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window) (measurable_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window) environment

Source-level all-time confidence tail for the block-start forced policy.

theorem measure_blockStartForcedCanonicalHistoryTrajectory_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) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S (finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window) (measurable_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window) environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

The concrete block-start forced policy has the same all-time confidence tail under its own canonical measure as any other measurable deterministic selector driven by the same linear sub-Gaussian environment.

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

The nonforced scheduled charge is bounded by the full pathwise width budget.

theorem blockStartOptimisticSuccessorRadiusWidthCharge_le_telescopingStandardScalarRadiusWidthBound {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hdelta : 0 < delta) (hS : 0 <= S) (window horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (trajectory : Nat -> Fin K × Real) : blockStartOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S window horizon trajectory <= telescopingStandardScalarRadiusWidthBound (Feature

The fixed initial arm has the standard deterministic linear-gap envelope.

theorem blockStartForcedCanonicalHistoryTrajectory_initialGap_le_ae {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) (hS : 0 <= S) (forcedAction : Nat -> Fin K) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0)) <= standardScalarInitialGapBound S L2

On the one all-time confidence event, every finite-horizon pseudo-regret is bounded by the deterministic forced-arm charge plus the explicit telescoping OFUL rate.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegret_le_forcedActionCharge_add_explicitBound_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 : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (forcedAction : Nat -> Fin K) (window : Nat) (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) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, forall horizon, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= blockStartForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction window horizon + telescopingHighProbabilityPseudoRegretBound (Feature

All-horizon violation event for the block-start forced pseudo-regret rate.

noncomputable def blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (forcedAction : Nat -> Fin K) (window : Nat) (best : Fin K) : Set (Nat -> Fin K × Real)

Every all-horizon forced-policy regret violation is a confidence failure a.e.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet_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 : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (forcedAction : Nat -> Fin K) (window : Nat) (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) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, trajectory ∈ blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction window best -> trajectory ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta

Complete all-horizon high-probability pseudo-regret theorem for the block-start forced policy. The ordinary OFUL rate is augmented only by the deterministic forced-arm gap charge.

theorem blockStartForcedCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_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) (forcedAction : Nat -> Fin K) (window : Nat) (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) : (forall horizon trajectory, 0 <= canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) ∧ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment (blockStartForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction window best) <= ENNReal.ofReal delta