Lean module · EXP3
BanditRLProof.Exp3ImportanceWeighted
# Finite-action importance-weighted loss identities This module supplies the finite-distribution algebra immediately above the deterministic Hedge theorem and below the probabilistic EXP3 process. It proves the estimator's armwise weighted-sum cancellation and exact mixed-square identity on an explicit finite action set. These statements are deterministic finite sums. Calling them conditional expectation facts requires a later law-transport theorem identifying the conditional action law with the supplied probabilities.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Exp3ConditionalMoments, BanditRLProof.TsallisImportanceWeightedMoment
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.importanceWeightedLoss
Compiled
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
def
BanditRLProof.Exp3.mixedImportanceWeightedLoss
Compiled
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
def
BanditRLProof.Exp3.weightedImportanceWeightedLoss
Compiled
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
def
BanditRLProof.Exp3.mixedSquaredImportanceWeightedLoss
Compiled
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
theorem
BanditRLProof.Exp3.importanceWeightedLoss_nonneg
Compiled
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
theorem
BanditRLProof.Exp3.sum_prob_mul_importanceWeightedLoss_eq_loss
Compiled
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
theorem
BanditRLProof.Exp3.mixedImportanceWeightedLoss_eq_selectedLoss
Compiled
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
theorem
BanditRLProof.Exp3.sum_prob_mul_mixedImportanceWeightedLoss_eq_mixedLoss
Compiled
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)
theorem
BanditRLProof.Exp3.sum_prob_mul_weightedImportanceWeightedLoss_eq_weightedLoss
Compiled
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)
theorem
BanditRLProof.Exp3.mixedSquaredImportanceWeightedLoss_eq_selectedLoss_sq_div
Compiled
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
theorem
BanditRLProof.Exp3.sum_prob_mul_mixedSquaredImportanceWeightedLoss_eq_sum_loss_sq
Compiled
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)
theorem
BanditRLProof.Exp3.sum_prob_mul_mixedSquaredImportanceWeightedLoss_le_card
Compiled
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