Lean module · Foundations
BanditRLProof.ExpectationWeightedPullCount
# Weighted lower-integral pull-count identities This module proves the nonnegative weighted-count lower-integral bridge. It remains in `ENNReal`, with an arbitrary finite action set and arbitrary nonnegative gap weights, before any `Rat`/`Real` or Bochner-expectation route.
Module map
Imports
BanditRLProof.ExpectationPullCount, BanditRLProof.MeasurablePullCountCast
Imported by
BanditRLProof, BanditRLProof.ExpectationWeightedPullCountBounds
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.lintegral_finset_sum_gap_mul_natCast_pullCount_eq
Compiled
The lower integral of a finite weighted sum of scalar-casted pull counts equals the same finite weighted sum of the corresponding action-event measures. This is the `EXP-WEIGHTED-PULLCOUNT-LINTEGRAL` bridge. It is shaped like a nonnegative expected-regret identity, but it deliberately avoids `FiniteBanditModel`, `Rat`, `Real`, Bochner expectation, filtrations, kernels, and concentration assumptions.
theorem lintegral_finset_sum_gap_mul_natCast_pullCount_eq {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure Omega) (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (gap : Action -> ENNReal) (arms : Finset Action) (n : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => arms.sum (fun a : Action => gap a * ((pullCount (action omega) a n : Nat) : ENNReal))) = arms.sum (fun a : Action => gap a * (Finset.range n).sum (fun t : Nat => mu {omega : Omega | action omega t = a}))