BanditRLProof.Exp3SampledHistoryScore

Remove the newest coordinate from an inclusive successor pair history.

def previousPairHistory {Action : Type u} {n : Nat} (history : History.FinitePairHistory Action Real (n + 1)) : History.FinitePairHistory Action Real n

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

theorem measurable_previousPairHistory {Action : Type u} [MeasurableSpace Action] {n : Nat} : Measurable (previousPairHistory (Action

Measurability of one importance-weighted coordinate when only the sampled action and its scalar observed loss are available.

theorem measurable_observedImportanceWeightedLoss {History : Type*} {Action : Type u} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (prob : History -> Action -> Real) (chosen : History -> Action) (observedLoss : History -> Real) (action : Action) (hprob : Measurable (fun history => prob history action)) (hchosen : Measurable chosen) (hloss : Measurable observedLoss) : Measurable (fun history => importanceWeightedLoss (prob history) (fun _ => observedLoss history) (chosen history) action)

The cumulative sampled importance-weighted loss through an inclusive history. At time zero the estimator uses the initial action law. At time `n + 1`, it uses the exploration-mixed law generated from the score on the prefix through `n`, exactly matching `HistoryAlgorithm.policy n`.

noncomputable def sampledHistoryScore {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) : (n : Nat) -> History.FinitePairHistory Action Real n -> Action -> Real | 0, history, action => importanceWeightedLoss (initialExploredDistribution arms eta gamma) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action | n + 1, history, action => let previous := previousPairHistory history sampledHistoryScore arms eta gamma n previous action + importanceWeightedLoss (exploredHistoryDistribution arms eta gamma (sampledHistoryScore arms eta gamma n) previous) (fun _ => (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).1 action @[simp] theorem sampledHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledHistoryScore arms eta gamma 0 history action = importanceWeightedLoss (initialExploredDistribution arms eta gamma) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action

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

theorem sampledHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledHistoryScore arms eta gamma 0 history action = importanceWeightedLoss (initialExploredDistribution arms eta gamma) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action

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

theorem sampledHistoryScore_succ {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (n : Nat) (history : History.FinitePairHistory Action Real (n + 1)) (action : Action) : sampledHistoryScore arms eta gamma (n + 1) history action = sampledHistoryScore arms eta gamma n (previousPairHistory history) action + importanceWeightedLoss (exploredHistoryDistribution arms eta gamma (sampledHistoryScore arms eta gamma n) (previousPairHistory history)) (fun _ => (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).1 action

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

theorem measurable_sampledHistoryScore {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) : forall n action, action ∈ arms -> Measurable (fun history : History.FinitePairHistory Action Real n => sampledHistoryScore arms eta gamma n history action)

The concrete sampled score satisfies the generic measurable-score API.

theorem measurableFiniteHistoryScore_sampledHistoryScore {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) : MeasurableFiniteHistoryScore arms (sampledHistoryScore arms eta gamma) where

Concrete exploration-mixed probabilities generated by sampled losses.

noncomputable def sampledHistoryDistribution {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (n : Nat) : History.FinitePairHistory Action Real n -> Action -> Real

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

theorem sampledHistoryDistribution_floor {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_le_one : gamma <= 1) (n : Nat) (history : History.FinitePairHistory Action Real n) (action : Action) : gamma / (arms.card : Real) <= sampledHistoryDistribution arms eta gamma n history action

The concrete stochastic history algorithm for sampled-loss EXP3.

noncomputable def sampledImportanceWeightedHistoryAlgorithm {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) : Thompson.HistoryAlgorithm Action Real

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

theorem sampledImportanceWeightedHistoryAlgorithm_policy {Action : Type u} [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) : (sampledImportanceWeightedHistoryAlgorithm arms harms eta gamma hgamma_nonneg hgamma_le_one).policy n = 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)

Complete recursive sampled-loss EXP3 trajectory kernel.

noncomputable def sampledImportanceWeightedTrajectoryKernel {Env : Type w} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] [Nonempty Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) : Kernel Env ((n : Nat) -> Action × Real)

Every successor action of the concrete sampled-loss EXP3 trajectory has the exploration-mixed law generated from its recursively accumulated importance-weighted score.

theorem sampledImportanceWeightedTrajectoryMeasure_condDistrib_action {Env : Type w} {Action : Type u} [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) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (n : Nat) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).1) (fun sample => Preorder.frestrictLe n sample.2) (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one environment) =ᵐ[ (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one environment).map (fun sample => 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)