Bandits.reward_cond_action.{u_1, u_2} {𝓐 : Type u_1} {Ω : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → 𝓐}
  {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace 𝓐]
  [Countable 𝓐]
  (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P)
  (a : 𝓐) (n : ℕ)
  (hμa :
    (MeasureTheory.Measure.map (fun ω => A n (Prod.fst ω))
          (MeasureTheory.Measure.prod P (streamMeasure ν)))
        {a} ≠
      0) :
  𝓛[fun ω => R n (Prod.fst ω) | fun ω => A n (Prod.fst ω) in {a};
      MeasureTheory.Measure.prod P (streamMeasure ν)] =
    ν a
Bandits.reward_cond_action.{u_1, u_2}
  {𝓐 : Type u_1} {Ω : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → 𝓐}
  {R : ℕ → Ω → ℝ}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {alg : Learning.Algorithm 𝓐 ℝ}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  [StandardBorelSpace 𝓐] [Countable 𝓐]
  (h :
    Learning.IsAlgEnvSeq A R alg
      (Learning.stationaryEnv ν) P)
  (a : 𝓐) (n : ℕ)
  (hμa :
    (MeasureTheory.Measure.map
          (fun ω => A n (Prod.fst ω))
          (MeasureTheory.Measure.prod P
            (streamMeasure ν)))
        {a} ≠
      0) :
  𝓛[fun ω => R n (Prod.fst ω) | fun ω =>
      A n (Prod.fst ω) in {a};
      MeasureTheory.Measure.prod P
        (streamMeasure ν)] =
    ν a