BanditRLProof.Exp3PredictableAdversary

A measurable adversarial loss-vector family selected before the current action. The successor loss vector may depend on the environment and the preceding pair history, but not on the action sampled at that successor step.

structure PredictableLossVector (Env : Type u) (Action : Type v) [MeasurableSpace Env] [MeasurableSpace Action] where

Deterministic chosen-coordinate feedback generated by a predictable loss family.

noncomputable def PredictableLossVector.environment {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) : Thompson.MeasurableHistoryEnvironment Env Action Real where

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

theorem PredictableLossVector.environment_initialFeedback_apply {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (env : Env) (action : Action) : loss.environment.initialFeedback (env, action) = Measure.dirac (loss.initial env action)

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

theorem PredictableLossVector.environment_feedback_apply {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (n : Nat) (env : Env) (history : History.FinitePairHistory Action Real n) (action : Action) : loss.environment.feedback n (env, (history, action)) = Measure.dirac (loss.successor n env history action)

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

theorem PredictableLossVector.initial_mem_unitInterval {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (env : Env) (action : Action) : loss.initial env action ∈ Set.Icc (0 : Real) 1

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

theorem PredictableLossVector.successor_mem_unitInterval {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (n : Nat) (env : Env) (history : History.FinitePairHistory Action Real n) (action : Action) : loss.successor n env history action ∈ Set.Icc (0 : Real) 1

Mixing fixed-environment trajectory laws preserves a common action kernel when the conditioning variable retains the environment coordinate.

theorem trajectoryMixture_condDistrib_action_given_environment_history {Env : Type u} {Omega : Type v} {History : Type w} {Action : Type x} [MeasurableSpace Env] [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (prior : Measure Env) [IsFiniteMeasure prior] (trajectory : Kernel Env Omega) [IsMarkovKernel trajectory] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (policy : Kernel History Action) [IsMarkovKernel policy] (hlaw : forall env, (trajectory env).map (fun omega => (history omega, action omega)) = (trajectory env).map history ⊗ₘ policy) : condDistrib (action ∘ Prod.snd) (fun sample : Env × Omega => (sample.1, history sample.2)) (prior ⊗ₘ trajectory) =ᵐ[ (prior ⊗ₘ trajectory).map (fun sample : Env × Omega => (sample.1, history sample.2))] policy.comap (fun input : Env × History => input.2) (measurable_snd : Measurable (fun input : Env × History => input.2))

The concrete sampled-score EXP3 action remains independent of the current predictable loss vector after conditioning on the environment and prefix.

theorem sampledImportanceWeightedTrajectoryMeasure_condDistrib_action_given_environment {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) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).1) (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2)) (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment) =ᵐ[ (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment).map (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2))] (finiteActionKernel arms (sampledHistoryDistribution arms eta gamma n) (exploredHistoryDistributionSource arms harms eta gamma (sampledHistoryScore arms eta gamma) (measurableFiniteHistoryScore_sampledHistoryScore arms eta gamma) hgamma_nonneg hgamma_le_one n)).comap (fun input : Env × History.FinitePairHistory Action Real n => input.2) (measurable_snd : Measurable (fun input : Env × History.FinitePairHistory Action Real n => input.2))