BanditRLProof.Exp3RealizedPredictableVariance

Exact centered second moment of a bounded loss under a finite action law.

noncomputable def selectedLossCenteredSecondMoment {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_selectedLossCenteredSecondMoment {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 (selectedLossCenteredSecondMoment arms prob loss)

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

theorem selectedLossCenteredSecondMoment_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 ≤ selectedLossCenteredSecondMoment arms prob loss history

A probability-weighted centered second moment of `[0,1]` losses is at most one.

theorem selectedLossCenteredSecondMoment_le_one {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (prob loss : History → Action → Real) (history : History) (hdist : FiniteActionDistribution arms (prob history)) (hloss : ∀ action ∈ arms, loss history action ∈ Set.Icc (0 : Real) 1) : selectedLossCenteredSecondMoment arms prob loss history ≤ 1

For `[0,1]` losses, the exact selected-loss variance is at most the unweighted armwise loss mass.

theorem selectedLossCenteredSecondMoment_le_lossMass {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (prob loss : History → Action → Real) (history : History) (hdist : FiniteActionDistribution arms (prob history)) (hloss : ∀ action ∈ arms, loss history action ∈ Set.Icc (0 : Real) 1) : selectedLossCenteredSecondMoment arms prob loss history ≤ arms.sum fun action => loss history action

Fixed-tilt MGF budget retaining the exact selected-loss variance.

theorem finiteActionSelectedLossDeviation_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_one : tilt ≤ 1) : let mean := arms.sum fun action => prob history action * loss history action Concentration.HasMGFUpperBoundAt (fun selected => loss history selected - mean) tilt (tilt ^ 2 * selectedLossCenteredSecondMoment arms prob loss history) (finiteActionMeasure arms (prob history))

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

theorem finiteActionSelectedLossDeviation_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_one : tilt ≤ 1) : let mean := arms.sum fun action => prob history action * loss history action Concentration.HasMGFUpperBoundAt (fun selected => tilt * (loss history selected - mean) - tilt ^ 2 * selectedLossCenteredSecondMoment arms prob loss history) 1 0 (finiteActionMeasure arms (prob history))

Exact selected-loss predictable variance at an actual generated time.

noncomputable def sampledTrajectoryPredictableRealizedVarianceAt {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_sampledTrajectoryPredictableRealizedVarianceAt {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 (sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t)

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

theorem sampledTrajectoryPredictableRealizedVarianceAt_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 ≤ sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t sample

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

theorem sampledTrajectoryPredictableRealizedVarianceAt_le_lossMassAt {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)) : sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t sample ≤ arms.sum fun action => predictableLossAt loss t sample action

Every generated selected-loss predictable variance is at most one.

theorem sampledTrajectoryPredictableRealizedVarianceAt_le_one {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)) : sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t sample ≤ 1

An identified finite conditional action law supplies a zero-budget MGF for the exact selected-loss variance-compensated increment.

theorem selectedLossDeviation_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) (hloss : Measurable (fun input : History × Action => loss input.1 input.2)) (hloss_mem : ∀ history action, loss history action ∈ Set.Icc (0 : Real) 1) (tilt : Real) (htilt_nonneg : 0 ≤ tilt) (htilt_le_one : tilt ≤ 1) (hcond : condDistrib action history mu =ᵐ[mu.map history] finiteActionKernel arms prob source) : let mean := fun h => arms.sum fun candidate => prob h candidate * loss h candidate Concentration.HasCondMGFUpperBoundAt (mHistory.comap history) hhistory.comap_le (fun omega => tilt * (loss (history omega) (action omega) - mean (history omega)) - tilt ^ 2 * selectedLossCenteredSecondMoment arms prob loss (history omega)) 1 0 mu

Initial generated selected-loss increment with its exact predictable variance compensation.

theorem sampledPredictableSelectedLossCompensated_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_one : tilt ≤ 1) : 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 * sampledTrajectorySelectedDeviationAt arms eta gamma loss 0 sample - tilt ^ 2 * sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss 0 sample) 1 0 mu

Successor generated selected-loss increment with its exact predictable variance compensation.

theorem sampledPredictableSelectedLossCompensated_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_one : tilt ≤ 1) : 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 * sampledTrajectorySelectedDeviationAt arms eta gamma loss (n + 1) sample - tilt ^ 2 * sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss (n + 1) sample) 1 0 mu

The deterministic-feedback realization transports the initial selected loss compensation to the observed realized-loss increment.

theorem sampledPredictableRealizedCompensated_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_one : tilt ≤ 1) : 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 * sampledTrajectoryRealizedDeviationAt arms eta gamma loss 0 sample - tilt ^ 2 * sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss 0 sample) 1 0 mu

The deterministic-feedback realization transports each successor selected loss compensation to the observed realized-loss increment.

theorem sampledPredictableRealizedCompensated_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_one : tilt ≤ 1) : 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 * sampledTrajectoryRealizedDeviationAt arms eta gamma loss (n + 1) sample - tilt ^ 2 * sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss (n + 1) sample) 1 0 mu

Shift actual-time selected-loss variances by one so that the process is predictable for the generated deviation filtration.

noncomputable def sampledPredictableRealizedVarianceProcess {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 => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample theorem measurable_sampledTrajectoryPredictableRealizedVarianceAt_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] (sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t)

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

theorem measurable_sampledTrajectoryPredictableRealizedVarianceAt_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] (sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss t)

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

theorem sampledPredictableRealizedVarianceProcess_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) (sampledPredictableRealizedVarianceProcess arms eta gamma loss)

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

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

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

theorem sampledPredictableRealizedVariance_sum_le_lossMass {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) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ (Finset.range horizon).sum (fun i => arms.sum fun action => predictableLossAt loss i sample action)

The first `horizon` generated selected-loss predictable variances have deterministic total budget `horizon`.

theorem sampledPredictableRealizedVariance_sum_le_horizon {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) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : (Finset.range horizon).sum (fun i => sampledTrajectoryPredictableRealizedVarianceAt arms eta gamma loss i sample) ≤ (horizon : Real)