Lean module · Foundations
BanditRLProof.ExpectationSums
# Lower-integral finite sums of pull-event indicators This module proves the finite-sum lower-integral bridge for pull-event indicators. It stays in `ENNReal` and arbitrary measures, before Bochner expectation, pull-count identities, filtrations, kernels, or concentration.
Module map
Imports
BanditRLProof.ExpectationFoundation
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCB, BanditRLProof.ExpectationPullCount
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_actionTrace_eval_eq_indicator_one
Compiled
The lower integral of a finite sum of pull-event indicators is the finite sum of the corresponding event measures. This is the `EXP-FINSET-INDICATOR-PULL` bridge. It isolates lower-integral finite-additivity before connecting the finite sum to `pullCount`.
theorem lintegral_finset_sum_actionTrace_eval_eq_indicator_one {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] (mu : Measure Omega) (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (a : Action) (s : Finset Nat) : MeasureTheory.lintegral mu (fun omega : Omega => s.sum (fun t : Nat => (({omega' : Omega | action omega' t = a} : Set Omega).indicator (1 : Omega -> ENNReal)) omega)) = s.sum (fun t : Nat => mu {omega : Omega | action omega t = a})