BanditRLProof.Exp3ComparatorBernstein

On `[-1, 1]`, the exponential remainder is bounded by the square.

theorem exp_le_one_add_self_add_sq_of_abs_le_one {x : Real} (hx : |x| <= 1) : Real.exp x <= 1 + x + x ^ 2

Optimize a quadratic fixed-tilt MGF budget under the hard constraint `tilt <= epsilon`.

theorem exists_tilt_fixedMGF_exponent_le_neg (horizon epsilon budget : Real) (hhorizon : 0 <= horizon) (hepsilon : 0 < epsilon) (hbudget : 0 <= budget) : exists tilt : Real, 0 <= tilt ∧ tilt <= epsilon ∧ -tilt * (2 * Real.sqrt (horizon * budget / epsilon) + budget / epsilon) + horizon * (tilt ^ 2 / epsilon) <= -budget

Exact centered second moment of one fixed-arm importance-weighted estimator.

theorem sum_prob_mul_sq_comparatorEstimatorDeviation_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hdist : FiniteActionDistribution arms prob) (comparator : Action) (hcomparator : comparator ∈ arms) (hprob : prob comparator ≠ 0) : arms.sum (fun chosen => prob chosen * (importanceWeightedLoss prob loss chosen comparator - loss comparator) ^ 2) = (loss comparator) ^ 2 / prob comparator - (loss comparator) ^ 2

The centered comparator estimator has second moment at most the reciprocal probability floor.

theorem sum_prob_mul_sq_comparatorEstimatorDeviation_le_inv_floor {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hdist : FiniteActionDistribution arms prob) (epsilon : Real) (hepsilon : 0 < epsilon) (comparator : Action) (hcomparator : comparator ∈ arms) (hfloor : epsilon <= prob comparator) (hloss : loss comparator ∈ Set.Icc (0 : Real) 1) : arms.sum (fun chosen => prob chosen * (importanceWeightedLoss prob loss chosen comparator - loss comparator) ^ 2) <= 1 / epsilon

Fixed-tilt MGF budget for a finite-law fixed-comparator estimator.

theorem finiteActionComparatorEstimator_hasMGFUpperBoundAt {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hdist : FiniteActionDistribution arms prob) (epsilon : Real) (hepsilon : 0 < epsilon) (comparator : Action) (hcomparator : comparator ∈ arms) (hfloor : epsilon <= prob comparator) (hloss : loss comparator ∈ Set.Icc (0 : Real) 1) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= epsilon) : Concentration.HasMGFUpperBoundAt (fun chosen => importanceWeightedLoss prob loss chosen comparator - loss comparator) tilt (tilt ^ 2 / epsilon) (finiteActionMeasure arms prob)

A finite conditional action law supplies the variance-sensitive fixed-tilt MGF budget for one fixed comparator estimator.

theorem comparatorEstimator_hasCondMGFUpperBoundAt_of_condDistrib_ae_eq_finiteActionKernel {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) (comparator : Action) (hcomparator : comparator ∈ arms) (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 => importanceWeightedLoss (prob (history omega)) (loss (history omega)) (action omega) comparator - loss (history omega) comparator) tilt (tilt ^ 2 / epsilon) mu

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

theorem sampledPredictableComparatorEstimatorDeviation_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) (comparator : Action) (hcomparator : comparator ∈ arms) (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 (sampledTrajectoryPredictableComparatorEstimatorDeviationAt arms eta gamma loss comparator 0) tilt (tilt ^ 2 / (gamma / (arms.card : Real))) mu

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

theorem sampledPredictableComparatorEstimatorDeviation_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) (comparator : Action) (hcomparator : comparator ∈ arms) (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 (sampledTrajectoryPredictableComparatorEstimatorDeviationAt arms eta gamma loss comparator (n + 1)) tilt (tilt ^ 2 / (gamma / (arms.card : Real))) mu

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

theorem sampledObservedComparatorEstimatorDeviation_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) (comparator : Action) (hcomparator : comparator ∈ arms) (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 (sampledTrajectoryObservedComparatorEstimatorDeviationAt arms eta gamma loss comparator 0) tilt (tilt ^ 2 / (gamma / (arms.card : Real))) mu

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

theorem sampledObservedComparatorEstimatorDeviation_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) (comparator : Action) (hcomparator : comparator ∈ arms) (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 (sampledTrajectoryObservedComparatorEstimatorDeviationAt arms eta gamma loss comparator (n + 1)) tilt (tilt ^ 2 / (gamma / (arms.card : Real))) mu

Variance-sensitive finite-horizon Chernoff bound for one fixed comparator on the generated EXP3 trajectory. The per-round budget is linear, rather than quadratic, in the reciprocal exploration floor.

theorem sampledObservedComparatorEstimatorDeviation_sum_tail_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) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (tilt : Real) (htilt_nonneg : 0 <= tilt) (htilt_le : tilt <= gamma / (arms.card : Real)) (threshold : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu.real {sample | threshold <= (Finset.range horizon).sum (fun i => sampledTrajectoryObservedComparatorEstimatorDeviationAt arms eta gamma loss comparator i sample)} <= Real.exp (-tilt * threshold + (horizon : Real) * (tilt ^ 2 / (gamma / (arms.card : Real))))

Variance-sensitive confidence radius obtained by optimizing the fixed-tilt comparator tail.

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

Delta-shaped variance-sensitive confidence bound for one fixed comparator's observed importance-weighted estimator on the generated EXP3 trajectory.

theorem sampledObservedComparatorEstimatorDeviation_sum_tail_bernstein_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) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment mu {sample | sampledComparatorEstimatorBernsteinConfidenceRadius arms gamma horizon delta <= (Finset.range horizon).sum (fun i => sampledTrajectoryObservedComparatorEstimatorDeviationAt arms eta gamma loss comparator i sample)} <= ENNReal.ofReal delta