BanditRLProof.Exp3MixedSquarePredictableVarianceTail

A centered mixed-square score is bounded by the reciprocal probability floor on the support of the finite sampling distribution.

theorem abs_mixedSquaredEstimatorDeviation_le_inv_floor {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [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) (chosen : Action) (hchosen : chosen ∈ arms) : |mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen - arms.sum (fun action => (loss history action) ^ 2)| <= 1 / epsilon

Exact finite-law fixed-tilt MGF bound. Unlike the deterministic Bernstein wrapper, its exponent retains the actual centered second moment.

theorem finiteActionMixedSquaredEstimator_hasMGFUpperBoundAt_variance {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= epsilon) : Concentration.HasMGFUpperBoundAt (fun chosen => mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen - arms.sum (fun action => (loss history action) ^ 2)) tilt (tilt ^ 2 * mixedSquaredEstimatorCenteredSecondMoment arms prob loss history) (finiteActionMeasure arms (prob history))

Finite-law exponential-supermartingale increment obtained by subtracting the exact variance budget from the centered mixed-square score.

theorem finiteActionMixedSquaredEstimator_compensated_hasMGFUpperBoundAt {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= epsilon) : Concentration.HasMGFUpperBoundAt (fun chosen => tilt * (mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen - arms.sum (fun action => (loss history action) ^ 2)) - tilt ^ 2 * mixedSquaredEstimatorCenteredSecondMoment arms prob loss history) 1 0 (finiteActionMeasure arms (prob history))

An identified finite conditional action law yields a zero-budget conditional MGF for the exact variance-compensated mixed-square increment.

theorem mixedSquaredEstimator_compensated_hasCondMGFUpperBoundAt_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type*} [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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= epsilon) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob source) : Concentration.HasCondMGFUpperBoundAt (mHistory.comap history) hhistory.comap_le (fun omega => tilt * (mixedSquaredImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega) - arms.sum (fun candidate => (loss (history omega) candidate) ^ 2)) - tilt ^ 2 * mixedSquaredEstimatorCenteredSecondMoment arms prob loss (history omega)) 1 0 mu

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

theorem sampledPredictableMixedSquaredCompensated_zero_hasCondMGFUpperBoundAt {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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= gamma / (arms.card : Real)) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment Concentration.HasCondMGFUpperBoundAt ((inferInstance : MeasurableSpace Env).comap (fun sample : Env × ((k : Nat) -> Action × Real) => sample.1)) measurable_fst.comap_le (fun sample => tilt * sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss 0 sample - tilt ^ 2 * sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss 0 sample) 1 0 mu

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

theorem sampledPredictableMixedSquaredCompensated_succ_hasCondMGFUpperBoundAt {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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= gamma / (arms.card : Real)) : 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) Concentration.HasCondMGFUpperBoundAt ((inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real n)).comap history) (measurable_fst.prodMk ((Preorder.measurable_frestrictLe n).comp measurable_snd)).comap_le (fun sample => tilt * sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss (n + 1) sample - tilt ^ 2 * sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss (n + 1) sample) 1 0 mu

Shifted variance-compensated increment process. Index `i + 1` contains the actual-time `i` centered increment and its predictable variance.

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

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

theorem sampledPredictableMixedSquaredCompensatedProcess_stronglyAdapted {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma tilt : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPredictableMixedSquaredCompensatedProcess arms eta gamma tilt loss)

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

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

Fixed-tilt predictable-variance tail for the generated centered mixed-square process. The variance is kept random and enters through the event `sum V <= varianceBudget`; it is not replaced by the deterministic `horizon * K / epsilon` envelope.

theorem sampledPredictableMixedSquaredDeviation_sum_tail_predictableVariance_fixedTilt {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) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= gamma / (arms.card : Real)) (threshold varianceBudget : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | threshold <= (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss i sample) ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) <= varianceBudget} <= ENNReal.ofReal (Real.exp (-tilt * threshold + tilt ^ 2 * varianceBudget))

Optimized radius for the mixed-square predictable-variance event.

noncomputable def sampledMixedSquaredPredictableVarianceRadius {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma varianceBudget delta : Real) : Real

Delta-shaped predictable-variance Bernstein/Freedman bound for the generated centered mixed-square process. This controls the deviation jointly with the event that its cumulative predictable variance is at most `varianceBudget`.

theorem sampledPredictableMixedSquaredDeviation_sum_tail_predictableVariance_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) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | sampledMixedSquaredPredictableVarianceRadius arms gamma varianceBudget delta <= (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss i sample) ∧ (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) <= varianceBudget} <= ENNReal.ofReal delta