BanditRLProof.Algorithms.ThompsonBayesRegretDecomposition

A real score whose time-`n + 1` value sees exactly the history through `n`.

structure HistoryActionScore (Action : Type u) (Reward : Type v) [MeasurableSpace Action] [MeasurableSpace Reward] where

Evaluate a history score on the action selected by one complete trace.

def atTrace {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (action : ActionTrace Action) (reward : RewardTrace Reward) : Nat -> Real | 0 => score.initial (action 0) | n + 1 => score.successor n (History.finitePairHistoryOfTrace action reward n) (action (n + 1)) /-- Evaluate the same visible-history score at a comparison action. -/ def atBestTrace {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (bestAction : Action) (action : ActionTrace Action) (reward : RewardTrace Reward) : Nat -> Real | 0 => score.initial bestAction | n + 1 => score.successor n (History.finitePairHistoryOfTrace action reward n) bestAction theorem measurable_atTrace {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (t : Nat) : Measurable (fun omega => score.atTrace (action omega) (reward omega) t)

Evaluate the same visible-history score at a comparison action.

def atBestTrace {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (bestAction : Action) (action : ActionTrace Action) (reward : RewardTrace Reward) : Nat -> Real | 0 => score.initial bestAction | n + 1 => score.successor n (History.finitePairHistoryOfTrace action reward n) bestAction theorem measurable_atTrace {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (t : Nat) : Measurable (fun omega => score.atTrace (action omega) (reward omega) t)

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

theorem measurable_atTrace {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (t : Nat) : Measurable (fun omega => score.atTrace (action omega) (reward omega) t)

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

theorem measurable_atBestTrace {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (bestAction : Omega -> Action) (hbestAction : Measurable bestAction) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (t : Nat) : Measurable (fun omega => score.atBestTrace (bestAction omega) (action omega) (reward omega) t)

Equal pushforwards give equal integrals of every measurable real score.

theorem integral_comp_eq_of_map_eq {Omega : Type u} {Target : Type v} [MeasurableSpace Omega] [MeasurableSpace Target] (mu : Measure Omega) (left right : Omega -> Target) (hleft : Measurable left) (hright : Measurable right) (hmap : mu.map left = mu.map right) (score : Target -> Real) (hscore : Measurable score) : integral mu (fun omega => score (left omega)) = integral mu (fun omega => score (right omega))

If two actions have the same conditional law given a history, every measurable history/action score has the same expectation under those actions.

theorem integral_historyAction_eq_of_condDistrib_ae_eq {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action bestAction : Omega -> Action) (haction : Measurable action) (hbestAction : Measurable bestAction) (hcond : condDistrib action history mu =ᵐ[mu.map history] condDistrib bestAction history mu) (score : History × Action -> Real) (hscore : Measurable score) : integral mu (fun omega => score (history omega, action omega)) = integral mu (fun omega => score (history omega, bestAction omega))

The environment-indexed trajectory kernel has the algorithm's action law at time zero.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_map_action_zero {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun trajectory => (trajectory 0).1) = Kernel.const Env algorithm.initialAction

Mixing the trajectory kernel through a probability prior preserves its initial action law.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_map_action_zero {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample => (sample.2 0).1) = algorithm.initialAction

The initial action and latent best action have the same marginal on the actual TS trajectory.

theorem uniformReferenceThompsonAlgorithm_map_action_zero_eq_bestAction {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Fintype Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment actualMeasure.map (fun sample => environmentTrajectoryAction sample 0) = actualMeasure.map (bestAction ∘ Prod.fst)

Evaluate the history score on the actual trajectory action.

def trajectoryHistoryScore {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (sample : Env × ((n : Nat) -> Action × Reward)) (t : Nat) : Real

Evaluate the same score at the latent environment's best action.

def trajectoryBestHistoryScore {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Action] [MeasurableSpace Reward] (score : HistoryActionScore Action Reward) (bestAction : Env -> Action) (sample : Env × ((n : Nat) -> Action × Reward)) (t : Nat) : Real

Probability matching on the actual recursive trajectory implies equality of every visible-history score at the selected and latent-best actions.

theorem uniformReferenceThompsonAlgorithm_integral_historyScore_eq_bestAction {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Fintype Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (score : HistoryActionScore Action Reward) (t : Nat) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment integral actualMeasure (fun sample => trajectoryHistoryScore score sample t) = integral actualMeasure (fun sample => trajectoryBestHistoryScore score bestAction sample t)

A selector is mean-optimal when it maximizes the environment-dependent action mean pointwise. This contract separates a genuine best-action regret interpretation from the comparator-relative algebra below.

def IsOptimalMeanSelector {Env : Type u} {Action : Type v} (mean : Env -> Action -> Real) (bestAction : Env -> Action) : Prop

Finite-horizon comparator-relative mean regret. It is Bayesian pseudo-regret when `bestAction` satisfies `IsOptimalMeanSelector mean bestAction` and the environment is integrated against a prior.

def trajectoryBayesMeanRegret {Env : Type u} {Action : Type v} {Reward : Type w} (mean : Env -> Action -> Real) (bestAction : Env -> Action) (sample : Env × ((n : Nat) -> Action × Reward)) (horizon : Nat) : Real

LML-shaped Thompson Bayesian regret decomposition on the locally generated recursive trajectory. Integrability is explicit; bounded clipped scores and bounded action means can discharge these four contracts downstream.

theorem integral_trajectoryBayesMeanRegret_eq_add_historyScore {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Fintype Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (mean : Env -> Action -> Real) (score : HistoryActionScore Action Reward) (horizon : Nat) (hmeanBest : Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => mean sample.1 (bestAction sample.1)) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hmeanAction : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => mean sample.1 (environmentTrajectoryAction sample t)) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hscoreAction : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => trajectoryHistoryScore score sample t) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hscoreBest : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => trajectoryBestHistoryScore score bestAction sample t) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment integral actualMeasure (fun sample => trajectoryBayesMeanRegret mean bestAction sample horizon) = integral actualMeasure (fun sample => ∑ t ∈ range horizon, (mean sample.1 (bestAction sample.1) - trajectoryBestHistoryScore score bestAction sample t)) + integral actualMeasure (fun sample => ∑ t ∈ range horizon, (trajectoryHistoryScore score sample t - mean sample.1 (environmentTrajectoryAction sample t)))