Prove independence lemmas

LeanBandits/ForMathlib/IndepFun.lean

@@ -4,7 +4,9 @@ open MeasureTheory Finset
 
 namespace ProbabilityTheory
 
-variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {mE : MeasurableSpace E} {μ : Measure Ω}
+variable {α Ω Ω' E ι : Type*} [Countable ι] {mα : MeasurableSpace α}
+  {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
+  {mE : MeasurableSpace E} {μ ν : Measure Ω}
 
 lemma iIndepFun_nat_iff_forall_indepFun {X : ℕ → Ω → E} (hX : ∀ n, AEMeasurable (X n) μ) :
     iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by
@@ -23,4 +25,47 @@ lemma iIndepFun_nat_iff_forall_indepFun {X : ℕ → Ω → E} (hX : ∀ n, AEMe
     intro n
     sorry
 
+-- todo: kernel version?
+lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f : Ω → Ω'}
+    (hf : AEMeasurable f μ) (hX : AEMeasurable X (μ.map f)) (hY : AEMeasurable Y (μ.map f)) :
+    X ⟂ᵢ[μ.map f] Y ↔ (X ∘ f) ⟂ᵢ[μ] (Y ∘ f) := by
+  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY,
+    indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)]
+  rw [AEMeasurable.map_map_of_aemeasurable hY hf, AEMeasurable.map_map_of_aemeasurable hX hf,
+    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
+  rfl
+
+lemma iIndepFun_map_iff [IsProbabilityMeasure μ] {X : ι → Ω' → E} {f : Ω → Ω'}
+    (hf : AEMeasurable f μ) (hX : ∀ n, AEMeasurable (X n) (μ.map f)) :
+    iIndepFun X (μ.map f) ↔ iIndepFun (fun n ↦ X n ∘ f) μ := by
+  have := Measure.isProbabilityMeasure_map hf (μ := μ)
+  rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀' hX,
+    iIndepFun_iff_map_fun_eq_infinitePi_map₀' (by fun_prop)]
+  rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
+  congr! 3
+  rw [AEMeasurable.map_map_of_aemeasurable (hX _) hf]
+
+lemma identDistrib_map_right_iff {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
+    (hf : AEMeasurable f ν) (hX : AEMeasurable X μ) (hY : AEMeasurable Y (ν.map f)) :
+    IdentDistrib X Y μ (ν.map f) ↔ IdentDistrib X (Y ∘ f) μ ν := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · constructor
+    · exact hX
+    · fun_prop
+    · rw [h.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
+  · constructor
+    · exact hX
+    · fun_prop
+    · rw [h.map_eq, AEMeasurable.map_map_of_aemeasurable hY hf]
+
+lemma identDistrib_comm (X : Ω → E) (Y : Ω' → E) {ν : Measure Ω'} :
+    IdentDistrib X Y μ ν ↔ IdentDistrib Y X ν μ :=
+  ⟨fun h ↦ h.symm, fun h ↦ h.symm⟩
+
+lemma identDistrib_map_left_iff {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
+    (hf : AEMeasurable f ν) (hX : AEMeasurable X μ) (hY : AEMeasurable Y (ν.map f)) :
+    IdentDistrib Y X (ν.map f) μ ↔ IdentDistrib (Y ∘ f) X ν μ := by
+  rw [identDistrib_comm Y, identDistrib_comm _ X]
+  exact identDistrib_map_right_iff hf hX hY
+
 end ProbabilityTheory

LeanBandits/RewardByCountMeasure.lean

@@ -365,7 +365,8 @@ lemma identDistrib_rewardByCount_stream' [Countable α] [StandardBorelSpace α]
       (Bandit.measure alg ν) (Bandit.streamMeasure ν) := by
   refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
   · refine identDistrib_rewardByCount_eval a (n + 1) n (by simp) (ν := ν)
-  · sorry
+  · have h_indep := iIndepFun_rewardByCount' alg ν a
+    exact iIndepFun.precomp (g := fun n ↦ n + 1) (fun i j hij ↦ by grind) h_indep
   · exact iIndepFun_eval_streamMeasure'' ν a
 
 lemma identDistrib_rewardByCount_stream [Countable α] [StandardBorelSpace α] [Nonempty α]
@@ -374,9 +375,15 @@ lemma identDistrib_rewardByCount_stream [Countable α] [StandardBorelSpace α] [
       (Bandit.measure alg ν) (Bandit.measure alg ν) := by
   refine (identDistrib_rewardByCount_stream' a).trans ?_
   refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
-  · sorry
-  · sorry
-  · sorry
+  · rw [← Bandit.snd_measure alg ν, Measure.snd,
+      identDistrib_map_left_iff (by fun_prop) (by fun_prop)
+        (Measurable.aemeasurable <| by fun_prop)]
+    exact IdentDistrib.refl (by fun_prop)
+  · exact iIndepFun_eval_streamMeasure'' ν a
+  · change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) (Bandit.measure alg ν)
+    rw [← iIndepFun_map_iff (by fun_prop) (fun _ ↦ Measurable.aemeasurable (by fun_prop))]
+    rw [← Measure.snd, Bandit.snd_measure]
+    exact iIndepFun_eval_streamMeasure'' ν a
 
 lemma indepFun_rewardByCount_of_ne {a b : α} (hab : a ≠ b) :
     IndepFun (fun ω s ↦ rewardByCount a s ω.1 ω.2) (fun ω s ↦ rewardByCount b s ω.1 ω.2)

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "98b14016adbf3d90a2cc79399e49b9ee67b4155c",
+   "rev": "be9d1e42709f0c71f23bf54fdcea77c4058cd659",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,