Lean module · Foundations
BanditRLProof.ExpectationPullCountBounds
# Lower-integral pull-count bounds This module proves the first probability-measure corollary of the local pull-count lower-integral identity. It stays in `ENNReal` and only uses the probability mass bound for measurable sets.
Module map
Imports
BanditRLProof.ExpectationPullCount
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_natCast_pullCount_le_time
Compiled
The lower integral of a scalar-casted pull count is bounded by the horizon under a probability measure. This is the `EXP-PULLCOUNT-LE-TIME` bridge. It is a probability-facing budget bound for expected pull counts, not a Bochner expectation or expected-regret theorem.
theorem lintegral_natCast_pullCount_le_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)) (a : Action) (n : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount (action omega) a n : Nat) : ENNReal)) <= (n : ENNReal)