BanditRLProof.OFULGeneratedTrajectoryPredictableConfidence

The canonical trajectory filtration strictly before the current coordinate. Level zero is trivial, while level `n + 1` contains exactly coordinates `0, ..., n`.

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

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

theorem canonicalHistoryTrajectoryBeforeFiltration_zero {K : Nat} : (canonicalHistoryTrajectoryBeforeFiltration (K

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

theorem canonicalHistoryTrajectoryBeforeFiltration_succ {K : Nat} (n : Nat) : (canonicalHistoryTrajectoryBeforeFiltration (K

The concrete scalar-ridge strict-fold selector is measurable in its history.

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

Pointwise predictable feature used by scalar-ridge confidence. At time zero it uses the deterministic initial arm. At time `n + 1` it uses the strict-fold selector evaluated only on coordinates through `n`.

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

Every coordinate of the predictable feature is strict-past measurable.

theorem canonicalHistoryTrajectoryPredictableFeature_stronglyMeasurable {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (t : Nat) (j : Feature) : StronglyMeasurable[ canonicalHistoryTrajectoryBeforeFiltration (K

The initial canonical action of the concrete OFUL algorithm is its Dirac arm a.e.

theorem canonicalHistoryTrajectory_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 delta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, Thompson.canonicalHistoryTrajectoryAction trajectory 0 = ⟨0, hK⟩

Actual and pointwise predictable canonical features agree a.e. at each time.

theorem canonicalHistoryTrajectoryFeature_ae_eq_predictableFeature {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) (t : Nat) : canonicalHistoryTrajectoryFeature actionFeature t =ᵐ[ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment] canonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R delta S t

Actual and predictable canonical features agree simultaneously at all times.

theorem canonicalHistoryTrajectoryFeature_ae_eq_predictableFeature_all {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) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, ∀ t, canonicalHistoryTrajectoryFeature actionFeature t trajectory = canonicalHistoryTrajectoryPredictableFeature hK lambda actionFeature R delta S t trajectory

Canonical reward residual around the pointwise predictable linear response.

noncomputable def canonicalHistoryTrajectoryPredictableResidual {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) (i : Nat) (trajectory : Nat -> Fin K × Real) : Real

The canonical reward coordinate at time `i` is measurable at level `i + 1`.

theorem measurable_canonicalHistoryTrajectoryResponse_before_succ {K : Nat} (i : Nat) : @Measurable (Nat -> Fin K × Real) Real (canonicalHistoryTrajectoryBeforeFiltration (K

The zero-initialized predictable residual process is strongly adapted.

theorem canonicalHistoryTrajectoryPredictableResidual_stronglyAdapted {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) : StronglyAdapted (canonicalHistoryTrajectoryBeforeFiltration (K

Maximum absolute projection over the finite arm set.

noncomputable def finiteActionProjectionBound {K : Nat} {Feature : Type u} [Fintype Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (theta : EuclideanSpace Real Feature) : Real

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

theorem finiteActionProjectionBound_nonneg {K : Nat} {Feature : Type u} [Fintype Feature] (hK : 0 < K) (actionFeature : Fin K -> Feature -> Real) (theta : EuclideanSpace Real Feature) : 0 <= finiteActionProjectionBound hK actionFeature theta

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

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

The remaining stochastic law for predictable canonical confidence. Measurability, adaptedness, deterministic finite-arm projection bounds, and the pointwise response identity are derived by this module. A concrete environment producer therefore only needs the parameter norm and the strict-past conditional MGF of the canonical predictable residual.

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

Pointwise feature equality preserves every fixed-time scalar-ridge event.

theorem mem_scalarRidgeConfidenceFailureAt_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) (n : Nat) (omega : Omega) (hfeature : forall i, feature i omega = feature' i omega) : omega ∈ scalarRidgeConfidenceFailureAt lambda thetaStar S feature response R delta n ↔ omega ∈ scalarRidgeConfidenceFailureAt lambda thetaStar S feature' response R delta n

Pointwise feature equality preserves the finite-window uniform failure event.

theorem mem_finiteHorizonUniformScalarRidgeConfidenceFailureSet_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) (horizon : Nat) (omega : Omega) (hfeature : forall i, feature i omega = feature' i omega) : omega ∈ finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R delta horizon ↔ omega ∈ finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S feature' response R delta horizon

Uniform scalar-ridge confidence on the actual canonical selected features, derived from only the predictable residual conditional law.

theorem measure_canonicalHistoryTrajectory_uniformScalarRidgeConfidenceFailureSet_le_of_predictableResidualLaw {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) (horizon : Nat) (source : CanonicalPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S environment horizon) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment (finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta horizon) <= ENNReal.ofReal delta

Canonical successor-gap tail derived from the strict-past predictable residual law. Unlike the earlier source theorem, no pointwise measurability of the actual selected feature is assumed.

theorem measure_canonicalHistoryTrajectorySumRangeSuccGapViolationSet_le_of_predictableResidualLaw {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) (horizon : Nat) (comparator : Nat -> Fin K) (source : CanonicalPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S environment horizon) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment (canonicalHistoryTrajectorySumRangeSuccGapViolationSet lambda thetaStar actionFeature R delta S horizon comparator) <= ENNReal.ofReal delta