BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedMarkovHighProbabilityRegret

Every generated predictable loss coordinate remains in the unit interval.

theorem predictableLossAt_mem_unitInterval {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) → Action × Real)) (action : Action) : predictableLossAt loss t sample action ∈ Set.Icc (0 : Real) 1

Cumulative armwise predictable loss mass along a generated trajectory.

noncomputable def sampledPredictableLossMassSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : Real

Unit-interval losses have armwise square mass at most armwise loss mass.

theorem sampledPredictableLossSquaredAt_le_lossMassAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) → Action × Real)) : arms.sum (fun action => (predictableLossAt loss t sample action) ^ 2) ≤ arms.sum (fun action => predictableLossAt loss t sample action)

Cumulative predictable loss-square energy is at most cumulative armwise predictable loss mass.

theorem sampledPredictableLossSquaredSum_le_lossMassSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableLossSquaredSum arms loss horizon sample ≤ sampledPredictableLossMassSum arms loss horizon sample

Cumulative predictable mixed-square variance is controlled by armwise predictable loss mass.

theorem sampledPredictableMixedSquaredVarianceSum_le_inv_floor_mul_lossMassSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableMixedSquaredVarianceSum arms eta gamma loss horizon sample ≤ (1 / (gamma / (arms.card : Real))) * sampledPredictableLossMassSum arms loss horizon sample

An almost-everywhere armwise loss-mass budget supplies the cumulative-variance `lintegral` contract required by the Markov route.

theorem sampledPredictableMixedSquaredVarianceLIntegral_le_of_lossMassSum_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (lossMassBudget : Real) (hmass : ∀ᵐ sample ∂mu, sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget) : sampledPredictableMixedSquaredVarianceLIntegral mu arms eta gamma loss horizon ≤ ENNReal.ofReal ((1 / (gamma / (arms.card : Real))) * lossMassBudget)

Off-bad observed-square tail when the armwise loss-mass budget may fail on an explicit bad set. No measurability assumption on that set is needed.

theorem sampledPredictableObservedMixedSquared_sum_tail_predictableVariance_off_bad_of_lossMassSum_le_or_mem {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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (lossMassBudget varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu ({sample | lossMassBudget + sampledMixedSquaredPredictableVarianceRadius arms gamma varianceBudget delta ≤ sampledObservedMixedSquaredSum arms eta gamma horizon sample ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} \ bad) ≤ ENNReal.ofReal delta

Residual observed-square tail when the armwise loss-mass budget may fail on an explicit bad set.

theorem sampledPredictableObservedMixedSquared_sum_tail_predictableVariance_of_lossMassSum_le_or_mem {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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (lossMassBudget varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | lossMassBudget + sampledMixedSquaredPredictableVarianceRadius arms gamma varianceBudget delta ≤ sampledObservedMixedSquaredSum arms eta gamma horizon sample ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ENNReal.ofReal delta + mu bad

The observed mixed estimator-square sum has its predictable mean bounded by the supplied almost-everywhere armwise loss-mass budget.

theorem sampledPredictableObservedMixedSquared_sum_tail_predictableVariance_of_lossMassSum_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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (lossMassBudget varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | lossMassBudget + sampledMixedSquaredPredictableVarianceRadius arms gamma varianceBudget delta ≤ sampledObservedMixedSquaredSum arms eta gamma horizon sample ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ENNReal.ofReal delta

Predictable regret budget whose mixed-square mean upper bound is the supplied armwise loss-mass budget rather than `K * T`.

noncomputable def sampledPredictableVarianceSquareSmallLossHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (lossMassBudget varianceBudget deltaSquare deltaConfidence : Real) : Real

Off-bad predictable small-loss regret on the variance-good event. The explicit bad set is removed from the source event, so it does not enter the confidence allocation.

theorem sampledPredictable_predictableVarianceSquareSmallLossHighProbabilityRegret_tail_joint_off_bad_of_lossMassSum_le_or_mem {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) (horizon : Nat) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu ({sample | sampledPredictableVarianceSquareSmallLossHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} \ bad) ≤ (ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence

Residual small-loss predictable regret on the variance-good event when the loss-mass budget may fail on an explicit bad set.

theorem sampledPredictable_predictableVarianceSquareSmallLossHighProbabilityRegret_tail_joint_of_lossMassSum_le_or_mem {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) (horizon : Nat) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSmallLossHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ (ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence + mu bad

Small-loss predictable regret on the event that cumulative predictable mixed-square variance stays below `varianceBudget`.

theorem sampledPredictable_predictableVarianceSquareSmallLossHighProbabilityRegret_tail_joint {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) (horizon : Nat) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSmallLossHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ (ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence

Realized small-loss regret budget with a caller-supplied predictable variance budget.

noncomputable def sampledPredictableVarianceSquareSmallLossRealizedHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (lossMassBudget varianceBudget deltaSquare deltaConfidence deltaRealized : Real) : Real

Off-bad realized small-loss regret on the predictable-variance-good event. The four confidence events are charged here; the explicit bad set can be charged once by a downstream pathwise decomposition.

theorem sampledPredictable_predictableVarianceSquareSmallLossRealizedHighProbabilityRegret_tail_joint_off_bad_of_lossMassSum_le_or_mem {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) (horizon : Nat) (hhorizon : 0 < horizon) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence deltaRealized : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu ({sample | sampledPredictableVarianceSquareSmallLossRealizedHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence deltaRealized ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} \ bad) ≤ ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized

Residual realized small-loss regret on the predictable-variance-good event when the loss-mass budget may fail on an explicit bad set.

theorem sampledPredictable_predictableVarianceSquareSmallLossRealizedHighProbabilityRegret_tail_joint_of_lossMassSum_le_or_mem {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) (horizon : Nat) (hhorizon : 0 < horizon) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence deltaRealized : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) (bad : Set (Env × ((k : Nat) → Action × Real))) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget ∨ sample ∈ bad) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSmallLossRealizedHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence deltaRealized ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized + (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment) bad

Realized small-loss regret on the predictable-variance-good event.

theorem sampledPredictable_predictableVarianceSquareSmallLossRealizedHighProbabilityRegret_tail_joint {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) (horizon : Nat) (hhorizon : 0 < horizon) (lossMassBudget varianceBudget : Real) (deltaSquare deltaConfidence deltaRealized : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSmallLossRealizedHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget varianceBudget deltaSquare deltaConfidence deltaRealized ≤ (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 i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) ≤ varianceBudget} ≤ ((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized

Five-event small-loss realized budget: the mixed-square predictable mean is `lossMassBudget`, while the Markov variance mean is `(1 / (gamma / K)) * lossMassBudget`.

noncomputable def sampledPredictableVarianceSquareSmallLossRealizedMarkovHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (lossMassBudget delta : Real) : Real

Primary armwise small-loss specialization of the Markov-closed realized EXP3 theorem.

theorem sampledPredictable_predictableVarianceSquareSmallLossRealizedMarkovHighProbabilityRegret_tail_total_delta {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) (horizon : Nat) (hhorizon : 0 < horizon) (lossMassBudget delta : Real) (hlossMassBudget : 0 < lossMassBudget) (hdelta : 0 < delta) (hmass : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), sampledPredictableLossMassSum arms loss horizon sample ≤ lossMassBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSmallLossRealizedMarkovHighProbabilityRegretBudget arms eta gamma horizon lossMassBudget delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ ENNReal.ofReal delta