BanditRLProof.Exp3RealizedRegret

The scalar loss realized at an actual generated-trajectory time.

def sampledTrajectoryRealizedLossAt {Env : Type u} {Action : Type v} (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Generated predictable feedback identifies the realized scalar loss with the predictable coordinate selected by the sampled action.

theorem sampledTrajectoryRealizedLossAt_ae_eq_selectedPredictable {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 sampledTrajectoryRealizedLossAt t =ᵐ[mu] (fun sample => predictableLossAt loss t sample (sample.2 t).1)

The selected predictable coordinate is measurable on the full trajectory space, even though the coordinate itself varies with the sampled action.

theorem measurable_sampledTrajectorySelectedPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (t : Nat) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => predictableLossAt loss t sample (sample.2 t).1)

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

theorem sampledTrajectorySelectedPredictableLossAt_mem_unitInterval {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : predictableLossAt loss t sample (sample.2 t).1 ∈ Set.Icc (0 : Real) 1

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

theorem integrable_sampledTrajectorySelectedPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (loss : PredictableLossVector Env Action) (t : Nat) : Integrable (fun sample => predictableLossAt loss t sample (sample.2 t).1) mu

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

theorem integrable_sampledTrajectoryRealizedLossAt {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 Integrable (sampledTrajectoryRealizedLossAt t) mu

At time zero, the expected realized loss is the exploration-distribution mixed predictable loss.

theorem sampledPredictableRealizedInitial_integral_eq_explored {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) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment integral mu (sampledTrajectoryRealizedLossAt 0) = integral mu (sampledTrajectoryExploredPredictableLossAt arms eta gamma loss 0)

At a successor time, conditioning on the retained environment/history prefix converts the expected selected predictable coordinate to the `p_t` finite sum.

theorem sampledPredictableRealizedSuccessor_integral_eq_explored {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) (n : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment integral mu (sampledTrajectoryRealizedLossAt (n + 1)) = integral mu (sampledTrajectoryExploredPredictableLossAt arms eta gamma loss (n + 1))

Every actual time has the realized-to-`p_t`-mixed first-moment identity.

theorem sampledPredictableRealizedAt_integral_eq_explored {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 integral mu (sampledTrajectoryRealizedLossAt t) = integral mu (sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t)

The realized and exploration-mixed predictable cumulative losses have the same expectation over every finite horizon.

theorem sampledPredictableRealized_finiteHorizon_integral_eq_explored {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) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample)) = integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryExploredPredictableLossAt arms eta gamma loss t sample))

Unoptimized expected regret for the scalar losses actually realized by the sampled predictable EXP3 trajectory.

theorem sampledPredictable_realizedExpectedRegret_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 => sampledTrajectoryRealizedLossAt 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)

Tuned large-horizon expected regret for the scalar loss actually realized by the sampled predictable EXP3 trajectory.

theorem sampledPredictable_realizedExpectedRegret_le_four_mul_sqrt {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) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (horizon : Nat) (hhorizon_pos : 0 < horizon) (hscale : 4 * (arms.card : Real) * Real.log arms.card <= (horizon : Real)) (comparator : Action) (hcomparator : comparator ∈ arms) : let K := (arms.card : Real) let T := (horizon : Real) let mu := prior ⊗ₘ tunedPredictableTrajectoryKernel arms harms hcard_two loss horizon hhorizon_pos hscale integral mu (fun sample => (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)) <= 4 * Real.sqrt (K * T * Real.log K)