Lean module · Foundations
BanditRLProof.ExpectationWeightedPullCountBounds
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.
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_le_sum_gap_mul_timeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))