Lean module · EXP3
BanditRLProof.Exp3RecursiveTrajectory
# Recursive measurable EXP3 trajectories This module turns a measurable finite-history score into the exploration-mixed exponential policy used by EXP3. It proves normalization, coordinate measurability, and a uniform exploration floor, packages the policy as the project's stochastic finite-history algorithm, and invokes the Mathlib-backed Ionescu--Tulcea trajectory kernel. The resulting theorem identifies every successor action's conditional law with the explicit finite-action policy. The score is an input contract here. Constructing it recursively from sampled importance-weighted losses is the next layer of the EXP3 route.
Module map
Imports
BanditRLProof.Exp3ScoreRegularity, BanditRLProof.Algorithms.ThompsonRecursiveSampler
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.historyWeight
Compiled
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
def
BanditRLProof.Exp3.historyTotalWeight
Compiled
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
def
BanditRLProof.Exp3.normalizedHistoryDistribution
Compiled
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
def
BanditRLProof.Exp3.exploredHistoryDistribution
Compiled
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
theorem
BanditRLProof.Exp3.historyTotalWeight_pos
Compiled
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
theorem
BanditRLProof.Exp3.normalizedHistoryDistribution_nonneg
Compiled
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
theorem
BanditRLProof.Exp3.sum_normalizedHistoryDistribution
Compiled
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
theorem
BanditRLProof.Exp3.exploredHistoryDistribution_nonneg
Compiled
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
theorem
BanditRLProof.Exp3.sum_exploredHistoryDistribution
Compiled
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
theorem
BanditRLProof.Exp3.exploredHistoryDistribution_floor
Compiled
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
theorem
BanditRLProof.Exp3.explorationFloor_pos
Compiled
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)
theorem
BanditRLProof.Exp3.finiteActionDistribution_exploredHistoryDistribution
Compiled
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
theorem
BanditRLProof.Exp3.measurable_historyWeight
Compiled
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)
theorem
BanditRLProof.Exp3.measurable_historyTotalWeight
Compiled
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)
theorem
BanditRLProof.Exp3.measurable_normalizedHistoryDistribution
Compiled
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)
theorem
BanditRLProof.Exp3.measurable_exploredHistoryDistribution
Compiled
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)
structure
BanditRLProof.Exp3.MeasurableFiniteHistoryScore
Compiled
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
def
BanditRLProof.Exp3.normalizedHistoryDistributionSource
Compiled
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
def
BanditRLProof.Exp3.exploredHistoryDistributionSource
Compiled
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
def
BanditRLProof.Exp3.initialExploredDistribution
Compiled
Initial EXP3 probabilities, obtained from zero cumulative scores.
noncomputable def initialExploredDistribution {Action : Type u} (arms : Finset Action) (eta gamma : Real) : Action -> Real
theorem
BanditRLProof.Exp3.finiteActionDistribution_initialExploredDistribution
Compiled
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)
def
BanditRLProof.Exp3.exploredHistoryAlgorithm
Compiled
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
theorem
BanditRLProof.Exp3.exploredHistoryAlgorithm_policy
Compiled
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)
def
BanditRLProof.Exp3.exploredTrajectoryKernel
Compiled
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)
theorem
BanditRLProof.Exp3.exploredTrajectoryMeasure_condDistrib_action
Compiled
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)