Law of rewardByCount

[RemyDegenne]

Main result:

lemma hasLaw_rewardByCount_infinitePi (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) :
    HasLaw (fun ω (p : 𝓐 × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω)
      (Measure.infinitePi fun p : 𝓐 × ℕ ↦ ν p.1) 𝔓

Done with Claude Fable 5.1, and reviewed afterwards. Main changes in review: change lemmas to use HasLaw and IdentDistrib instead of bare equalities of Measure.map (and add supporting API); move aux lemmas to their appropriate places and generalize them; remove unnecessary assumptions.