BanditRLProof.OFULAllTimeConfidence

Countable union of scalar-ridge confidence failures over every horizon.

def allTimeScheduledScalarRidgeConfidenceFailureSet {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) : Set Omega

Membership means failure at at least one deterministic horizon.

theorem mem_allTimeScheduledScalarRidgeConfidenceFailureSet_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) (omega : Omega) : omega ∈ allTimeScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt ↔ ∃ n, omega ∈ scalarRidgeConfidenceFailureAt lambda thetaStar S feature response R (deltaAt n) n

Outside the countable failure union, every deterministic-horizon confidence ellipsoid holds simultaneously.

theorem not_mem_allTimeScheduledScalarRidgeConfidenceFailureSet_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) (omega : Omega) : omega ∉ allTimeScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt ↔ ∀ n, 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

All-time scheduled confidence: countable subadditivity bounds the failure probability by the `ENNReal` sum of the fixed-time budgets.

theorem measure_allTimeScheduledScalarRidgeConfidenceFailureSet_le_tsum {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) (hsubGaussian : forall i, HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (hresponse : forall omega i, response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (deltaAt : Nat -> Real) (hdeltaAt : forall n, 0 < deltaAt n) (hdeltaAt_one : forall n, deltaAt n <= 1) : mu (allTimeScheduledScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R deltaAt) <= ∑' n, ENNReal.ofReal (deltaAt n)

Positive telescoping weight `1 / ((n+1)(n+2))`.

noncomputable def allTimeTelescopingWeight (n : Nat) : Real

The telescoping weight is a difference of consecutive reciprocals.

theorem allTimeTelescopingWeight_eq_sub (n : Nat) : allTimeTelescopingWeight n = 1 / (((n + 1 : Nat) : Real)) - 1 / (((n + 2 : Nat) : Real))

Exact finite partial sum of the telescoping weights.

theorem sum_range_allTimeTelescopingWeight (n : Nat) : (Finset.range n).sum allTimeTelescopingWeight = 1 - 1 / (((n + 1 : Nat) : Real))

Every telescoping confidence weight is nonnegative.

theorem allTimeTelescopingWeight_nonneg (n : Nat) : 0 <= allTimeTelescopingWeight n

Every telescoping confidence weight is at most one.

theorem allTimeTelescopingWeight_le_one (n : Nat) : allTimeTelescopingWeight n <= 1

The telescoping weights sum exactly to one.

theorem hasSum_allTimeTelescopingWeight : HasSum allTimeTelescopingWeight 1

Time-`n` share of an all-time failure budget.

noncomputable def allTimeTelescopingDelta (delta : Real) (n : Nat) : Real

Display the scheduled budget as `delta / ((n+1)(n+2))`.

theorem allTimeTelescopingDelta_eq_div (delta : Real) (n : Nat) : allTimeTelescopingDelta delta n = delta / (((n + 1 : Nat) : Real) * ((n + 2 : Nat) : Real))

Positive outer budget gives positive timewise budgets.

theorem allTimeTelescopingDelta_pos {delta : Real} (hdelta : 0 < delta) (n : Nat) : 0 < allTimeTelescopingDelta delta n

If `delta <= 1`, every timewise budget is also at most one.

theorem allTimeTelescopingDelta_le_one {delta : Real} (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : allTimeTelescopingDelta delta n <= 1

The `ENNReal` scheduled failure budgets sum exactly to `ofReal delta`.

theorem tsum_ofReal_allTimeTelescopingDelta {delta : Real} (hdelta : 0 <= delta) : ∑' n, ENNReal.ofReal (allTimeTelescopingDelta delta n) = ENNReal.ofReal delta

Failure set for the exact telescoping all-time confidence schedule.

def allTimeTelescopingScalarRidgeConfidenceFailureSet {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) : Set Omega

All-time scalar-ridge confidence under the exact telescoping failure schedule. The result is one countable event on one process, not a family of horizon-dependent generated algorithms.

theorem measure_allTimeTelescopingScalarRidgeConfidenceFailureSet_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) (hsubGaussian : forall i, HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (hresponse : forall omega i, response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) : mu (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S feature response R delta) <= ENNReal.ofReal delta