BanditRLProof.Exp3RealizedRegretAllTime

Exact finite-prefix decomposition of realized selected-loss regret into exploration-mixed predictable regret and realized deviation.

theorem sampledTrajectoryRealizedRegret_eq_predictableRegret_add_realizedDeviation {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator) = ((Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) + (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedDeviationAt arms eta gamma loss t sample)

At prefix `n+1`, add the predictable-regret and pure realized-deviation schedules after assigning half of the total confidence budget to each event family.

noncomputable def sampledRealizedRegretGeometricAllTimeBudget {Action : Type v} (arms : Finset Action) (eta gamma delta : Real) (n : Nat) : Real

Countable realized selected-loss regret failure event over every positive prefix of one generated EXP3 trajectory.

noncomputable def sampledRealizedRegretGeometricAllTimeFailureSet {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (delta : Real) : Set (Env × ((k : Nat) -> Action × Real))

Membership is realized selected-loss regret failure at at least one positive prefix.

theorem mem_sampledRealizedRegretGeometricAllTimeFailureSet_iff {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (delta : Real) (sample : Env × ((k : Nat) -> Action × Real)) : sample ∈ sampledRealizedRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta ↔ ∃ n, sampledRealizedRegretGeometricAllTimeBudget arms eta gamma delta n <= (Finset.range (n + 1)).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range (n + 1)).sum (fun t => predictableLossAt loss t sample comparator)

A combined realized-regret crossing forces either a predictable-regret crossing or a pure realized-deviation crossing at the same prefix.

theorem sampledRealizedRegretGeometricAllTimeFailureSet_subset {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (comparator : Action) (delta : Real) : sampledRealizedRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta ⊆ sampledPredictableRegretGeometricAllTimeFailureSet arms eta gamma loss comparator (delta / 2) ∪ sampledRealizedDeviationGeometricAllTimeFailureSet arms eta gamma loss (delta / 2)

On one fixed generated EXP3 process and against one fixed supported comparator, realized selected-loss regret stays below the sum of the scheduled predictable-regret and realized-deviation budgets at every positive prefix, outside a set of outer measure at most the total confidence budget.

theorem measure_sampledRealizedRegretGeometricAllTimeFailureSet_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu (sampledRealizedRegretGeometricAllTimeFailureSet arms eta gamma loss comparator delta) <= ENNReal.ofReal delta