BanditRLProof.Exp3MixedSquarePredictableVarianceLossEnergyRealizedMarkovHighProbabilityRegret

A finite-action centered mixed-square estimator has variance at most the inverse probability floor times the armwise loss-square energy.

theorem sum_prob_mul_sq_mixedSquaredEstimatorDeviation_le_inv_floor_mul_sum_loss_sq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action → Real) (hdist : FiniteActionDistribution arms prob) (epsilon : Real) (hepsilon : 0 < epsilon) (hfloor : ∀ action, action ∈ arms → epsilon ≤ prob action) (hloss : ∀ action, action ∈ arms → loss action ∈ Set.Icc (0 : Real) 1) : arms.sum (fun chosen => prob chosen * (mixedSquaredImportanceWeightedLoss arms prob loss chosen - arms.sum (fun action => (loss action) ^ 2)) ^ 2) ≤ (1 / epsilon) * arms.sum (fun action => (loss action) ^ 2)

No declaration docstring is present; use the chapter context and exact statement below.

theorem mixedSquaredEstimatorCenteredSecondMoment_le_inv_floor_mul_sum_loss_sq {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (prob loss : History → Action → Real) (history : History) (hdist : FiniteActionDistribution arms (prob history)) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : mixedSquaredEstimatorCenteredSecondMoment arms prob loss history ≤ (1 / epsilon) * arms.sum (fun action => (loss history action) ^ 2)

Pointwise generated-time specialization of the finite loss-energy bound.

theorem sampledTrajectoryPredictableMixedSquaredVarianceAt_le_inv_floor_mul_lossSquaredAt {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) (t : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss t sample ≤ (1 / (gamma / (arms.card : Real))) * arms.sum (fun action => (predictableLossAt loss t sample action) ^ 2)

Cumulative predictable variance is controlled by cumulative armwise predictable loss-square energy.

theorem sampledPredictableMixedSquaredVarianceSum_le_inv_floor_mul_lossSquaredSum {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))) * sampledPredictableLossSquaredSum arms loss horizon sample

A pathwise predictable loss-square budget yields the generated cumulative-variance `lintegral` budget required by the Markov route.

theorem sampledPredictableMixedSquaredVarianceLIntegral_le_of_lossSquaredSum_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) (lossSquaredBudget : Real) (henergy : ∀ sample, sampledPredictableLossSquaredSum arms loss horizon sample ≤ lossSquaredBudget) : sampledPredictableMixedSquaredVarianceLIntegral mu arms eta gamma loss horizon ≤ ENNReal.ofReal ((1 / (gamma / (arms.card : Real))) * lossSquaredBudget)

Realized Markov budget specialized to a cumulative predictable loss-square energy budget.

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

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

theorem sampledPredictable_predictableVarianceSquareLossEnergyRealizedMarkovHighProbabilityRegret_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) (lossSquaredBudget delta : Real) (hlossSquaredBudget : 0 < lossSquaredBudget) (hdelta : 0 < delta) (henergy : ∀ sample, sampledPredictableLossSquaredSum arms loss horizon sample ≤ lossSquaredBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareLossEnergyRealizedMarkovHighProbabilityRegretBudget arms eta gamma horizon lossSquaredBudget delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ ENNReal.ofReal delta