BanditRLProof.Exp3PredictableMoments

Mixing fixed-environment trajectory laws preserves a history-dependent output kernel when the conditioning variable retains the environment coordinate.

theorem trajectoryMixture_map_environment_history_output_eq_compProd {Env : Type u} {Omega : Type v} {History : Type w} {Output : Type x} [MeasurableSpace Env] [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Output] (prior : Measure Env) [IsFiniteMeasure prior] (trajectory : Kernel Env Omega) [IsMarkovKernel trajectory] (history : Omega -> History) (hhistory : Measurable history) (output : Omega -> Output) (houtput : Measurable output) (outputKernel : Kernel (Env × History) Output) [IsMarkovKernel outputKernel] (hlaw : forall env, (trajectory env).map (fun omega => (history omega, output omega)) = (trajectory env).map history ⊗ₘ outputKernel.comap (fun h => (env, h)) (measurable_const.prodMk measurable_id)) : (prior ⊗ₘ trajectory).map (fun sample : Env × Omega => ((sample.1, history sample.2), output sample.2)) = (prior ⊗ₘ trajectory).map (fun sample : Env × Omega => (sample.1, history sample.2)) ⊗ₘ outputKernel

The canonical measurable trajectory, mixed over an environment prior, has the joint law obtained by adjoining one global measurable history-step kernel to the retained environment/prefix history.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_map_environment_prefix_next_eq_compProd {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Reward) (environment : Thompson.MeasurableHistoryEnvironment Env Action Reward) (n : Nat) : (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => ((sample.1, Preorder.frestrictLe n sample.2), sample.2 (n + 1))) = (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.1, Preorder.frestrictLe n sample.2)) ⊗ₘ Thompson.measurableEnvironmentHistoryStepKernel algorithm environment n

Conditional on the latent environment and the preceding finite pair history, the next canonical trajectory pair follows the global measurable history-step kernel.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_condDistrib_nextPair_given_environment_prefix {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Reward) (environment : Thompson.MeasurableHistoryEnvironment Env Action Reward) (n : Nat) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Reward) => sample.2 (n + 1)) (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.1, Preorder.frestrictLe n sample.2)) (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment) =ᵐ[ (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.1, Preorder.frestrictLe n sample.2))] Thompson.measurableEnvironmentHistoryStepKernel algorithm environment n

The sampled EXP3 distribution viewed on a retained environment/prefix history.

noncomputable def sampledEnvironmentHistoryDistributionSource {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) (n : Nat) : MeasurableFiniteActionDistribution arms (fun input : Env × History.FinitePairHistory Action Real n => sampledHistoryDistribution arms eta gamma n input.2) where

Predictable successor losses satisfy the regularity contract required by the EXP3 conditional first- and second-moment transport layer.

theorem sampledPredictableSuccessorLossRegularity {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) (n : Nat) : BoundedMeasurableLossWithProbabilityFloor arms (fun input : Env × History.FinitePairHistory Action Real n => sampledHistoryDistribution arms eta gamma n input.2) (fun input : Env × History.FinitePairHistory Action Real n => loss.successor n input.1 input.2) (gamma / (arms.card : Real)) where

The time-zero sampled EXP3 distribution viewed as a constant kernel on environments.

noncomputable def sampledInitialEnvironmentDistributionSource {Env : Type u} {Action : Type v} [MeasurableSpace Env] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) : MeasurableFiniteActionDistribution arms (fun _env : Env => initialExploredDistribution arms eta gamma) where

Initial predictable losses satisfy the sampled EXP3 regularity contract.

theorem sampledPredictableInitialLossRegularity {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) : BoundedMeasurableLossWithProbabilityFloor arms (fun _env : Env => initialExploredDistribution arms eta gamma) loss.initial (gamma / (arms.card : Real)) where

Mixing the canonical trajectory through a prior preserves its global initial-pair law.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_map_environment_eval_zero {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [Nonempty Action] [MeasurableSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Reward) (environment : Thompson.MeasurableHistoryEnvironment Env Action Reward) : (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.1, sample.2 0)) = prior ⊗ₘ Thompson.measurableEnvironmentInitialPairKernel algorithm environment

The prior-mixed canonical trajectory retains the environment beside its initial action law.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_map_environment_action_zero {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [Nonempty Action] [MeasurableSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Reward) (environment : Thompson.MeasurableHistoryEnvironment Env Action Reward) : (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.1, (sample.2 0).1)) = prior ⊗ₘ Kernel.const Env algorithm.initialAction

Conditional on the retained environment, the canonical initial action follows `initialAction`.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_condDistrib_action_zero_given_environment {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Reward) (environment : Thompson.MeasurableHistoryEnvironment Env Action Reward) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.2 0).1) (fun sample : Env × ((k : Nat) -> Action × Reward) => sample.1) (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment) =ᵐ[ (prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample : Env × ((k : Nat) -> Action × Reward) => sample.1)] Kernel.const Env algorithm.initialAction

Under predictable deterministic feedback, the observed initial reward is the initial loss-vector coordinate selected by the initial action.

theorem canonicalPredictableTrajectoryMeasure_reward_zero_eq_initialLoss_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [Nonempty Action] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Real) (loss : PredictableLossVector Env Action) : (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 0).2) =ᵐ[ prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm loss.environment] (fun sample : Env × ((k : Nat) -> Action × Real) => loss.initial sample.1 (sample.2 0).1)

The time-zero sampled EXP3 estimator has the observed-scalar armwise first moment and exact probability-mixed estimator-square moment.

theorem sampledPredictableObservedInitial_first_second_moment {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) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment let prob := initialExploredDistribution arms eta gamma (integral mu (fun sample => importanceWeightedLoss prob (fun _ => (sample.2 0).2) (sample.2 0).1 comparator) = integral prior (fun env => loss.initial env comparator)) ∧ (integral mu (fun sample => mixedSquaredImportanceWeightedLoss arms prob (fun _ => (sample.2 0).2) (sample.2 0).1) = integral prior (fun env => arms.sum (fun action => (loss.initial env action) ^ 2)))

Under predictable deterministic feedback, the observed successor reward is the loss-vector coordinate selected by the action in the same successor pair.

theorem canonicalPredictableTrajectoryMeasure_reward_eq_successorLoss_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : Thompson.HistoryAlgorithm Action Real) (loss : PredictableLossVector Env Action) (n : Nat) : (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).2) =ᵐ[ prior ⊗ₘ Thompson.canonicalMeasurableEnvironmentTrajectoryKernel algorithm loss.environment] (fun sample : Env × ((k : Nat) -> Action × Real) => loss.successor n sample.1 (Preorder.frestrictLe n sample.2) (sample.2 (n + 1)).1)

Concrete sampled-loss EXP3 observes exactly the selected predictable successor loss in every round, almost surely under the environment/trajectory mixture.

theorem sampledPredictableTrajectoryMeasure_reward_eq_successorLoss_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) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (n : Nat) : (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).2) =ᵐ[ prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment] (fun sample : Env × ((k : Nat) -> Action × Real) => loss.successor n sample.1 (Preorder.frestrictLe n sample.2) (sample.2 (n + 1)).1)

The concrete sampled EXP3 successor round has the armwise unbiased first moment and the exact probability-mixed estimator-square moment for every predictable loss vector with positive exploration.

theorem sampledPredictableSuccessorLoss_first_second_moment {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) (comparator : Action) (hcomparator : comparator ∈ arms) : 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) let prob := fun input : Env × History.FinitePairHistory Action Real n => sampledHistoryDistribution arms eta gamma n input.2 let roundLoss := fun input : Env × History.FinitePairHistory Action Real n => loss.successor n input.1 input.2 (integral mu (fun sample => importanceWeightedLoss (prob (history sample)) (roundLoss (history sample)) (sample.2 (n + 1)).1 comparator) = integral (mu.map history) (fun input => roundLoss input comparator)) ∧ (integral mu (fun sample => mixedSquaredImportanceWeightedLoss arms (prob (history sample)) (roundLoss (history sample)) (sample.2 (n + 1)).1) = integral (mu.map history) (fun input => arms.sum (fun action => (roundLoss input action) ^ 2)))

Observed-scalar form of the sampled EXP3 roundwise moment theorem. The score uses only the reward coordinate stored in the generated trajectory; the right sides expose the full predictable loss vector required by regret analysis.

theorem sampledPredictableObservedSuccessor_first_second_moment {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) (comparator : Action) (hcomparator : comparator ∈ arms) : 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) let prob := fun input : Env × History.FinitePairHistory Action Real n => sampledHistoryDistribution arms eta gamma n input.2 let roundLoss := fun input : Env × History.FinitePairHistory Action Real n => loss.successor n input.1 input.2 (integral mu (fun sample => importanceWeightedLoss (prob (history sample)) (fun _ => (sample.2 (n + 1)).2) (sample.2 (n + 1)).1 comparator) = integral (mu.map history) (fun input => roundLoss input comparator)) ∧ (integral mu (fun sample => mixedSquaredImportanceWeightedLoss arms (prob (history sample)) (fun _ => (sample.2 (n + 1)).2) (sample.2 (n + 1)).1) = integral (mu.map history) (fun input => arms.sum (fun action => (roundLoss input action) ^ 2)))

Sampling probabilities used by the concrete trajectory at every actual time index.

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

Predictable loss vector selected before the action at every actual time index.

def predictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action -> Real

The scalar-feedback importance-weighted coordinate used at an actual time.

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

The scalar-feedback probability-mixed estimator square used at an actual time.

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

Measurable finite-action source for the sampled probability vector at any time.

noncomputable def sampledTrajectoryProbabilitySourceAt {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) (t : Nat) : MeasurableFiniteActionDistribution arms (sampledTrajectoryProbabilityAt (Env

Predictable trajectory losses satisfy one uniform regularity interface at every time.

theorem sampledPredictableTrajectoryLossRegularityAt {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) : BoundedMeasurableLossWithProbabilityFloor arms (sampledTrajectoryProbabilityAt (Env

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

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

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

theorem measurable_observedImportanceWeightedLossAt {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) (t : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : Measurable (observedImportanceWeightedLossAt (Env

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

theorem measurable_observedMixedSquaredImportanceWeightedLossAt {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) (t : Nat) : Measurable (observedMixedSquaredImportanceWeightedLossAt (Env

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

theorem integrable_predictableImportanceWeightedLossAt {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_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) (comparator : Action) (hcomparator : comparator ∈ arms) : let prob := sampledTrajectoryProbabilityAt (Env := Env) arms eta gamma t let roundLoss := predictableLossAt loss t Integrable (fun sample => importanceWeightedLoss (prob sample) (roundLoss sample) (sample.2 t).1 comparator) mu

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

theorem integrable_predictableMixedSquaredImportanceWeightedLossAt {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_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) : let prob := sampledTrajectoryProbabilityAt (Env := Env) arms eta gamma t let roundLoss := predictableLossAt loss t Integrable (fun sample => mixedSquaredImportanceWeightedLoss arms (prob sample) (roundLoss sample) (sample.2 t).1) mu

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

theorem integrable_predictableLossAt {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) (action : Action) : Integrable (fun sample => predictableLossAt loss t sample action) mu

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

theorem integrable_predictableLossSqSumAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (loss : PredictableLossVector Env Action) (t : Nat) : Integrable (fun sample => arms.sum (fun action => (predictableLossAt loss t sample action) ^ 2)) mu

On the generated predictable trajectory, observed scalar scores agree almost everywhere with their latent predictable-loss counterparts.

theorem observedAt_eq_predictableAt_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) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) (comparator : Action) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ((fun sample => observedImportanceWeightedLossAt arms eta gamma t sample comparator) =ᵐ[mu] (fun sample => importanceWeightedLoss (sampledTrajectoryProbabilityAt arms eta gamma t sample) (predictableLossAt loss t sample) (sample.2 t).1 comparator)) ∧ ((fun sample => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample) =ᵐ[mu] (fun sample => mixedSquaredImportanceWeightedLoss arms (sampledTrajectoryProbabilityAt arms eta gamma t sample) (predictableLossAt loss t sample) (sample.2 t).1))

The two observed score families are integrable under the generated predictable trajectory law at every actual time index.

theorem integrable_observedAt {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) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment Integrable (fun sample => observedImportanceWeightedLossAt arms eta gamma t sample comparator) mu ∧ Integrable (fun sample => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample) mu

At every actual time, including time zero, the observed armwise first moment and probability-mixed estimator-square moment equal the corresponding predictable loss-vector moments on the common full trajectory law.

theorem sampledPredictableObservedAt_first_second_moment {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) (comparator : Action) (hcomparator : comparator ∈ arms) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_le_one loss.environment (integral mu (fun sample => observedImportanceWeightedLossAt arms eta gamma t sample comparator) = integral mu (fun sample => predictableLossAt loss t sample comparator)) ∧ (integral mu (fun sample => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample) = integral mu (fun sample => arms.sum (fun action => (predictableLossAt loss t sample action) ^ 2)))

Finite-horizon observed EXP3 first and mixed-second moments over `t < horizon`; when the horizon is positive this range includes time zero.

theorem sampledPredictableObserved_finiteHorizon_first_second_moment {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) (comparator : Action) (hcomparator : comparator ∈ arms) : 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 => observedImportanceWeightedLossAt arms eta gamma t sample comparator)) = integral mu (fun sample => (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator))) ∧ (integral mu (fun sample => (Finset.range horizon).sum (fun t => observedMixedSquaredImportanceWeightedLossAt arms eta gamma t sample)) = integral mu (fun sample => (Finset.range horizon).sum (fun t => arms.sum (fun action => (predictableLossAt loss t sample action) ^ 2))))