BanditRLProof.Exp3PredictableIntegration

The pure exponential-weights probability used by Hedge at an actual sampled-trajectory time.

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

Measurable finite-distribution source for the pure Hedge probabilities at every actual trajectory time.

noncomputable def sampledTrajectoryPureProbabilitySourceAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (t : Nat) : MeasurableFiniteActionDistribution arms (sampledTrajectoryPureProbabilityAt (Env

Pure-Hedge predictable loss at one actual trajectory time.

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

Exploration-mixed predictable loss at one actual trajectory time.

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

The pure-Hedge mixed observed estimator at one actual trajectory time.

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

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

theorem measurable_sampledTrajectoryPurePredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (loss : PredictableLossVector Env Action) (t : Nat) : Measurable (sampledTrajectoryPurePredictableLossAt arms eta gamma loss t)

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

theorem sampledTrajectoryPurePredictableLossAt_mem_unitInterval {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledTrajectoryPurePredictableLossAt arms eta gamma loss t sample ∈ Set.Icc (0 : Real) 1

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

theorem integrable_sampledTrajectoryPurePredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (loss : PredictableLossVector Env Action) (t : Nat) : Integrable (sampledTrajectoryPurePredictableLossAt arms eta gamma loss t) mu

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

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

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

theorem sampledTrajectoryExploredPredictableLossAt_mem_unitInterval {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)) : sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample ∈ Set.Icc (0 : Real) 1

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

theorem integrable_sampledTrajectoryExploredPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) : Integrable (sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t) mu

The observed scalar reward can be replaced almost surely by its selected predictable coordinate inside the pure-Hedge mixed estimator.

theorem sampledTrajectoryPureObservedLossAt_ae_eq_weightedPredictable {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment (fun sample => sampledTrajectoryPureObservedLossAt arms eta gamma t sample) =ᵐ[mu] (fun sample => weightedImportanceWeightedLoss arms (sampledTrajectoryProbabilityAt arms eta gamma t sample) (sampledTrajectoryPureProbabilityAt arms eta gamma t sample) (predictableLossAt loss t sample) (sample.2 t).1)

The pure-Hedge observed mixed estimator is integrable on the generated trajectory law.

theorem integrable_sampledTrajectoryPureObservedLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (t : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment Integrable (sampledTrajectoryPureObservedLossAt arms eta gamma t) mu

At time zero, the pure-Hedge mixed observed estimator has the same integral as the pure-Hedge predictable loss.

theorem sampledPredictablePureObservedInitial_integral_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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 integral mu (sampledTrajectoryPureObservedLossAt arms eta gamma 0) = integral mu (sampledTrajectoryPurePredictableLossAt arms eta gamma loss 0)

At a successor time, the pure-Hedge mixed observed estimator has the same integral as the pure-Hedge predictable loss.

theorem sampledPredictablePureObservedSuccessor_integral_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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 integral mu (sampledTrajectoryPureObservedLossAt arms eta gamma (n + 1)) = integral mu (sampledTrajectoryPurePredictableLossAt arms eta gamma loss (n + 1))

Every actual time satisfies the adaptive pure-Hedge first-moment identity.

theorem sampledPredictablePureObservedAt_integral_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (t : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment integral mu (sampledTrajectoryPureObservedLossAt arms eta gamma t) = integral mu (sampledTrajectoryPurePredictableLossAt arms eta gamma loss t)

The adaptive pure-Hedge first-moment identity summed over a finite horizon.

theorem sampledPredictablePureObserved_finiteHorizon_integral_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryPureObservedLossAt arms eta gamma t sample)) = integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryPurePredictableLossAt arms eta gamma loss t sample))

The a.e. sampled-Hedge inequality with its pure estimator-square term replaced by the exploration-mixed square.

theorem sampledPredictableTrajectoryMeasure_hedge_exploredSecondMoment_le_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment ∀ᵐ sample ∂mu, (Finset.range horizon).sum (fun t => sampledTrajectoryPureObservedLossAt arms eta gamma t sample) - (Finset.range horizon).sum (fun t => observedImportanceWeightedLossAt arms eta gamma t sample comparator) <= Real.log arms.card / eta + (eta * (1 / (1 - gamma))) * (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample)

Integrated sampled-Hedge control with the exploration-mixed second moment on the generated predictable trajectory law.

theorem sampledPredictable_integral_pureHedge_le_exploredSecondMoment {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryPureObservedLossAt arms eta gamma t sample)) - integral mu (fun sample => (Finset.range horizon).sum (fun t => observedImportanceWeightedLossAt arms eta gamma t sample comparator)) <= Real.log arms.card / eta + (eta * (1 / (1 - gamma))) * integral mu (fun sample => (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample))

Expected exploration-mixed predictable loss is at most expected pure predictable loss plus `gamma` per round.

theorem sampledPredictable_integral_exploredLoss_le_pure_add_gamma {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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_nonneg : 0 <= gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_lt_one.le loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample)) <= integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryPurePredictableLossAt arms eta gamma loss t sample)) + gamma * (horizon : Real)

The explored probability-mixed estimator square has expectation at most `|arms| * horizon` under predictable `[0,1]` losses.

theorem sampledPredictableObserved_finiteHorizon_secondMoment_integral_le_card_mul {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample)) <= (arms.card : Real) * (horizon : Real)

Unoptimized expected predictable EXP3 regret bound. This is the first complete generated-trajectory theorem on the route; eta/gamma optimization is kept as a separate deterministic parameter leaf.

theorem sampledPredictable_expectedRegret_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace 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) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= Real.log arms.card / eta + (eta * (1 / (1 - gamma))) * ((arms.card : Real) * (horizon : Real)) + gamma * (horizon : Real)