BanditRLProof.Exp3MixedSquareConfidence

Under a positive probability floor and unit losses, the mixed estimator square has the sharper reciprocal-floor bound, rather than the generic square of that reciprocal.

theorem mixedSquaredImportanceWeightedLoss_le_inv_floor {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (chosen : Action) : mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen <= 1 / epsilon

A finite-action mixed estimator square, centered by its exact conditional mean, is conditionally sub-Gaussian whenever the selected action has the stated finite-action conditional distribution.

theorem mixedSquaredEstimator_hasCondSubgaussianMGF_of_condDistrib_ae_eq_finiteActionKernel {Omega : Type u} {History : Type v} {Action : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [mHistory : MeasurableSpace History] [StandardBorelSpace History] [mAction : MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob source) : ProbabilityTheory.HasCondSubgaussianMGF (mHistory.comap history) hhistory.comap_le (fun omega => mixedSquaredImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega) - arms.sum (fun candidate => (loss (history omega) candidate) ^ 2)) (Concentration.intervalVarianceProxy 0 (1 / epsilon)) mu

The predictable mixed-square deviation at an actual generated time.

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

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

theorem sampledPredictableMixedSquaredDeviation_zero_hasCondSubgaussianMGF {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) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace Env).comap (fun sample : Env × ((k : Nat) -> Action × Real) => sample.1)) measurable_fst.comap_le (sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss 0) (Concentration.intervalVarianceProxy 0 (1 / (gamma / (arms.card : Real)))) mu

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

theorem sampledPredictableMixedSquaredDeviation_succ_hasCondSubgaussianMGF {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) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (n : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment let history := fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2) ProbabilityTheory.HasCondSubgaussianMGF ((inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real n)).comap history) (measurable_fst.prodMk ((Preorder.measurable_frestrictLe n).comp measurable_snd)).comap_le (sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss (n + 1)) (Concentration.intervalVarianceProxy 0 (1 / (gamma / (arms.card : Real)))) mu

Shift the actual-time predictable mixed-square deviations by one so that the process starts with the deterministic zero required by the finite-sum conditional concentration API.

noncomputable def sampledPredictableMixedSquaredDeviationProcess {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) : Nat -> Env × ((k : Nat) -> Action × Real) -> Real | 0, _sample => 0 | i + 1, sample => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss i sample noncomputable def sampledMixedSquaredVarianceProxy {Action : Type v} (arms : Finset Action) (gamma : Real) : NNReal

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

noncomputable def sampledMixedSquaredVarianceProxy {Action : Type v} (arms : Finset Action) (gamma : Real) : NNReal

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

noncomputable def sampledMixedSquaredDeviationProxy {Action : Type v} (arms : Finset Action) (gamma : Real) : Nat -> NNReal | 0 => 0 | _i + 1 => sampledMixedSquaredVarianceProxy arms gamma set_option maxHeartbeats 800000 in theorem sampledPredictableMixedSquaredDeviationProcess_stronglyAdapted {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) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableMixedSquaredDeviationProcess arms eta gamma loss)

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

theorem sampledPredictableMixedSquaredDeviationProcess_stronglyAdapted {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) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableMixedSquaredDeviationProcess arms eta gamma loss)

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

theorem sampledPredictableMixedSquaredDeviationProcess_sum_range_succ {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : (Finset.range (horizon + 1)).sum (fun i => sampledPredictableMixedSquaredDeviationProcess arms eta gamma loss i sample) = (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss i sample)

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

theorem sampledMixedSquaredDeviationProxy_sum_range_succ {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) : (Finset.range (horizon + 1)).sum (sampledMixedSquaredDeviationProxy arms gamma) = (horizon : NNReal) * sampledMixedSquaredVarianceProxy arms gamma

Exponential tail for the centered predictable mixed estimator-square sum.

theorem sampledPredictableMixedSquaredDeviation_sum_tail_ennreal {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) {eps : Real} (heps : 0 <= eps) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | eps <= (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * sampledMixedSquaredVarianceProxy arms gamma : NNReal)) : Real))))

The latent predictable mixed estimator-square sum.

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

The sum of exact conditional means of the latent mixed-square scores.

noncomputable def sampledPredictableLossSquaredSum {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

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

theorem sampledPredictableLossSquaredAt_le_card {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 candidate => (predictableLossAt loss t sample candidate) ^ 2) <= (arms.card : Real)

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

theorem sampledPredictableLossSquaredSum_le_card_mul {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 <= (arms.card : Real) * (horizon : Real)

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

theorem sampledPredictableMixedSquaredDeviation_sum_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : (Finset.range horizon).sum (fun t => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss t sample) = sampledPredictableMixedSquaredSum arms eta gamma loss horizon sample - sampledPredictableLossSquaredSum arms loss horizon sample

Exponential tail for the latent, uncentered mixed estimator-square sum.

theorem sampledPredictableMixedSquared_sum_tail_ennreal {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) {eps : Real} (heps : 0 <= eps) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | (arms.card : Real) * (horizon : Real) + eps <= sampledPredictableMixedSquaredSum arms eta gamma loss horizon sample} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * sampledMixedSquaredVarianceProxy arms gamma : NNReal)) : Real))))

The observed scalar-feedback mixed-square sum agrees almost everywhere with the latent predictable mixed-square sum.

theorem sampledObservedMixedSquaredSum_eq_predictable_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment sampledObservedMixedSquaredSum arms eta gamma horizon =ᵐ[mu] sampledPredictableMixedSquaredSum arms eta gamma loss horizon

Exponential confidence for the observed mixed estimator-square sum.

theorem sampledPredictableObservedMixedSquared_sum_tail_exponential {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) {eps : Real} (heps : 0 <= eps) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | (arms.card : Real) * (horizon : Real) + eps <= sampledObservedMixedSquaredSum arms eta gamma horizon sample} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * sampledMixedSquaredVarianceProxy arms gamma : NNReal)) : Real))))

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

noncomputable def sampledMixedSquaredConfidenceRadius {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real

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

theorem sampledMixedSquaredVarianceProxy_pos {Action : Type v} (arms : Finset Action) (harms : arms.Nonempty) (gamma : Real) (hgamma_pos : 0 < gamma) : 0 < ((sampledMixedSquaredVarianceProxy arms gamma : NNReal) : Real)

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

theorem sampledPredictableObservedMixedSquared_sum_tail_exp_neg_budget {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) (hhorizon : 0 < horizon) (budget : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | (arms.card : Real) * (horizon : Real) + Real.sqrt (2 * ((((horizon : NNReal) * sampledMixedSquaredVarianceProxy arms gamma : NNReal)) : Real) * budget) <= sampledObservedMixedSquaredSum arms eta gamma horizon sample} <= ENNReal.ofReal (Real.exp (-budget))

Delta-shaped exponential confidence bound for the observed finite-horizon mixed estimator-square sum.

theorem sampledPredictableObservedMixedSquared_sum_tail_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) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | (arms.card : Real) * (horizon : Real) + sampledMixedSquaredConfidenceRadius arms gamma horizon delta <= sampledObservedMixedSquaredSum arms eta gamma horizon sample} <= ENNReal.ofReal delta