Lean module · Foundations
BanditRLProof.ScalarENNReal
# Scalar `ENNReal.ofReal` bridges This module contains scalar conversion leaves used before any probability or bandit-specific expectation statement. The lemmas here are deliberately independent of `FiniteBanditModel`, traces, integrals, and filtrations.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ENNReal.ofReal_finset_sum_mul_natCast_of_nonneg
Compiled
For a finite sum of nonnegative real weights times natural counts, `ofReal` commutes with the weighted sum and turns the counts into `ENNReal` casts. This is the `OFREAL-FINSET-WEIGHTED-NAT-FAITHFULNESS` scalar leaf. It is a faithfulness lemma under explicit pointwise nonnegativity of the real weights; it is not an expectation theorem.
theorem ofReal_finset_sum_mul_natCast_of_nonneg {ι : Type u} (s : Finset ι) (gap : ι -> Real) (count : ι -> Nat) (hgap : forall i : ι, i ∈ s -> 0 <= gap i) : ENNReal.ofReal (s.sum (fun i : ι => gap i * ((count i : Nat) : Real))) = s.sum (fun i : ι => ENNReal.ofReal (gap i) * ((count i : Nat) : ENNReal))