Lean module · Foundations
BanditRLProof.ExpectationPullCount
# Lower-integral pull-count identities This module connects the `ENNReal` finite-sum lower-integral bridge back to the local recursive `pullCount` quantity. It remains before Bochner expectation, expected regret, filtrations, kernels, or concentration.
Module map
Imports
BanditRLProof.ExpectationSums, BanditRLProof.LeafLemmas
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCB, BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount, BanditRLProof.ExpectationPullCountBounds, BanditRLProof.ExpectationWeightedPullCount
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ennreal_natCast_pullCount_eq_finset_range_indicator_one
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem ennreal_natCast_pullCount_eq_finset_range_indicator_one {Omega : Type u} {Action : Type v} [DecidableEq Action] (action : Omega -> ActionTrace Action) (a : Action) (n : Nat) (omega : Omega) : ((pullCount (action omega) a n : Nat) : ENNReal) = (Finset.range n).sum (fun t : Nat => (({omega' : Omega | action omega' t = a} : Set Omega).indicator (1 : Omega -> ENNReal)) omega)
theorem
BanditRLProof.lintegral_natCast_pullCount_eq_sum_measure_actionTrace_eval_eq
Compiled
The lower integral of the scalar-casted local pull count is the finite sum of the corresponding action-event measures. This is the `EXP-PULLCOUNT-LINTEGRAL` bridge. It connects the compiled finite-sum lower-integral identity to the recursive `pullCount` surface without choosing a Bochner expectation or probability-measure interface.
theorem lintegral_natCast_pullCount_eq_sum_measure_actionTrace_eval_eq {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure Omega) (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)) = (Finset.range n).sum (fun t : Nat => mu {omega : Omega | action omega t = a})