Learning.RoundRobin.action_zero.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      0) :
  A 0 =ᵐ[P] fun x => ⟨0, hK⟩
Learning.RoundRobin.action_zero.{u_1, u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P 0) :
  A 0 =ᵐ[P] fun x => ⟨0, hK⟩