Lean module · EXP3
BanditRLProof.Exp3SampledHedge
# Pathwise Hedge control for the concrete sampled EXP3 score This module identifies the recursively accumulated `sampledHistoryScore` with the deterministic cumulative-loss surface used by `Exp3HedgeRegret`. It also identifies the corresponding pure exponential-weights distribution and the exploration-mixed trajectory probability. The final theorem specializes the deterministic second-order Hedge bound to one concrete sampled trajectory. The result is pathwise. Its scalar-feedback nonnegativity premise is intended to be discharged almost surely by the predictable `[0,1]` reward law before integrating the bound.
Module map
Imports
BanditRLProof.Exp3PredictableMoments
Imported by
BanditRLProof, BanditRLProof.Exp3PredictableHedge, BanditRLProof.TsallisFTRLRecursiveTrajectory
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledTrajectoryObservedLoss
Compiled
The complete importance-weighted loss vector observed at an actual time.
noncomputable def sampledTrajectoryObservedLoss {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (sample : Env × ((k : Nat) -> Action × Real)) : Nat -> Action -> Real
theorem
BanditRLProof.Exp3.previousPairHistory_frestrictLe
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem previousPairHistory_frestrictLe {Action : Type v} (n : Nat) (trajectory : (k : Nat) -> Action × Real) : previousPairHistory (Preorder.frestrictLe (n + 1) trajectory) = Preorder.frestrictLe n trajectory
theorem
BanditRLProof.Exp3.sampledHistoryScore_frestrictLe_eq_cumulativeLoss
Compiled
The inclusive sampled score through `n` is Hedge cumulative loss at `n+1`.
theorem sampledHistoryScore_frestrictLe_eq_cumulativeLoss {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (sample : Env × ((k : Nat) -> Action × Real)) (n : Nat) (action : Action) : sampledHistoryScore arms eta gamma n (Preorder.frestrictLe n sample.2) action = cumulativeLoss (sampledTrajectoryObservedLoss arms eta gamma sample) (n + 1) action
theorem
BanditRLProof.Exp3.distribution_sampledTrajectoryObservedLoss_succ
Compiled
At a successor time, the Hedge distribution is the normalized sampled score.
theorem distribution_sampledTrajectoryObservedLoss_succ {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (sample : Env × ((k : Nat) -> Action × Real)) (n : Nat) (action : Action) : distribution arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) (n + 1) action = normalizedHistoryDistribution arms eta (sampledHistoryScore arms eta gamma n) (Preorder.frestrictLe n sample.2) action
theorem
BanditRLProof.Exp3.sampledTrajectoryProbabilityAt_eq_mix_distribution
Compiled
The concrete sampling law is uniform exploration mixed with the Hedge law.
theorem sampledTrajectoryProbabilityAt_eq_mix_distribution {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (action : Action) : sampledTrajectoryProbabilityAt arms eta gamma t sample action = (1 - gamma) * distribution arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t action + gamma / (arms.card : Real)
theorem
BanditRLProof.Exp3.sampledTrajectoryProbabilityAt_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledTrajectoryProbabilityAt_nonneg {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (action : Action) : 0 <= sampledTrajectoryProbabilityAt arms eta gamma t sample action
theorem
BanditRLProof.Exp3.sampledTrajectoryObservedLoss_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sampledTrajectoryObservedLoss_nonneg {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (sample : Env × ((k : Nat) -> Action × Real)) (t : Nat) (action : Action) (hreward : 0 <= (sample.2 t).2) : 0 <= sampledTrajectoryObservedLoss arms eta gamma sample t action
theorem
BanditRLProof.Exp3.sampledTrajectory_hedge_regret_le
Compiled
Concrete finite-horizon sampled-trajectory specialization of Hedge.
theorem sampledTrajectory_hedge_regret_le {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (heta : 0 < eta) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (sample : Env × ((k : Nat) -> Action × Real)) (horizon : Nat) (hreward_nonneg : forall t, t < horizon -> 0 <= (sample.2 t).2) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range horizon).sum (fun t => mixedLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t) - cumulativeLoss (sampledTrajectoryObservedLoss arms eta gamma sample) horizon comparator <= Real.log arms.card / eta + eta * (Finset.range horizon).sum (fun t => mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t)
theorem
BanditRLProof.Exp3.sampledHistoryScore_hedge_regret_le
Compiled
The same pathwise Hedge bound with its comparator term exposed as the concrete inclusive `sampledHistoryScore`.
theorem sampledHistoryScore_hedge_regret_le {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (heta : 0 < eta) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (sample : Env × ((k : Nat) -> Action × Real)) (n : Nat) (hreward_nonneg : forall t, t < n + 1 -> 0 <= (sample.2 t).2) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range (n + 1)).sum (fun t => mixedLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t) - sampledHistoryScore arms eta gamma n (Preorder.frestrictLe n sample.2) comparator <= Real.log arms.card / eta + eta * (Finset.range (n + 1)).sum (fun t => mixedSquaredLoss arms eta (sampledTrajectoryObservedLoss arms eta gamma sample) t)