Prove indepFun_eval_streamMeasure'

LeanBandits.lean

@@ -7,6 +7,7 @@ import LeanBandits.BanditAlgorithms.UCB
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.IdentDistrib
 import LeanBandits.ForMathlib.IndepFun
+import LeanBandits.ForMathlib.IndepInfinitePi
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.MeasurableArgMax

LeanBandits/Bandit/Bandit.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
 import LeanBandits.SequentialLearning.Deterministic
+import LeanBandits.ForMathlib.IndepInfinitePi
 import Mathlib.Probability.IdentDistrib
-import Mathlib.Probability.Independence.InfinitePi
 
 /-!
 # Bandit
@@ -143,8 +143,8 @@ lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m :
   exact (iIndepFun_eval_streamMeasure ν).indepFun (by grind)
 
 lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) :
-    IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := by
-  sorry
+    IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) :=
+  indepFun_proj_infinitePi_infinitePi h
 
 lemma indepFun_eval_snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν]
     {a b : α} (h : a ≠ b) :

LeanBandits/ForMathlib/IndepInfinitePi.lean

@@ -0,0 +1,30 @@
+import Mathlib.Probability.Independence.InfinitePi
+
+open MeasureTheory Measure ProbabilityTheory Set Function
+
+namespace MeasurableSpace
+
+variable {δ : Type*} {X : δ → Type*} [m : ∀ a, MeasurableSpace (X a)] {α : Type*}
+
+-- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
+theorem comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a) := by
+  simp_rw [pi, comap_iSup, comap_comp, comp_def]
+
+end MeasurableSpace
+
+namespace ProbabilityTheory
+
+variable {ι κ : Type*} {𝓧 : ι → κ → Type*} [m𝓧 : ∀ i j, MeasurableSpace (𝓧 i j)]
+    {μ : (i : ι) → (j : κ) → Measure (𝓧 i j)} [∀ i j, IsProbabilityMeasure (μ i j)]
+
+-- Mathlib/Probability/Independence/InfinitePi.lean
+lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) :
+    IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) (infinitePi (fun i ↦ infinitePi (μ i))) := by
+  simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi]
+  have hd : Disjoint (range fun i : ι ↦ (i, a)) (range fun i ↦ (i, b)) := by
+    simp [disjoint_range_iff, h]
+  convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop))
+    (iIndepFun_uncurry_infinitePi' (X := fun _ _ x ↦ x) μ (by fun_prop)) hd
+  all_goals rw [iSup_range]
+
+end ProbabilityTheory