BanditRLProof.Exp3PureConfidence

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

theorem weightedEstimator_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 weight loss : History -> Action -> Real) (probSource : MeasurableFiniteActionDistribution arms prob) (weightSource : MeasurableFiniteActionDistribution arms weight) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob probSource) : ProbabilityTheory.HasCondSubgaussianMGF (mHistory.comap history) hhistory.comap_le (fun omega => weightedImportanceWeightedLoss arms (prob (history omega)) (weight (history omega)) (loss (history omega)) (action omega) - arms.sum (fun candidate => weight (history omega) candidate * loss (history omega) candidate)) (Concentration.intervalVarianceProxy 0 (1 / epsilon)) mu

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

noncomputable def sampledTrajectoryWeightedPurePredictableDeviationAt {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.

noncomputable def sampledTrajectoryPureObservedDeviationAt {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 sampledWeightedPurePredictableDeviation_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 (sampledTrajectoryWeightedPurePredictableDeviationAt arms eta gamma loss 0) (sampledComparatorEstimatorVarianceProxy arms gamma) mu

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

theorem sampledWeightedPurePredictableDeviation_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 (sampledTrajectoryWeightedPurePredictableDeviationAt arms eta gamma loss (n + 1)) (sampledComparatorEstimatorVarianceProxy arms gamma) mu

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

theorem sampledPureObservedDeviation_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 (sampledTrajectoryPureObservedDeviationAt arms eta gamma loss 0) (sampledComparatorEstimatorVarianceProxy arms gamma) mu

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

theorem sampledPureObservedDeviation_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 (sampledTrajectoryPureObservedDeviationAt arms eta gamma loss (n + 1)) (sampledComparatorEstimatorVarianceProxy arms gamma) mu

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

noncomputable def sampledPureObservedDeviationProcess {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 => sampledTrajectoryPureObservedDeviationAt arms eta gamma loss i sample theorem sampledPureObservedDeviationProcess_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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPureObservedDeviationProcess arms eta gamma loss)

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

theorem sampledPureObservedDeviationProcess_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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPureObservedDeviationProcess arms eta gamma loss)

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

noncomputable abbrev sampledPureObservedDeviationVarianceProxy {Action : Type v} (arms : Finset Action) (gamma : Real) : NNReal

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

noncomputable abbrev sampledPureObservedDeviationProxy {Action : Type v} (arms : Finset Action) (gamma : Real) : Nat -> NNReal

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

theorem sampledPureObservedDeviationProcess_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 => sampledPureObservedDeviationProcess arms eta gamma loss i sample) = (Finset.range horizon).sum (fun i => sampledTrajectoryPureObservedDeviationAt arms eta gamma loss i sample)

One-sided concentration for the pure-Hedge cross-weighted observed EXP3 estimator minus its true pure-Hedge predictable loss.

theorem sampledPureObservedDeviation_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 => sampledTrajectoryPureObservedDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * sampledPureObservedDeviationVarianceProxy arms gamma : NNReal)) : Real))))

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

noncomputable def sampledPureObservedDeviationConfidenceRadius {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 sampledPureObservedDeviation_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 | Real.sqrt (2 * ((((horizon : NNReal) * sampledPureObservedDeviationVarianceProxy arms gamma : NNReal)) : Real) * budget) <= (Finset.range horizon).sum (fun i => sampledTrajectoryPureObservedDeviationAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-budget))

Delta-shaped one-sided confidence bound for the pure-Hedge cross-weighted observed EXP3 estimator against its true pure-Hedge predictable loss.

theorem sampledPureObservedDeviation_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 | sampledPureObservedDeviationConfidenceRadius arms gamma horizon delta <= (Finset.range horizon).sum (fun i => sampledTrajectoryPureObservedLossAt arms eta gamma i sample - sampledTrajectoryPurePredictableLossAt arms eta gamma loss i sample)} <= ENNReal.ofReal delta

The pure-Hedge predictable loss minus its observed cross-weighted estimator. This is the sign needed when the sampled Hedge inequality is converted to true predictable regret.

noncomputable def sampledTrajectoryPurePredictableMinusObservedAt {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 sampledPurePredictableMinusObserved_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 (sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss 0) (sampledPureObservedDeviationVarianceProxy arms gamma) mu

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

theorem sampledPurePredictableMinusObserved_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 (sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss (n + 1)) (sampledPureObservedDeviationVarianceProxy arms gamma) mu

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

noncomputable def sampledPurePredictableMinusObservedProcess {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 => sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss i sample theorem sampledPurePredictableMinusObservedProcess_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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPurePredictableMinusObservedProcess arms eta gamma loss)

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

theorem sampledPurePredictableMinusObservedProcess_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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : StronglyAdapted (sampledPredictableDeviationFiltration Env Action) (sampledPurePredictableMinusObservedProcess arms eta gamma loss)

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

theorem sampledPurePredictableMinusObservedProcess_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 => sampledPurePredictableMinusObservedProcess arms eta gamma loss i sample) = (Finset.range horizon).sum (fun i => sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss i sample)

One-sided concentration in the sign required by the predictable-regret decomposition: true pure-Hedge predictable loss minus its observed estimator.

theorem sampledPurePredictableMinusObserved_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 => sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((((horizon : NNReal) * sampledPureObservedDeviationVarianceProxy arms gamma : NNReal)) : Real))))

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

theorem sampledPurePredictableMinusObserved_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 | Real.sqrt (2 * ((((horizon : NNReal) * sampledPureObservedDeviationVarianceProxy arms gamma : NNReal)) : Real) * budget) <= (Finset.range horizon).sum (fun i => sampledTrajectoryPurePredictableMinusObservedAt arms eta gamma loss i sample)} <= ENNReal.ofReal (Real.exp (-budget))

Delta-shaped lower-tail counterpart in the sign needed by the generated predictable EXP3 regret decomposition.

theorem sampledPurePredictableMinusObserved_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 | sampledPureObservedDeviationConfidenceRadius arms gamma horizon delta <= (Finset.range horizon).sum (fun i => sampledTrajectoryPurePredictableLossAt arms eta gamma loss i sample - sampledTrajectoryPureObservedLossAt arms eta gamma i sample)} <= ENNReal.ofReal delta