Lean module · Foundations
BanditRLProof.ExpectationWeightedPullCountBounds
# Weighted lower-integral pull-count bounds This module proves the finite weighted-count budget bound under a probability measure. It stays in `ENNReal`; no `Rat`/`Real`, Bochner expectation, filtration, kernel, or concentration interface is selected here.
Module map
Imports
BanditRLProof.ExpectationWeightedPullCount, BanditRLProof.ExpectationPullCountBounds
Imported by
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_le_sum_gap_mul_time
Compiled
The lower integral of a finite weighted sum of scalar-casted pull counts is bounded by the corresponding weighted horizon budget under a probability measure. This is the `EXP-WEIGHTED-PULLCOUNT-LE-TIME` bridge. It is an `ENNReal` probability-count budget bound, not a Bochner expected-regret theorem.
theorem lintegral_finset_sum_gap_mul_natCast_pullCount_le_sum_gap_mul_time {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (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 * (n : ENNReal))