BanditRLProof.Exp3MixedSquarePredictableVariance

Exact centered second moment of the mixed importance-weighted square under a finite sampling distribution.

noncomputable def mixedSquaredEstimatorCenteredSecondMoment {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (history : History) : Real

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

theorem measurable_mixedSquaredEstimatorCenteredSecondMoment {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Measurable (mixedSquaredEstimatorCenteredSecondMoment arms prob loss)

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

theorem mixedSquaredEstimatorCenteredSecondMoment_nonneg {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (history : History) (hdist : FiniteActionDistribution arms (prob history)) : 0 <= mixedSquaredEstimatorCenteredSecondMoment arms prob loss history

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

theorem mixedSquaredEstimatorCenteredSecondMoment_le_card_div_floor {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 <= (arms.card : Real) / epsilon

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

theorem integral_sq_mixedSquaredEstimatorDeviation_finiteActionMeasure_eq {History : Type u} {Action : Type v} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (history : History) (hdist : FiniteActionDistribution arms (prob history)) : integral (finiteActionMeasure arms (prob history)) (fun chosen => (mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen - arms.sum (fun action => (loss history action) ^ 2)) ^ 2) = mixedSquaredEstimatorCenteredSecondMoment arms prob loss history

Transport the centered mixed-square score law from an identified finite conditional action distribution into the ambient conditional-expectation kernel.

theorem mixedSquaredEstimatorDeviation_condExpKernel_map_eq_finiteActionMeasure_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) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob source) : Filter.Eventually (fun omega => Measure.map (fun y => mixedSquaredImportanceWeightedLoss arms (prob (history y)) (loss (history y)) (action y) - arms.sum (fun candidate => (loss (history y) candidate) ^ 2)) (@condExpKernel Omega mOmega _ mu _ (mHistory.comap history) omega) = Measure.map (fun selected => mixedSquaredImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) selected - arms.sum (fun candidate => (loss (history omega) candidate) ^ 2)) (finiteActionMeasure arms (prob (history omega)))) (ae (mu.trim hhistory.comap_le))

The ambient conditional-expectation kernel integrates the squared centered mixed-square increment to the explicit finite-law centered second moment.

theorem integral_sq_mixedSquaredEstimatorDeviation_condExpKernel_eq_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) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob source) : Filter.Eventually (fun omega => integral (@condExpKernel Omega mOmega _ mu _ (mHistory.comap history) omega) (fun y => (mixedSquaredImportanceWeightedLoss arms (prob (history y)) (loss (history y)) (action y) - arms.sum (fun candidate => (loss (history y) candidate) ^ 2)) ^ 2) = mixedSquaredEstimatorCenteredSecondMoment arms prob loss (history omega)) (ae (mu.trim hhistory.comap_le))

Exact finite-law predictable variance at an actual generated time.

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

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

theorem measurable_sampledTrajectoryPredictableMixedSquaredVarianceAt {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) : Measurable (sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss t)

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

theorem sampledTrajectoryPredictableMixedSquaredVarianceAt_nonneg {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) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : 0 <= sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss t sample

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

theorem sampledTrajectoryPredictableMixedSquaredVarianceAt_le {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 <= (arms.card : Real) / (gamma / (arms.card : Real))

At generated time zero, the ambient conditional-expectation kernel given the environment integrates the squared centered mixed-square increment to the explicit predictable variance.

theorem sampledPredictableMixedSquaredDeviation_zero_condExpKernel_integral_sq_eq_variance {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 Filter.Eventually (fun omega => integral (@condExpKernel (Env × ((k : Nat) -> Action × Real)) inferInstance _ mu _ ((inferInstance : MeasurableSpace Env).comap (fun sample => sample.1)) omega) (fun y => (sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss 0 y) ^ 2) = sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss 0 omega) (ae (mu.trim measurable_fst.comap_le))

At a generated successor time, the ambient conditional-expectation kernel given the environment and preceding finite prefix integrates the squared centered mixed-square increment to the explicit predictable variance.

theorem sampledPredictableMixedSquaredDeviation_succ_condExpKernel_integral_sq_eq_variance {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) Filter.Eventually (fun omega => integral (@condExpKernel (Env × ((k : Nat) -> Action × Real)) inferInstance _ mu _ ((inferInstance : MeasurableSpace (Env × History.FinitePairHistory Action Real n)).comap history) omega) (fun y => (sampledTrajectoryPredictableMixedSquaredDeviationAt arms eta gamma loss (n + 1) y) ^ 2) = sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss (n + 1) omega) (ae (mu.trim (measurable_fst.prodMk ((Preorder.measurable_frestrictLe n).comp measurable_snd)).comap_le))

Shift the actual-time conditional variances by one. The resulting process is predictable for the generated deviation filtration.

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

Every shifted mixed-square increment has conditional square integral equal to the matching shifted predictable variance under the existing generated filtration.

theorem sampledPredictableMixedSquaredDeviationProcess_condExpKernel_integral_sq_eq_varianceProcess {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 Filter.Eventually (fun omega => integral (@condExpKernel (Env × ((k : Nat) -> Action × Real)) inferInstance _ mu _ (sampledPredictableDeviationFiltration Env Action n) omega) (fun y => (sampledPredictableMixedSquaredDeviationProcess arms eta gamma loss (n + 1) y) ^ 2) = sampledPredictableMixedSquaredVarianceProcess arms eta gamma loss (n + 1) omega) (ae (mu.trim ((sampledPredictableDeviationFiltration Env Action).le n)))

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

theorem measurable_sampledTrajectoryPredictableMixedSquaredVarianceAt_filtration {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) : Measurable[sampledPredictableDeviationFiltration Env Action t] (sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss t)

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

theorem sampledPredictableMixedSquaredVarianceProcess_isPredictable {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) : IsPredictable (sampledPredictableDeviationFiltration Env Action) (sampledPredictableMixedSquaredVarianceProcess arms eta gamma loss)

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

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

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

theorem sampledPredictableMixedSquaredVariance_sum_le {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)) : (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableMixedSquaredVarianceAt arms eta gamma loss i sample) <= (horizon : Real) * ((arms.card : Real) / (gamma / (arms.card : Real)))