BanditRLProof.Exp3HedgeRegret

Cumulative loss of one action before round `t`.

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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))

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

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

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

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

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

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)

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)

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