BanditRLProof.Algorithms.StochasticGradientBanditAudit

The denominator in the source softmax rule, Equation (3).

def softmaxDenominator (theta : Action -> Real) : Real

The source softmax sampling probability, Equation (3).

def softmaxProbability (theta : Action -> Real) (a : Action) : Real

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

theorem softmaxDenominator_pos [Nonempty Action] (theta : Action -> Real) : 0 < softmaxDenominator theta

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

theorem softmaxProbability_pos [Nonempty Action] (theta : Action -> Real) (a : Action) : 0 < softmaxProbability theta a

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

theorem softmaxProbability_nonneg [Nonempty Action] (theta : Action -> Real) (a : Action) : 0 <= softmaxProbability theta a

Equation (3) defines a normalized finite sampling law.

theorem softmaxProbability_sum [Nonempty Action] (theta : Action -> Real) : ∑ a, softmaxProbability theta a = 1

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

theorem softmaxProbability_le_one [Nonempty Action] (theta : Action -> Real) (a : Action) : softmaxProbability theta a <= 1

Algorithm 1 / Equation (4), before multiplication by the learning rate.

def sourceIncrement (p : Action -> Real) (reward : Real) (selected k : Action) : Real

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

theorem sourceIncrement_eq_indicator (p : Action -> Real) (reward : Real) (selected k : Action) : sourceIncrement p reward selected k = reward * ((if selected = k then 1 else 0) - p k)

Algorithm 1 preserves the zero sum of its parameter vector.

theorem sum_sourceIncrement (p : Action -> Real) (reward : Real) (selected : Action) (hp : ∑ k, p k = 1) : ∑ k, sourceIncrement p reward selected k = 0

The policy value at a fixed pre-action history.

def policyValue (p mean : Action -> Real) : Real

The finite conditional-mean version of the source expected update.

def expectedSourceIncrement (p mean : Action -> Real) (k : Action) : Real

Equation (5), in policy-gradient-coordinate form.

theorem expectedSourceIncrement_eq_gradientCoordinate (p mean : Action -> Real) (k : Action) : expectedSourceIncrement p mean k = p k * (mean k - policyValue p mean)

The source instantaneous expected gap `E_t[Delta_{A_t}]`.

def instantaneousGap (p gap : Action -> Real) : Real

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

theorem instantaneousGap_eq_bestMean_sub_policyValue (p mean gap : Action -> Real) (bestMean : Real) (hp : ∑ a, p a = 1) (hgap : ∀ a, gap a = bestMean - mean a) : instantaneousGap p gap = bestMean - policyValue p mean

Equation (5), in instantaneous-gap-coordinate form.

theorem expectedSourceIncrement_eq_gapCoordinate (p mean gap : Action -> Real) (bestMean : Real) (k : Action) (hp : ∑ a, p a = 1) (hgap : ∀ a, gap a = bestMean - mean a) : expectedSourceIncrement p mean k = p k * (instantaneousGap p gap - gap k)

The gap-coordinate update isolated from Equation (5).

def gapExpectedIncrement (p gap : Action -> Real) (k : Action) : Real

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

theorem expectedSourceIncrement_eq_gapExpectedIncrement (p mean gap : Action -> Real) (bestMean : Real) (k : Action) (hp : ∑ a, p a = 1) (hgap : ∀ a, gap a = bestMean - mean a) : expectedSourceIncrement p mean k = gapExpectedIncrement p gap k

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

theorem instantaneousGap_ge_minGap_mul_failureMass (p gap : Action -> Real) (best : Action) (Delta : Real) (hp : ∑ a, p a = 1) (hp_nonneg : ∀ a, 0 <= p a) (hgap_best : gap best = 0) (hgap_min : ∀ a, a ≠ best -> Delta <= gap a) : Delta * (1 - p best) <= instantaneousGap p gap

Pointwise Equation (6): the best coordinate gains at least the positive gap times its success/failure probability product.

theorem gapExpectedIncrement_best_ge (p gap : Action -> Real) (best : Action) (Delta : Real) (hp : ∑ a, p a = 1) (hp_nonneg : ∀ a, 0 <= p a) (hgap_best : gap best = 0) (hgap_min : ∀ a, a ≠ best -> Delta <= gap a) : Delta * (p best * (1 - p best)) <= gapExpectedIncrement p gap best

The finite-horizon best-parameter expectation represented by Equation (6), after conditioning at each round.

def bestParameterIncrementSum (eta : Real) (p : Nat -> Action -> Real) (gap : Action -> Real) (best : Action) (horizon : Nat) : Real

Finite-horizon Equation (6).

theorem bestParameterIncrementSum_ge (eta Delta : Real) (p : Nat -> Action -> Real) (gap : Action -> Real) (best : Action) (horizon : Nat) (heta : 0 <= eta) (hp : ∀ t, ∑ a, p t a = 1) (hp_nonneg : ∀ t a, 0 <= p t a) (hgap_best : gap best = 0) (hgap_min : ∀ a, a ≠ best -> Delta <= gap a) : eta * Delta * (∑ t ∈ Finset.range horizon, p t best * (1 - p t best)) <= bestParameterIncrementSum eta p gap best horizon

The gap-weighted finite-horizon expected pseudo-regret from Equation (2).

def sourceExpectedPseudoRegret (p : Nat -> Action -> Real) (gap : Action -> Real) (horizon : Nat) : Real

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

theorem instantaneousGap_le_maxGap_mul_failureMass (p gap : Action -> Real) (best : Action) (DeltaMax : Real) (hp : ∑ a, p a = 1) (hp_nonneg : ∀ a, 0 <= p a) (hgap_best : gap best = 0) (hgap_max : ∀ a, a ≠ best -> gap a <= DeltaMax) : instantaneousGap p gap <= DeltaMax * (1 - p best)

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

theorem failureMass_eq_successFailure_add_sq (x : Real) : 1 - x = x * (1 - x) + (1 - x) ^ 2

Equation (7), with its positive learning-rate/minimum-gap denominator and maximum-gap envelope exposed explicitly.

theorem sourceRegretDecomposition_le (eta Delta DeltaMax : Real) (p : Nat -> Action -> Real) (gap : Action -> Real) (best : Action) (horizon : Nat) (heta : 0 < eta) (hDelta : 0 < Delta) (hDeltaMax : 0 <= DeltaMax) (hp : ∀ t, ∑ a, p t a = 1) (hp_nonneg : ∀ t a, 0 <= p t a) (hgap_best : gap best = 0) (hgap_min : ∀ a, a ≠ best -> Delta <= gap a) (hgap_max : ∀ a, a ≠ best -> gap a <= DeltaMax) : sourceExpectedPseudoRegret p gap horizon <= (DeltaMax / (eta * Delta)) * bestParameterIncrementSum eta p gap best horizon + DeltaMax * (∑ t ∈ Finset.range horizon, (1 - p t best) ^ 2)