BanditRLProof.Exp3RecursiveTrajectory

Exponential weight generated by a finite-history cumulative score.

noncomputable def historyWeight {Action History : Type*} (eta : Real) (score : History -> Action -> Real) (history : History) (action : Action) : Real

Total exponential weight on the explicit finite support.

noncomputable def historyTotalWeight {Action History : Type*} (arms : Finset Action) (eta : Real) (score : History -> Action -> Real) (history : History) : Real

Normalized exponential history policy before explicit exploration mixing.

noncomputable def normalizedHistoryDistribution {Action History : Type*} (arms : Finset Action) (eta : Real) (score : History -> Action -> Real) (history : History) (action : Action) : Real

EXP3 policy: normalized exponential weights mixed with uniform exploration.

noncomputable def exploredHistoryDistribution {Action History : Type*} (arms : Finset Action) (eta gamma : Real) (score : History -> Action -> Real) (history : History) (action : Action) : Real

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

theorem historyTotalWeight_pos {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : History -> Action -> Real) (history : History) : 0 < historyTotalWeight arms eta score history

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

theorem normalizedHistoryDistribution_nonneg {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : History -> Action -> Real) (history : History) (action : Action) : 0 <= normalizedHistoryDistribution arms eta score history action

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

theorem sum_normalizedHistoryDistribution {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : History -> Action -> Real) (history : History) : arms.sum (normalizedHistoryDistribution arms eta score history) = 1

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

theorem exploredHistoryDistribution_nonneg {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : History -> Action -> Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (history : History) (action : Action) : 0 <= exploredHistoryDistribution arms eta gamma score history action

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

theorem sum_exploredHistoryDistribution {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : History -> Action -> Real) (history : History) : arms.sum (exploredHistoryDistribution arms eta gamma score history) = 1

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

theorem exploredHistoryDistribution_floor {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : History -> Action -> Real) (hgamma_le_one : gamma <= 1) (history : History) (action : Action) : gamma / (arms.card : Real) <= exploredHistoryDistribution arms eta gamma score history action

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

theorem explorationFloor_pos {Action : Type*} (arms : Finset Action) (harms : arms.Nonempty) (gamma : Real) (hgamma_pos : 0 < gamma) : 0 < gamma / (arms.card : Real)

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

theorem finiteActionDistribution_exploredHistoryDistribution {Action History : Type*} (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : History -> Action -> Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (history : History) : FiniteActionDistribution arms (exploredHistoryDistribution arms eta gamma score history) where

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

theorem measurable_historyWeight {Action History : Type*} [MeasurableSpace History] (eta : Real) (score : History -> Action -> Real) (action : Action) (hscore : Measurable (fun history => score history action)) : Measurable (fun history => historyWeight eta score history action)

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

theorem measurable_historyTotalWeight {Action History : Type*} [MeasurableSpace History] (arms : Finset Action) (eta : Real) (score : History -> Action -> Real) (hscore : forall action, action ∈ arms -> Measurable (fun history => score history action)) : Measurable (historyTotalWeight arms eta score)

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

theorem measurable_normalizedHistoryDistribution {Action History : Type*} [MeasurableSpace History] (arms : Finset Action) (eta : Real) (score : History -> Action -> Real) (hscore : forall action, action ∈ arms -> Measurable (fun history => score history action)) (action : Action) (haction : action ∈ arms) : Measurable (fun history => normalizedHistoryDistribution arms eta score history action)

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

theorem measurable_exploredHistoryDistribution {Action History : Type*} [MeasurableSpace History] (arms : Finset Action) (eta gamma : Real) (score : History -> Action -> Real) (hscore : forall action, action ∈ arms -> Measurable (fun history => score history action)) (action : Action) (haction : action ∈ arms) : Measurable (fun history => exploredHistoryDistribution arms eta gamma score history action)

Coordinate measurability for a score indexed by inclusive pair histories.

structure MeasurableFiniteHistoryScore {Action : Type u} {Loss : Type v} [MeasurableSpace Action] [MeasurableSpace Loss] (arms : Finset Action) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) : Prop where

The un-explored normalized exponential-weights policy supplies measurable probability vectors on every finite-history level.

def normalizedHistoryDistributionSource {Action : Type u} {Loss : Type v} [MeasurableSpace Action] [MeasurableSpace Loss] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (n : Nat) : MeasurableFiniteActionDistribution arms (normalizedHistoryDistribution arms eta (score n)) where

The exploration-mixed history policy supplies measurable probability vectors.

def exploredHistoryDistributionSource {Action : Type u} {Loss : Type v} [MeasurableSpace Action] [MeasurableSpace Loss] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (n : Nat) : MeasurableFiniteActionDistribution arms (exploredHistoryDistribution arms eta gamma (score n)) where

Initial EXP3 probabilities, obtained from zero cumulative scores.

noncomputable def initialExploredDistribution {Action : Type u} (arms : Finset Action) (eta gamma : Real) : Action -> Real

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

theorem finiteActionDistribution_initialExploredDistribution {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) : FiniteActionDistribution arms (initialExploredDistribution arms eta gamma)

Stochastic finite-history algorithm generated by the EXP3 score policy.

noncomputable def exploredHistoryAlgorithm {Action : Type u} {Loss : Type v} [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Loss] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) : Thompson.HistoryAlgorithm Action Loss where

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

theorem exploredHistoryAlgorithm_policy {Action : Type u} {Loss : Type v} [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Loss] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (n : Nat) : (exploredHistoryAlgorithm arms harms eta gamma score hscore hgamma_nonneg hgamma_le_one).policy n = finiteActionKernel arms (exploredHistoryDistribution arms eta gamma (score n)) (exploredHistoryDistributionSource arms harms eta gamma score hscore hgamma_nonneg hgamma_le_one n)

Complete environment-indexed recursive EXP3 action/loss trajectory kernel.

noncomputable def exploredTrajectoryKernel {Env : Type w} {Action : Type u} {Loss : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Loss] [Nonempty Action] [Nonempty Loss] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (environment : Thompson.MeasurableHistoryEnvironment Env Action Loss) : Kernel Env ((n : Nat) -> Action × Loss)

Every successor action of the recursive trajectory has the explicit exploration-mixed EXP3 policy as its conditional law given the finite history.

theorem exploredTrajectoryMeasure_condDistrib_action {Env : Type w} {Action : Type u} {Loss : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Loss] [StandardBorelSpace Loss] [Nonempty Loss] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (score : (n : Nat) -> History.FinitePairHistory Action Loss n -> Action -> Real) (hscore : MeasurableFiniteHistoryScore arms score) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (environment : Thompson.MeasurableHistoryEnvironment Env Action Loss) (n : Nat) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Loss) => (sample.2 (n + 1)).1) (fun sample => Preorder.frestrictLe n sample.2) (prior ⊗ₘ exploredTrajectoryKernel arms harms eta gamma score hscore hgamma_nonneg hgamma_le_one environment) =ᵐ[ (prior ⊗ₘ exploredTrajectoryKernel arms harms eta gamma score hscore hgamma_nonneg hgamma_le_one environment).map (fun sample => Preorder.frestrictLe n sample.2)] finiteActionKernel arms (exploredHistoryDistribution arms eta gamma (score n)) (exploredHistoryDistributionSource arms harms eta gamma score hscore hgamma_nonneg hgamma_le_one n)