Lean module · EXP3

BanditRLProof.Exp3HedgeRegret

# Deterministic exponential-weights regret This module closes the full-information exponential-weights/Hedge potential argument that sits immediately below EXP3. It defines weights from cumulative losses, normalizes them on an explicit nonempty finite action set, proves the one-step logarithmic potential inequality, and telescopes it into second-order and `[0,1]` finite-horizon regret bounds. No probability space or importance-weighted estimator is used here. The EXP3 route must separately construct an estimator, prove its conditional unbiasedness and second-moment bound, and then take expectations of this pathwise theorem.

Module map

Source: BanditRLProof/Exp3HedgeRegret.lean
Teaching chapter: 7. EXP3 and adversarial concentration
Declarations: 26
Placeholders: 0

Imports

BanditRLProof.Exp3Potential

Imported by

BanditRLProof, BanditRLProof.Exp3ImportanceWeighted

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.Exp3.cumulativeLoss Compiled

Cumulative loss of one action before round `t`.

noncomputable def cumulativeLoss {Action : Type u} (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : Real

Source line 30 Chapter context: EXP3

def BanditRLProof.Exp3.weight Compiled

Exponential weight generated by the cumulative loss before round `t`.

noncomputable def weight {Action : Type u} (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : Real

Source line 35 Chapter context: EXP3

def BanditRLProof.Exp3.totalWeight Compiled

Total exponential weight on an explicit finite action set.

noncomputable def totalWeight {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : Real

Source line 40 Chapter context: EXP3

def BanditRLProof.Exp3.distribution Compiled

Normalized exponential weight at round `t`.

noncomputable def distribution {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : Real

Source line 46 Chapter context: EXP3

def BanditRLProof.Exp3.mixedLoss Compiled

Mixed loss incurred by the normalized exponential weights at round `t`.

noncomputable def mixedLoss {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : Real

Source line 52 Chapter context: EXP3

def BanditRLProof.Exp3.mixedSquaredLoss Compiled

Mixed second moment of the losses at round `t`.

noncomputable def mixedSquaredLoss {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : Real

Source line 58 Chapter context: EXP3

theorem BanditRLProof.Exp3.cumulativeLoss_succ Compiled

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

theorem cumulativeLoss_succ {Action : Type u} (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : cumulativeLoss loss (t + 1) a = cumulativeLoss loss t a + loss t a

Source line 63 Chapter context: EXP3

theorem BanditRLProof.Exp3.weight_pos Compiled

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

theorem weight_pos {Action : Type u} (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : 0 < weight eta loss t a

Source line 68 Chapter context: EXP3

theorem BanditRLProof.Exp3.weight_succ Compiled

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

theorem weight_succ {Action : Type u} (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : weight eta loss (t + 1) a = weight eta loss t a * Real.exp (-eta * loss t a)

Source line 73 Chapter context: EXP3

theorem BanditRLProof.Exp3.totalWeight_pos Compiled

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

theorem totalWeight_pos {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : 0 < totalWeight arms eta loss t

Source line 83 Chapter context: EXP3

theorem BanditRLProof.Exp3.distribution_nonneg Compiled

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

theorem distribution_nonneg {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : 0 <= distribution arms eta loss t a

Source line 92 Chapter context: EXP3

theorem BanditRLProof.Exp3.distribution_pos Compiled

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

theorem distribution_pos {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (a : Action) : 0 < distribution arms eta loss t a

Source line 99 Chapter context: EXP3

theorem BanditRLProof.Exp3.sum_distribution Compiled

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

theorem sum_distribution {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : arms.sum (distribution arms eta loss t) = 1

Source line 106 Chapter context: EXP3

theorem BanditRLProof.Exp3.totalWeight_zero Compiled

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

theorem totalWeight_zero {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) : totalWeight arms eta loss 0 = arms.card

Source line 117 Chapter context: EXP3

theorem BanditRLProof.Exp3.exp_neg_le_one_sub_add_sq Compiled

Global quadratic upper bound for a nonnegative exponential argument.

theorem exp_neg_le_one_sub_add_sq {x : Real} (hx : 0 <= x) : Real.exp (-x) <= 1 - x + x ^ 2

Source line 123 Chapter context: EXP3

theorem BanditRLProof.Exp3.exp_neg_mul_le_one_sub_add_sq_of_nonneg Compiled

Quadratic exponential bound for arbitrary nonnegative learning rates and losses.

theorem exp_neg_mul_le_one_sub_add_sq_of_nonneg {eta ell : Real} (heta : 0 <= eta) (hell : 0 <= ell) : Real.exp (-eta * ell) <= 1 - eta * ell + eta ^ 2 * ell ^ 2

Source line 140 Chapter context: EXP3

theorem BanditRLProof.Exp3.exp_neg_mul_le_one_sub_add_sq Compiled

Backwards-compatible bounded-loss specialization of the global bound.

theorem exp_neg_mul_le_one_sub_add_sq {eta ell : Real} (heta : 0 <= eta) (_heta_le : eta <= 1) (hell : 0 <= ell) (_hell_le : ell <= 1) : Real.exp (-eta * ell) <= 1 - eta * ell + eta ^ 2 * ell ^ 2

Source line 147 Chapter context: EXP3

theorem BanditRLProof.Exp3.totalWeight_succ_div_eq_sum_distribution_mul_exp Compiled

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

theorem totalWeight_succ_div_eq_sum_distribution_mul_exp {Action : Type u} (arms : Finset Action) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) : totalWeight arms eta loss (t + 1) / totalWeight arms eta loss t = arms.sum (fun a => distribution arms eta loss t a * Real.exp (-eta * loss t a))

Source line 153 Chapter context: EXP3

theorem BanditRLProof.Exp3.totalWeight_succ_div_le_of_nonneg Compiled

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

theorem totalWeight_succ_div_le_of_nonneg {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 <= eta) (loss : Nat -> Action -> Real) (t : Nat) (hloss : forall a, a ∈ arms -> 0 <= loss t a) : totalWeight arms eta loss (t + 1) / totalWeight arms eta loss t <= 1 - eta * mixedLoss arms eta loss t + eta ^ 2 * mixedSquaredLoss arms eta loss t

Source line 169 Chapter context: EXP3

theorem BanditRLProof.Exp3.totalWeight_succ_div_le Compiled

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

theorem totalWeight_succ_div_le {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 <= eta) (_heta_le : eta <= 1) (loss : Nat -> Action -> Real) (t : Nat) (hloss : forall a, a ∈ arms -> 0 <= loss t a ∧ loss t a <= 1) : totalWeight arms eta loss (t + 1) / totalWeight arms eta loss t <= 1 - eta * mixedLoss arms eta loss t + eta ^ 2 * mixedSquaredLoss arms eta loss t

Source line 218 Chapter context: EXP3

theorem BanditRLProof.Exp3.log_totalWeight_succ_sub_le_of_nonneg Compiled

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

theorem log_totalWeight_succ_sub_le_of_nonneg {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 <= eta) (loss : Nat -> Action -> Real) (t : Nat) (hloss : forall a, a ∈ arms -> 0 <= loss t a) : Real.log (totalWeight arms eta loss (t + 1)) - Real.log (totalWeight arms eta loss t) <= -eta * mixedLoss arms eta loss t + eta ^ 2 * mixedSquaredLoss arms eta loss t

Source line 231 Chapter context: EXP3

theorem BanditRLProof.Exp3.log_totalWeight_succ_sub_le Compiled

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

theorem log_totalWeight_succ_sub_le {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 <= eta) (_heta_le : eta <= 1) (loss : Nat -> Action -> Real) (t : Nat) (hloss : forall a, a ∈ arms -> 0 <= loss t a ∧ loss t a <= 1) : Real.log (totalWeight arms eta loss (t + 1)) - Real.log (totalWeight arms eta loss t) <= -eta * mixedLoss arms eta loss t + eta ^ 2 * mixedSquaredLoss arms eta loss t

Source line 249 Chapter context: EXP3

theorem BanditRLProof.Exp3.mixedSquaredLoss_le_one Compiled

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

theorem mixedSquaredLoss_le_one {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Nat -> Action -> Real) (t : Nat) (hloss : forall a, a ∈ arms -> 0 <= loss t a ∧ loss t a <= 1) : mixedSquaredLoss arms eta loss t <= 1

Source line 262 Chapter context: EXP3

theorem BanditRLProof.Exp3.hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss_of_nonneg Compiled

Second-order finite-horizon Hedge regret bound against one comparator action.

theorem hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss_of_nonneg {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (loss : Nat -> Action -> Real) (T : Nat) (hloss : forall t, t < T -> forall a, a ∈ arms -> 0 <= loss t a) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range T).sum (fun t => mixedLoss arms eta loss t) - cumulativeLoss loss T comparator <= Real.log arms.card / eta + eta * (Finset.range T).sum (fun t => mixedSquaredLoss arms eta loss t)

Source line 283 Open teaching explanation Chapter context: EXP3

theorem BanditRLProof.Exp3.hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss Compiled

Bounded-loss compatibility wrapper for the generalized second-order theorem.

theorem hedge_regret_le_log_card_div_add_eta_mul_mixedSquaredLoss {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (_heta_le : eta <= 1) (loss : Nat -> Action -> Real) (T : Nat) (hloss : forall t, t < T -> forall a, a ∈ arms -> 0 <= loss t a ∧ loss t a <= 1) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range T).sum (fun t => mixedLoss arms eta loss t) - cumulativeLoss loss T comparator <= Real.log arms.card / eta + eta * (Finset.range T).sum (fun t => mixedSquaredLoss arms eta loss t)

Source line 359 Chapter context: EXP3

theorem BanditRLProof.Exp3.hedge_regret_le_log_card_div_add_eta_mul_horizon Compiled

Finite-horizon Hedge regret for losses in `[0,1]`. This is the deterministic full-information theorem consumed by the future importance-weighted EXP3 route.

theorem hedge_regret_le_log_card_div_add_eta_mul_horizon {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (heta_le : eta <= 1) (loss : Nat -> Action -> Real) (T : Nat) (hloss : forall t, t < T -> forall a, a ∈ arms -> 0 <= loss t a ∧ loss t a <= 1) (comparator : Action) (hcomparator : comparator ∈ arms) : (Finset.range T).sum (fun t => mixedLoss arms eta loss t) - cumulativeLoss loss T comparator <= Real.log arms.card / eta + eta * T

Source line 382 Chapter context: EXP3