BanditRLProof.OFULUniformTimeConfidence

Failure of the scalar-ridge confidence ellipsoid at one horizon.

def scalarRidgeConfidenceFailureAt {Omega : Type u} {Feature : Type v} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R delta : Real) (n : Nat) : Set Omega

Union of scalar-ridge confidence failures over all `n <= horizon`, with the confidence level selected by `deltaAt n`.

def finiteHorizonScheduledScalarRidgeConfidenceFailureSet {Omega : Type u} {Feature : Type v} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R : Real) (deltaAt : Nat -> Real) (horizon : Nat) : Set Omega

Membership in the scheduled failure set is failure at some `n <= horizon`.

theorem mem_finiteHorizonScheduledScalarRidgeConfidenceFailureSet_iff {Omega : Type u} {Feature : Type v} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R : Real) (deltaAt : Nat -> Real) (horizon : Nat) (omega : Omega) : omega ∈ finiteHorizonScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt horizon ↔ ∃ n, n <= horizon ∧ omega ∈ scalarRidgeConfidenceFailureAt lambda thetaStar S feature response R (deltaAt n) n

Outside the scheduled failure union, every scalar-ridge confidence ellipsoid in the inclusive finite window holds simultaneously.

theorem not_mem_finiteHorizonScheduledScalarRidgeConfidenceFailureSet_iff {Omega : Type u} {Feature : Type v} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R : Real) (deltaAt : Nat -> Real) (horizon : Nat) (omega : Omega) : omega ∉ finiteHorizonScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt horizon ↔ ∀ n, n <= horizon -> matrixNorm (Matrix.scalar Feature lambda + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate (Matrix.scalar Feature lambda) feature response n omega - thetaStar) <= finiteHorizonScalarConfidenceRadius feature R (deltaAt n) lambda S n omega

Scheduled finite-window confidence: the failure-union probability is bounded by the sum of the fixed-time confidence budgets.

theorem measure_finiteHorizonScheduledScalarRidgeConfidenceFailureSet_le_sum {Omega : Type u} {Feature : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (S : Real) (htheta : euclideanLength thetaStar <= S) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (R : Real) (hR : 0 < R) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (horizon : Nat) (hsubGaussian : forall i, i < horizon -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (hresponse : forall omega i, i < horizon -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (deltaAt : Nat -> Real) (hdeltaAt : forall n, n <= horizon -> 0 < deltaAt n) (hdeltaAt_one : forall n, n <= horizon -> deltaAt n <= 1) : mu (finiteHorizonScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt horizon) <= (Finset.range (horizon + 1)).sum (fun n => ENNReal.ofReal (deltaAt n))

Equal-share finite-window failure union. The inclusive window has `horizon + 1` horizons, so each fixed-time theorem receives `delta / (horizon + 1)`.

def finiteHorizonUniformScalarRidgeConfidenceFailureSet {Omega : Type u} {Feature : Type v} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (thetaStar : Feature -> Real) (S : Real) (feature : Nat -> Omega -> Feature -> Real) (response : Nat -> Omega -> Real) (R delta : Real) (horizon : Nat) : Set Omega

Uniform scalar-ridge confidence over every deterministic horizon `n <= horizon`, obtained by equal allocation of the total failure budget.

theorem measure_finiteHorizonUniformScalarRidgeConfidenceFailureSet_le {Omega : Type u} {Feature : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (S : Real) (htheta : euclideanLength thetaStar <= S) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (R : Real) (hR : 0 < R) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (horizon : Nat) (hsubGaussian : forall i, i < horizon -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (hresponse : forall omega i, i < horizon -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) : mu (finiteHorizonUniformScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R delta horizon) <= ENNReal.ofReal delta