BanditRLProof.OFULConcreteHistoryRidgeSelection

A determinant is measurable when every random matrix entry is measurable.

theorem measurable_matrix_det_of_apply {Omega Index : Type*} [MeasurableSpace Omega] [Fintype Index] [DecidableEq Index] (A : Omega -> Matrix Index Index Real) (hA : forall i j, Measurable (fun omega => A omega i j)) : Measurable (fun omega => Matrix.det (A omega))

Every adjugate entry is measurable under coordinatewise matrix measurability.

theorem measurable_matrix_adjugate_apply_of_apply {Omega Index : Type*} [MeasurableSpace Omega] [Fintype Index] [DecidableEq Index] (A : Omega -> Matrix Index Index Real) (hA : forall i j, Measurable (fun omega => A omega i j)) (i j : Index) : Measurable (fun omega => Matrix.adjugate (A omega) i j)

Every entry of Mathlib's nonsingular inverse is measurable. The proof uses the determinant/adjugate formula, including its zero-at-singular convention.

theorem measurable_matrix_nonsingInv_apply_of_apply {Omega Index : Type*} [MeasurableSpace Omega] [Fintype Index] [DecidableEq Index] (A : Omega -> Matrix Index Index Real) (hA : forall i j, Measurable (fun omega => A omega i j)) (i j : Index) : Measurable (fun omega => (A omega)⁻¹ i j)

A random matrix-vector product is coordinatewise measurable.

theorem measurable_matrix_mulVec_apply_of_apply {Omega Index : Type*} [MeasurableSpace Omega] [Fintype Index] (A : Omega -> Matrix Index Index Real) (x : Omega -> Index -> Real) (hA : forall i j, Measurable (fun omega => A omega i j)) (hx : forall i, Measurable (fun omega => x omega i)) (i : Index) : Measurable (fun omega => (A omega).mulVec (x omega) i)

A random finite dot product is measurable coordinatewise.

theorem measurable_dotProduct_of_apply {Omega Index : Type*} [MeasurableSpace Omega] [Fintype Index] (x y : Omega -> Index -> Real) (hx : forall i, Measurable (fun omega => x omega i)) (hy : forall i, Measurable (fun omega => y omega i)) : Measurable (fun omega => dotProduct (x omega) (y omega))

The OFUL confidence width is measurable from matrix and feature coordinates.

theorem measurable_confidenceWidth_of_apply {Omega Feature : Type*} [MeasurableSpace Omega] [Fintype Feature] [DecidableEq Feature] (V : Omega -> Matrix Feature Feature Real) (x : Omega -> Feature -> Real) (hV : forall i j, Measurable (fun omega => V omega i j)) (hx : forall i, Measurable (fun omega => x omega i)) : Measurable (fun omega => confidenceWidth (V omega) (x omega))

The OFUL optimistic score is measurable from its scalar coordinates.

theorem measurable_optimisticScore_of_apply {Omega Feature : Type*} [MeasurableSpace Omega] [Fintype Feature] [DecidableEq Feature] (thetaHat : Omega -> Feature -> Real) (V : Omega -> Matrix Feature Feature Real) (beta : Omega -> Real) (x : Omega -> Feature -> Real) (hthetaHat : forall i, Measurable (fun omega => thetaHat omega i)) (hV : forall i j, Measurable (fun omega => V omega i j)) (hbeta : Measurable beta) (hx : forall i, Measurable (fun omega => x omega i)) : Measurable (fun omega => optimisticScore (thetaHat omega) (V omega) (beta omega) (x omega))

Entries of a finite-horizon feature Gram are measurable.

theorem measurable_finiteHorizonFeatureGram_apply {Omega Feature : Type*} [MeasurableSpace Omega] (feature : Nat -> Omega -> Feature -> Real) (hfeature : forall t i, Measurable (fun omega => feature t omega i)) (n : Nat) (i j : Feature) : Measurable (fun omega => finiteHorizonFeatureGram feature n omega i j)

Coordinates of the finite-horizon response vector are measurable.

theorem measurable_finiteHorizonResponseVector_apply {Omega Feature : Type*} [MeasurableSpace Omega] [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (hfeature : forall t i, Measurable (fun omega => feature t omega i)) (hresponse : forall t, Measurable (response t)) (n : Nat) (i : Feature) : Measurable (fun omega => finiteHorizonResponseVector feature response n omega i)

Every coordinate of the finite-horizon ridge estimate is measurable.

theorem measurable_finiteHorizonRidgeEstimate_apply {Omega Feature : Type*} [MeasurableSpace Omega] [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (hfeature : forall t i, Measurable (fun omega => feature t omega i)) (hresponse : forall t, Measurable (response t)) (n : Nat) (i : Feature) : Measurable (fun omega => finiteHorizonRidgeEstimate V0 feature response n omega i)

The scalar-ridge finite-horizon confidence radius is measurable.

theorem measurable_finiteHorizonScalarConfidenceRadius {Omega Feature : Type*} [MeasurableSpace Omega] [Fintype Feature] [DecidableEq Feature] (feature : Nat -> Omega -> Feature -> Real) (hfeature : forall t i, Measurable (fun omega => feature t omega i)) (R delta lambda S : Real) (n : Nat) : Measurable (finiteHorizonScalarConfidenceRadius feature R delta lambda S n)

Feature observed at a history coordinate, with zero outside the prefix.

noncomputable def finiteHistoryObservedFeature {K : Nat} {Feature : Type u} (actionFeature : Fin K -> Feature -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (t : Nat) : Feature -> Real

Reward observed at a history coordinate, with zero outside the prefix.

noncomputable def finiteHistoryObservedResponse {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (t : Nat) : Real

Every coordinate of the history-observed feature process is measurable.

theorem measurable_finiteHistoryObservedFeature_apply {K : Nat} {Feature : Type u} (actionFeature : Fin K -> Feature -> Real) (n t : Nat) (i : Feature) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => finiteHistoryObservedFeature actionFeature n history t i)

The history-observed response process is measurable.

theorem measurable_finiteHistoryObservedResponse {K : Nat} (n t : Nat) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => finiteHistoryObservedResponse n history t)

Scalar-ridge estimate reconstructed from the inclusive finite history.

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

Scalar-ridge design matrix reconstructed from the inclusive finite history.

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

Scalar confidence radius reconstructed from the inclusive finite history.

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

The fixed feature of an arm, exposed on the finite-history component API.

def finiteHistoryFixedActionFeature {K : Nat} {Feature : Type u} (actionFeature : Fin K -> Feature -> Real) (n : Nat) (_history : History.FinitePairHistory (Fin K) Real n) (action : Fin K) : Feature -> Real

Concrete scalar-ridge OFUL score computed from an inclusive finite history.

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

Every fixed-arm concrete scalar-ridge score is measurable. In particular, callers do not need to supply a score-measurability premise.

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

Deterministic score-maximizing arm for the concrete scalar-ridge state.

noncomputable def 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) (history : History.FinitePairHistory (Fin K) Real n) : Fin K

The concrete finite-history selector maximizes its scalar-ridge score.

theorem finiteHistoryScalarRidgeOptimisticAction_score_max {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) (history : History.FinitePairHistory (Fin K) Real n) (action : Fin K) : finiteHistoryScalarRidgeOptimisticScore lambda actionFeature R delta S n history action <= finiteHistoryScalarRidgeOptimisticScore lambda actionFeature R delta S n history (finiteHistoryScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history)

Concrete measurable history algorithm obtained from the reconstructed scalar-ridge state, with score measurability discharged internally.

noncomputable def finiteHistoryScalarRidgeOptimisticAlgorithm {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

Feature selected by the concrete scalar-ridge history selector.

noncomputable def finiteHistoryScalarRidgeSelectedFeature {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) (history : History.FinitePairHistory (Fin K) Real n) : Feature -> Real

On the canonical recursive trajectory, the feature of the actual successor arm is almost surely the feature selected from the realized scalar-ridge state.

theorem canonicalHistoryTrajectory_observedFeature_succ_ae_eq_finiteHistoryScalarRidgeSelectedFeature {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 (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment, actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)) = finiteHistoryScalarRidgeSelectedFeature hK lambda actionFeature R delta S n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)