Lean module · Foundations
BanditRLProof.ExpectationWeightedPullCount
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.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.lintegral_finset_sum_gap_mul_natCast_pullCount_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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}))