BanditRLProof.Exp3ImportanceWeighted

Loss estimate that reveals only the loss of the sampled action.

noncomputable def importanceWeightedLoss {Action : Type u} (prob loss : Action -> Real) (chosen action : Action) : Real

The loss mixed by `prob` after replacing losses by one sampled estimate.

noncomputable def mixedImportanceWeightedLoss {Action : Type u} (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) : Real

An importance-weighted estimate mixed by weights that may differ from the sampling probabilities used in the estimator denominator.

noncomputable def weightedImportanceWeightedLoss {Action : Type u} (arms : Finset Action) (prob weight loss : Action -> Real) (chosen : Action) : Real

The mixed square of one sampled importance-weighted loss vector.

noncomputable def mixedSquaredImportanceWeightedLoss {Action : Type u} (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) : Real

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

theorem importanceWeightedLoss_nonneg {Action : Type u} [DecidableEq Action] {prob loss : Action -> Real} {chosen action : Action} (hprob : 0 <= prob action) (hloss : 0 <= loss action) : 0 <= importanceWeightedLoss prob loss chosen action

The probability-weighted finite sum of one coordinate recovers its loss.

theorem sum_prob_mul_importanceWeightedLoss_eq_loss {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (action : Action) (haction : action ∈ arms) (hprob : prob action ≠ 0) : arms.sum (fun chosen => prob chosen * importanceWeightedLoss prob loss chosen action) = loss action

Pathwise cancellation: the mixed estimate is the sampled loss.

theorem mixedImportanceWeightedLoss_eq_selectedLoss {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) (hchosen : chosen ∈ arms) (hprob : prob chosen ≠ 0) : mixedImportanceWeightedLoss arms prob loss chosen = loss chosen

Averaging the pathwise mixed estimate recovers the true mixed loss.

theorem sum_prob_mul_mixedImportanceWeightedLoss_eq_mixedLoss {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hprob : forall action, action ∈ arms -> prob action ≠ 0) : arms.sum (fun chosen => prob chosen * mixedImportanceWeightedLoss arms prob loss chosen) = arms.sum (fun action => prob action * loss action)

Averaging an estimator mixed by arbitrary predictable weights recovers the same weighted true loss.

theorem sum_prob_mul_weightedImportanceWeightedLoss_eq_weightedLoss {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob weight loss : Action -> Real) (hprob : forall action, action ∈ arms -> prob action ≠ 0) : arms.sum (fun chosen => prob chosen * weightedImportanceWeightedLoss arms prob weight loss chosen) = arms.sum (fun action => weight action * loss action)

Exact pathwise mixed-square formula for a sampled action.

theorem mixedSquaredImportanceWeightedLoss_eq_selectedLoss_sq_div {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) (hchosen : chosen ∈ arms) (hprob : prob chosen ≠ 0) : mixedSquaredImportanceWeightedLoss arms prob loss chosen = (loss chosen) ^ 2 / prob chosen

Exact probability-weighted finite sum of the mixed estimator's square.

theorem sum_prob_mul_mixedSquaredImportanceWeightedLoss_eq_sum_loss_sq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hprob : forall action, action ∈ arms -> prob action ≠ 0) : arms.sum (fun chosen => prob chosen * mixedSquaredImportanceWeightedLoss arms prob loss chosen) = arms.sum (fun action => (loss action) ^ 2)

For losses in `[0,1]`, the probability-weighted mixed square is at most the arm count.

theorem sum_prob_mul_mixedSquaredImportanceWeightedLoss_le_card {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hprob : forall action, action ∈ arms -> prob action ≠ 0) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : arms.sum (fun chosen => prob chosen * mixedSquaredImportanceWeightedLoss arms prob loss chosen) <= arms.card