Lean module · Foundations
BanditRLProof.ExpectationFiniteBanditBounds
This module specializes the generic finite-action weighted pull-count budget bound to the canonical finite action type Fin K and Finset.univ.
Module map
Imports
BanditRLProof.ExpectationWeightedPullCountBounds
Imported by
BanditRLProof, BanditRLProof.ExpectationFiniteBanditModelBounds
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.lintegral_univ_sum_gap_mul_natCast_pullCount_le_sum_gap_mul_time
Compiled
The `Fin K`/`Finset.univ` specialization of the `ENNReal` weighted pull-count budget bound under a probability measure. This is the `EXP-WEIGHTED-PULLCOUNT-LE-TIME-FIN` bridge. It is still only an `ENNReal` finite-action probability-count bound; it does not introduce `FiniteBanditModel`, `Rat`/`Real`, or Bochner expectation.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.lintegral_univ_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_univ_sum_gap_mul_natCast_pullCount_le_sum_gap_mul_time {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (gap : Fin K -> ENNReal) (n : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => gap a * ((pullCount (action omega) a n : Nat) : ENNReal))) <= (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => gap a * (n : ENNReal))