From 7953b5c1df079d61f0110e990baf579ba88fc0b0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 3 Sep 2026 14:36:46 +0200 Subject: [PATCH 1/2] rework the ArrayProbSpace independence proofs --- .../Probability/HasCondDistrib.lean | 15 + .../Probability/Independence/IndepFun.lean | 94 +++ .../Independence/IndepInfinitePi.lean | 5 + .../Online/Bandit/ArrayProbSpace.lean | 798 ++++-------------- 4 files changed, 288 insertions(+), 624 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index 87a686a6..e9ef0f0f 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -112,6 +112,21 @@ lemma HasCondDistrib.indepFun_of_const [IsProbabilityMeasure μ] {Q : Measure Ω rw [indepFun_iff_map_prod_eq_prod_map_map h.aemeasurable_fst h.aemeasurable_snd, h.map_eq, h.hasLaw_of_const.map_eq, Measure.compProd_const] +lemma IndepFun.hasCondDistrib_const [IsFiniteMeasure μ] {Q : Measure Ω} [SFinite Q] + (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : HasLaw Y Q μ) : + HasCondDistrib Y X (Kernel.const β Q) μ where + aemeasurable := hX.prodMk hY.aemeasurable + map_eq := by + rw [(indepFun_iff_map_prod_eq_prod_map_map hX hY.aemeasurable).1 h, hY.map_eq, + Measure.compProd_const] + +lemma hasCondDistrib_self [SFinite μ] (hX : AEMeasurable X μ) : + HasCondDistrib X X (@Kernel.id β mβ) μ where + aemeasurable := hX.prodMk hX + map_eq := by + rw [Measure.compProd_id, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] + rfl + lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q] (h : HasCondDistrib Y X (Kernel.const β Q) μ) : HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean index 80df7dff..cd596ffa 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean @@ -50,6 +50,15 @@ lemma indepFun_cond_of_indepFun {α β γ : Type*} {mα : MeasurableSpace α} {m rw [← mul_assoc (μ (Y ⁻¹' s)), ENNReal.mul_inv_cancel h_zero.2 h_zero.1, one_mul] congr +lemma indepFun_cond_comp {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure α} + {X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y) + {Z : γ → δ} (hZ : Measurable Z) (z : δ) : + X ⟂ᵢ[μ[|(Z ∘ Y) ⁻¹' {z}]] Y := by + have h_preim : (Z ∘ Y) ⁻¹' {z} = Y ⁻¹' (Z ⁻¹' {z}) := by grind + simp_rw [h_preim] + exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z)) + lemma iIndepFun_nat_iff_forall_indepFun [IsProbabilityMeasure μ] {X : ℕ → Ω → E} (hX : ∀ n, AEMeasurable (X n) μ) : iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by @@ -134,3 +143,88 @@ lemma identDistrib_map_left_iff {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'} exact identDistrib_map_right_iff hf hX hY end ProbabilityTheory + +namespace ProbabilityTheory + +section Prod + +variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} + +lemma hasLaw_fst_prod (μ : Measure α) (ν : Measure β) [IsProbabilityMeasure ν] : + HasLaw Prod.fst μ (μ.prod ν) where + map_eq := Measure.fst_prod + +lemma hasLaw_snd_prod (μ : Measure α) [IsProbabilityMeasure μ] (ν : Measure β) [SFinite ν] : + HasLaw Prod.snd ν (μ.prod ν) where + map_eq := Measure.snd_prod + +/-- If `X` and `T` are independent under `ν`, then under `μ.prod ν` the function `X ∘ Prod.snd` +is independent of `(Prod.fst, T ∘ Prod.snd)`. -/ +lemma IndepFun.snd_prod {μ : Measure α} [IsProbabilityMeasure μ] {ν : Measure β} [SFinite ν] + {X : β → γ} {T : β → δ} (h : IndepFun X T ν) (hX : Measurable X) (hT : Measurable T) : + IndepFun (fun p : α × β ↦ X p.2) (fun p ↦ (p.1, T p.2)) (μ.prod ν) := by + rw [indepFun_iff_measure_inter_preimage_eq_mul] + intro s t hs ht + rw [indepFun_iff_measure_inter_preimage_eq_mul] at h + have hXs : MeasurableSet ((fun p : α × β ↦ X p.2) ⁻¹' s) := hs.preimage (by fun_prop) + have hYt : MeasurableSet ((fun p : α × β ↦ (p.1, T p.2)) ⁻¹' t) := ht.preimage (by fun_prop) + rw [Measure.prod_apply (hXs.inter hYt), Measure.prod_apply hXs, Measure.prod_apply hYt] + have h_eq : ∀ x, ν (Prod.mk x ⁻¹' ((fun p : α × β ↦ X p.2) ⁻¹' s ∩ (fun p ↦ (p.1, T p.2)) ⁻¹' t)) + = ν (X ⁻¹' s) * (ν.map T) (Prod.mk x ⁻¹' t) := fun x ↦ by + rw [Measure.map_apply hT (ht.preimage measurable_prodMk_left)] + exact h s _ hs (ht.preimage measurable_prodMk_left) + have h_eq' : ∀ x, ν (Prod.mk x ⁻¹' ((fun p : α × β ↦ (p.1, T p.2)) ⁻¹' t)) + = (ν.map T) (Prod.mk x ⁻¹' t) := fun x ↦ by + rw [Measure.map_apply hT (ht.preimage measurable_prodMk_left)] + rfl + have h_eq'' : ∀ x, ν (Prod.mk x ⁻¹' ((fun p : α × β ↦ X p.2) ⁻¹' s)) = ν (X ⁻¹' s) := + fun _ ↦ rfl + simp_rw [h_eq, h_eq', h_eq''] + rw [lintegral_const_mul _ (measurable_measure_prodMk_left ht), lintegral_const, measure_univ, + mul_one] + +/-- If `X` and `T` are independent under `μ`, then under `μ.prod ν` the function `X ∘ Prod.fst` +is independent of `(T ∘ Prod.fst, Prod.snd)`. -/ +lemma IndepFun.fst_prod {μ : Measure α} [SFinite μ] {ν : Measure β} [IsProbabilityMeasure ν] + {X : α → γ} {T : α → δ} (h : IndepFun X T μ) (hX : Measurable X) (hT : Measurable T) : + IndepFun (fun p : α × β ↦ X p.1) (fun p ↦ (T p.1, p.2)) (μ.prod ν) := by + rw [indepFun_iff_measure_inter_preimage_eq_mul] + intro s t hs ht + rw [indepFun_iff_measure_inter_preimage_eq_mul] at h + have hXs : MeasurableSet ((fun p : α × β ↦ X p.1) ⁻¹' s) := hs.preimage (by fun_prop) + have hYt : MeasurableSet ((fun p : α × β ↦ (T p.1, p.2)) ⁻¹' t) := ht.preimage (by fun_prop) + rw [Measure.prod_apply_symm (hXs.inter hYt), Measure.prod_apply_symm hXs, + Measure.prod_apply_symm hYt] + have h_eq : ∀ y, μ ((fun x ↦ (x, y)) ⁻¹' + ((fun p : α × β ↦ X p.1) ⁻¹' s ∩ (fun p ↦ (T p.1, p.2)) ⁻¹' t)) + = μ (X ⁻¹' s) * (μ.map T) ((fun x ↦ (x, y)) ⁻¹' t) := fun y ↦ by + rw [Measure.map_apply hT (ht.preimage measurable_prodMk_right)] + exact h s _ hs (ht.preimage measurable_prodMk_right) + have h_eq' : ∀ y, μ ((fun x ↦ (x, y)) ⁻¹' ((fun p : α × β ↦ (T p.1, p.2)) ⁻¹' t)) + = (μ.map T) ((fun x ↦ (x, y)) ⁻¹' t) := fun y ↦ by + rw [Measure.map_apply hT (ht.preimage measurable_prodMk_right)] + rfl + have h_eq'' : ∀ y, μ ((fun x ↦ (x, y)) ⁻¹' ((fun p : α × β ↦ X p.1) ⁻¹' s)) = μ (X ⁻¹' s) := + fun _ ↦ rfl + simp_rw [h_eq, h_eq', h_eq''] + rw [lintegral_const_mul _ (measurable_measure_prodMk_right ht), lintegral_const, measure_univ, + mul_one] + +end Prod + +/-- A coordinate of an independent family is independent of any function that is measurable +with respect to the other coordinates. -/ +lemma iIndepFun.indepFun_of_measurable_iSup_comap {ι Ω β : Type*} {𝓧 : ι → Type*} + [∀ i, MeasurableSpace (𝓧 i)] {mΩ : MeasurableSpace Ω} {mβ : MeasurableSpace β} + {μ : Measure Ω} {X : ∀ i, Ω → 𝓧 i} (hX : iIndepFun X μ) (hXm : ∀ i, Measurable (X i)) + {S : Set ι} {i : ι} (hi : i ∉ S) {Y : Ω → β} + (hY : Measurable[⨆ j ∈ S, MeasurableSpace.comap (X j) inferInstance] Y) : + IndepFun (X i) Y μ := by + rw [IndepFun_iff_Indep] + refine indep_of_indep_of_le_right ?_ hY.comap_le + have h := indep_iSup_of_disjoint (fun j ↦ (hXm j).comap_le) hX.iIndep (S := {i}) (T := S) + (Set.disjoint_singleton_left.2 hi) + simpa using h + +end ProbabilityTheory diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean index d73ec59e..0adab54b 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean @@ -26,6 +26,11 @@ end MeasurableSpace namespace ProbabilityTheory +lemma hasLaw_eval_infinitePi {ι : Type*} {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)} + (μ : (i : ι) → Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (i : ι) : + HasLaw (Function.eval i) (μ i) (infinitePi μ) := + (measurePreserving_eval_infinitePi μ i).hasLaw + variable {ι κ : Type*} {𝓧 : ι → κ → Type*} [m𝓧 : ∀ i j, MeasurableSpace (𝓧 i j)] {μ : (i : ι) → (j : κ) → Measure (𝓧 i j)} [∀ i j, IsProbabilityMeasure (μ i j)] diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 291fdbae..3506fd35 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -11,7 +11,6 @@ public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfin public import LeanMachineLearning.ForMathlib.Probability.Integrable public import LeanMachineLearning.SequentialLearning.SumRewards public import LeanMachineLearning.SequentialLearning.StationaryEnv -public import Mathlib.Probability.Independence.Integration public import Mathlib.Probability.Kernel.Representation /-! @@ -22,7 +21,7 @@ an infinite array of i.i.d. rewards is first produced for all actions. When the action `a` for the `n`th time, it receives the reward in the row `a` of the array and column `n`. Some statements about bandit algorithms are easier to prove in this space, and can then be -transfered to any other probability space using the fact that the conditinonal distributions of the +transferred to any other probability space using the fact that the conditional distributions of the arms and rewards specified in the bandit model determine their laws uniquely. ## Main definitions @@ -38,7 +37,7 @@ arms and rewards specified in the bandit model determine their laws uniquely. @[expose] public section -open MeasureTheory ProbabilityTheory Filter Real Finset Learning +open MeasureTheory ProbabilityTheory Filter Finset Learning open scoped ENNReal NNReal @@ -59,12 +58,6 @@ instance (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : IsProbabilityMeasure (stream section StreamMeasure -lemma _root_.hasLaw_eval_infinitePi {ι : Type*} {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)} - (μ : (i : ι) → Measure (X i)) [hμ : ∀ i, IsProbabilityMeasure (μ i)] (i : ι) : - HasLaw (Function.eval i) (μ i) (Measure.infinitePi μ) where - aemeasurable := Measurable.aemeasurable (by fun_prop) - map_eq := by exact (measurePreserving_eval_infinitePi μ i).map_eq - lemma hasLaw_eval_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : HasLaw (fun h : ℕ → 𝓐 → R ↦ h n) (Measure.infinitePi ν) (streamMeasure ν) := hasLaw_eval_infinitePi (fun _ ↦ Measure.infinitePi ν) n @@ -89,15 +82,11 @@ lemma integrable_eval_streamMeasure (ν : Kernel 𝓐 ℝ) [IsMarkovKernel ν] ( lemma integral_eval_streamMeasure (ν : Kernel 𝓐 ℝ) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ∫ h, h n a ∂(streamMeasure ν) = (ν a)[id] := by - calc ∫ h, h n a ∂(streamMeasure ν) - _ = ∫ x, x ∂((streamMeasure ν).map (fun h ↦ h n a)) := by - rw [integral_map (Measurable.aemeasurable (by fun_prop)) (by fun_prop)] - _ = (ν a)[id] := by simp [(hasLaw_eval_eval_streamMeasure ν n a).map_eq] + simpa using (hasLaw_eval_eval_streamMeasure ν n a).integral_eq lemma iIndepFun_eval_streamMeasure' (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : iIndepFun (fun n ω ↦ ω n) (streamMeasure ν) := - iIndepFun_infinitePi (P := fun (_ : ℕ) ↦ Measure.infinitePi ν) (Ω := fun _ ↦ 𝓐 → R) - (X := fun i u ↦ u) (fun i ↦ by fun_prop) + iIndepFun_infinitePi fun _ ↦ measurable_id lemma iIndepFun_eval_streamMeasure'' (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) : iIndepFun (fun n ω ↦ ω n a) (streamMeasure ν) := @@ -128,14 +117,7 @@ section ProbabilitySpace variable (𝓐 R) in /-- Probability space for the array model of stochastic bandits. -/ -def probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → R) - -instance {𝓐 R : Type*} [MeasurableSpace R] : MeasurableSpace (probSpace 𝓐 R) := - inferInstanceAs (MeasurableSpace ((ℕ → I) × (ℕ → 𝓐 → R))) - -instance {𝓐 R : Type*} [Countable 𝓐] [MeasurableSpace R] [StandardBorelSpace R] : - StandardBorelSpace (probSpace 𝓐 R) := - inferInstanceAs (StandardBorelSpace ((ℕ → I) × (ℕ → 𝓐 → R))) +abbrev probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → R) /-- Probability measure for the array model of stochastic bandits. -/ noncomputable @@ -145,6 +127,32 @@ def arrayMeasure (ν : Kernel 𝓐 R) : Measure (probSpace 𝓐 R) := instance (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : IsProbabilityMeasure (arrayMeasure ν) := Measure.prod.instIsProbabilityMeasure _ _ +lemma hasLaw_fst_apply_arrayMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : + HasLaw (fun ω : probSpace 𝓐 R ↦ ω.1 n) volume (arrayMeasure ν) := + (hasLaw_eval_infinitePi (fun _ ↦ volume) n).comp (hasLaw_fst_prod _ _) + +lemma hasLaw_snd_apply_arrayMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : + HasLaw (fun ω : probSpace 𝓐 R ↦ ω.2 n a) (ν a) (arrayMeasure ν) := + (hasLaw_eval_eval_streamMeasure ν n a).comp (hasLaw_snd_prod _ _) + +lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 R} [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : + (arrayMeasure ν).map (fun ω ↦ ω.2 n a) = ν a := + (hasLaw_snd_apply_arrayMeasure ν n a).map_eq + +/-- Modification of `ω` in which the rewards of action `a` are read only up to index `m - 1`: +in row `a` of the reward array, the entry at index `i` is kept if `i < m` and replaced by the entry +at index `m + 1 + i` otherwise. The result does not depend on the coordinate `(m, a)` of the +array. -/ +def truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 R) : probSpace 𝓐 R := + (ω.1, fun i b ↦ if b = a then ω.2 (if i < m then i else m + 1 + i) b else ω.2 i b) + +@[fun_prop] +lemma measurable_truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) : + Measurable (truncRow a m : probSpace 𝓐 R → probSpace 𝓐 R) := by + refine Measurable.prodMk measurable_fst + (measurable_pi_lambda _ fun i ↦ measurable_pi_lambda _ fun b ↦ ?_) + by_cases hb : b = a <;> simp only [hb, ↓reduceIte] <;> fun_prop + variable [Nonempty 𝓐] [StandardBorelSpace 𝓐] /-- The initial action is the image of a uniform random variable by this function. -/ @@ -394,7 +402,7 @@ lemma hist_congr (alg : Algorithm 𝓐 R) (n : ℕ) {ω ω' : probSpace 𝓐 R} pullCount' n (fun i ↦ (action alg i ω, reward alg i ω)) (action alg (n + 1) ω') + 1 grind -lemma stepsUntil_congr_aux (alg : Algorithm 𝓐 R) +lemma action_eq_and_pullCount_eq_congr_aux (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 R} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) @@ -420,15 +428,17 @@ lemma stepsUntil_congr_aux (alg : Algorithm 𝓐 R) simp only at h_hist rw [h_hist] -lemma stepsUntil_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 R} +lemma action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) + {ω ω' : probSpace 𝓐 R} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) : (action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m) ↔ (action alg (n + 1) ω' = a ∧ pullCount (action alg) a (n + 1) ω' = m) := - ⟨stepsUntil_congr_aux alg a m n hω1 hω2_ne hω2_eq, - stepsUntil_congr_aux alg a m n (by grind) (by grind) (by grind)⟩ + ⟨action_eq_and_pullCount_eq_congr_aux alg a m n hω1 hω2_ne hω2_eq, + action_eq_and_pullCount_eq_congr_aux alg a m n (by grind) (by grind) (by grind)⟩ -lemma stepsUntil_indicator_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 R} +lemma indicator_action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) + {ω ω' : probSpace 𝓐 R} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) : {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator (fun _ ↦ 1) @@ -436,7 +446,7 @@ lemma stepsUntil_indicator_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator (fun _ ↦ 1) ω' := by simp only [Set.indicator_apply, Set.mem_ofPred_eq] - simp_rw [stepsUntil_congr alg a m n hω1 hω2_ne hω2_eq] + simp_rw [action_eq_and_pullCount_eq_congr alg a m n hω1 hω2_ne hω2_eq] end Congruence @@ -458,133 +468,80 @@ lemma measurable_hist_comap [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) change Measurable ((fun p ↦ p ⟨min i n, by simp⟩) ∘ (fun x : (Iic n → I) × (ℕ → 𝓐 → R) ↦ x.1)) exact Measurable.comp (by fun_prop) measurable_fst -variable [Nonempty R] - --- very bad name -/-- All random variables in the space, except for the unseen rewards for action `a` after -time `n`. -/ +/-- `truncRow` at the number of pulls of `a` up to time `n`: the rewards of action `a` that have +not been observed by time `n` are replaced. The history up to time `n` is measurable with respect +to this function (see `measurable_hist_truncRowPullCount`), and on the event +`pullCount (action alg) a (n + 1) = m` it coincides with `truncRow a m`. -/ noncomputable -def truePast (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 R) : +def truncRowPullCount (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 R) : probSpace 𝓐 R := - (ω.1, fun i b ↦ if b = a then if pullCount (action alg) a (n + 1) ω ≠ 0 then - ω.2 (min i ((pullCount (action alg) a (n + 1) ω) - 1)) a else Nonempty.some inferInstance - else ω.2 i b) - -lemma truePast_eq_of_pullCount_eq (alg : Algorithm 𝓐 R) - (a : 𝓐) (n m : ℕ) (ω : probSpace 𝓐 R) - (h_pc : pullCount (action alg) a (n + 1) ω = m) : - truePast alg a n ω = (ω.1, fun i b ↦ if b = a then if m ≠ 0 then - ω.2 (min i (m - 1)) a else Nonempty.some inferInstance else ω.2 i b) := by - simp [truePast, h_pc] - grind - -lemma truePast_eq_of_pullCount_eq_of_ne_zero (alg : Algorithm 𝓐 R) - (a : 𝓐) (n m : ℕ) (ω : probSpace 𝓐 R) - (h_pc : pullCount (action alg) a (n + 1) ω = m) (hm : m ≠ 0) : - truePast alg a n ω = (ω.1, fun i b ↦ if b = a then - ω.2 (min i (m - 1)) a else ω.2 i b) := by - simp [truePast, h_pc, hm] - grind - -lemma measurable_hist_truePast [Countable 𝓐] (alg : Algorithm 𝓐 R) - (a : 𝓐) (n : ℕ) : - Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] (hist alg · n) := by - have h_eq : (hist alg · n) = (hist alg · n) ∘ (truePast alg a n) := by + truncRow a (pullCount (action alg) a (n + 1) ω) ω + +lemma measurable_hist_truncRowPullCount [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) : + Measurable[MeasurableSpace.comap (truncRowPullCount alg a n) inferInstance] (hist alg · n) := by + have h_eq : (hist alg · n) = (hist alg · n) ∘ (truncRowPullCount alg a n) := by ext ω : 1 refine hist_congr alg n (fun _ _ ↦ rfl) fun i b hi ↦ ?_ by_cases hb : b = a · subst hb - simp only [truePast, ↓reduceIte] - rw [min_eq_left, ite_eq_left (by grind)] - grind - · simp [truePast, hb] + simp [truncRowPullCount, truncRow, hi] + · simp [truncRowPullCount, truncRow, hb] rw [h_eq] - refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl) - fun_prop - -lemma measurable_action_add_one_truePast [Countable 𝓐] (alg : Algorithm 𝓐 R) - (a : 𝓐) (n : ℕ) : - Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] - (action alg (n + 1)) := by - rw [action_add_one_eq] - change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] - ((fun p ↦ algFunction alg n p.1 p.2) ∘ (fun ω ↦ (hist alg ω n, ω.1 (n + 1)))) - refine (measurable_algFunction alg n).comp (Measurable.prodMk ?_ ?_) - · exact measurable_hist_truePast alg a n - · have : (fun ω ↦ ω.1 (n + 1)) = - (fun (p : probSpace 𝓐 R) ↦ p.1 (n + 1)) ∘ (truePast alg a n) := rfl - rw [this] - exact Measurable.comp (by fun_prop) (Measurable.of_comap_le le_rfl) - -lemma measurable_pullCount_add_one_truePast [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) : - Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] - (pullCount (action alg) a (n + 1)) := by - change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] - (fun ω ↦ pullCount (action alg) a (n + 1) ω) - simp_rw [pullCount_eq_sum] - refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop) - refine (measurableSet_singleton _).preimage ?_ - have h_meas := measurable_hist_truePast alg a n - simp_rw [hist_eq _ _ n, @measurable_pi_iff] at h_meas - exact (h_meas ⟨i, by grind⟩).fst - -lemma measurable_stepsUntil [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) : - Measurable[MeasurableSpace.comap - (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b)) inferInstance] + exact (measurable_hist alg n).comp (Measurable.of_comap_le le_rfl) + +lemma measurableSet_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) + (n m : ℕ) : + MeasurableSet {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m} := + MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop)) + ((measurableSet_singleton _).preimage (by fun_prop)) + +lemma preimage_action_pullCount_eq (alg : Algorithm 𝓐 R) (a : 𝓐) (n m : ℕ) : + (fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) + ⁻¹' {(a, m)} = + {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator + (fun _ ↦ 1) ⁻¹' {1} := by + ext ω + simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply, + Set.mem_ofPred_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false, Classical.not_imp, + Decidable.not_not, and_congr_right_iff] + intro ha + simp [ha] + +lemma measurable_indicator_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 R) + (a : 𝓐) (m n : ℕ) : + Measurable[MeasurableSpace.comap (truncRow a m) inferInstance] (({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) := by let f := ({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1) - have h_eq : f = f ∘ - fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b) := by + have h_eq : f = f ∘ truncRow a m := by ext ω - exact stepsUntil_indicator_congr alg a m n (by grind) (by grind) (by grind) - change Measurable[MeasurableSpace.comap - (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b)) inferInstance] f + exact indicator_action_eq_and_pullCount_eq_congr alg a m n (fun _ ↦ rfl) + (fun _ _ hb ↦ by simp [truncRow, hb]) (fun i hi ↦ by simp [truncRow, show i < m by omega]) + change Measurable[MeasurableSpace.comap (truncRow a m) inferInstance] f rw [h_eq] - refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl) - refine Measurable.indicator (by fun_prop) ?_ - exact MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop)) - ((measurableSet_singleton _).preimage (by fun_prop)) + exact (Measurable.indicator (by fun_prop) + (measurableSet_action_eq_and_pullCount_eq alg a n m)).comp (Measurable.of_comap_le le_rfl) -omit [Nonempty R] in lemma measurable_pullCount_action_add_one_hist (alg : Algorithm 𝓐 R) (n : ℕ) : - Measurable[MeasurableSpace.comap (fun ω ↦ (action alg (n + 1) ω, hist alg ω n)) inferInstance] + Measurable[MeasurableSpace.comap (fun ω ↦ (hist alg ω n, action alg (n + 1) ω)) inferInstance] (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by simp_rw [pullCount_eq_sum] refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop) - refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_fst) + refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_snd) rw [measurable_iff_comap_le] simp_rw [hist_eq _ _ n] rw [← measurable_iff_comap_le] unfold action refine Measurable.fst (mγ := inferInstance) ?_ have : (hist alg · i ⟨i, by grind⟩) = - (fun ω : 𝓐 × (Iic n → 𝓐 × R) ↦ ω.2 ⟨i, by grind⟩) ∘ - (fun ω ↦ (action alg (n + 1) ω, fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩)) := rfl + (fun ω : (Iic n → 𝓐 × R) × 𝓐 ↦ ω.1 ⟨i, by grind⟩) ∘ + (fun ω ↦ (fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩, action alg (n + 1) ω)) := rfl rw [this] exact measurable_comp_comap _ (Measurable.prodMk (by fun_prop) (by fun_prop)) end MeasurabilityAdvanced -set_option backward.isDefEq.respectTransparency false in -omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in -lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 R} [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : - (arrayMeasure ν).map (fun ω ↦ ω.2 n a) = ν a := by - calc (arrayMeasure ν).map (fun ω ↦ ω.2 n a) - _ = (arrayMeasure ν).snd.map (fun ω ↦ ω n a) := by - unfold Measure.snd - rw [Measure.map_map (by fun_prop) (by fun_prop)] - rfl - _ = ν a := by - rw [arrayMeasure, Measure.snd_prod, streamMeasure] - have : (fun ω ↦ ω n a) = (fun h : 𝓐 → R ↦ h a) ∘ (fun ω : ℕ → 𝓐 → R ↦ ω n) := rfl - rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), Measure.infinitePi_map_eval, - Measure.infinitePi_map_eval] - section Independence omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in @@ -598,55 +555,16 @@ lemma indepFun_fst_zero_snd_zero_action (ν : Kernel 𝓐 R) [IsMarkovKernel ν] indepFun_prod (X := fun ω : ℕ → I ↦ ω 0) (Y := fun ω : ℕ → 𝓐 → R ↦ ω 0 a) (by fun_prop) (by fun_prop) --- proved by Claude, then slightly golfed -omit [DecidableEq 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓐] in +omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : (fun ω ↦ ω.1 (n + 1)) ⟂ᵢ[arrayMeasure ν] (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by - let μ₁ : Measure (ℕ → I) := Measure.infinitePi fun _ ↦ volume - let μ₂ : Measure (ℕ → 𝓐 → R) := streamMeasure ν - -- Coordinates of μ₁ are independent - have h_indep : iIndepFun (fun i (ω : ℕ → I) ↦ ω i) μ₁ := - iIndepFun_infinitePi (fun _ ↦ measurable_id) - have h_indep_n : IndepFun (fun ω ↦ ω (n + 1)) (fun ω ↦ fun i : Iic n ↦ ω i) μ₁ := by - have h := h_indep.indepFun_finset₀ {n + 1} (Iic n) (by simp) - (fun i ↦ (measurable_pi_apply i).aemeasurable) - convert h.comp (measurable_pi_apply ⟨n + 1, by simp⟩) measurable_id using 1 - · rfl - · rfl - rw [indepFun_iff_measure_inter_preimage_eq_mul] - intro s t hs ht - let X : (ℕ → I) × (ℕ → 𝓐 → R) → I := fun ω ↦ ω.1 (n + 1) - let Y : (ℕ → I) × (ℕ → 𝓐 → R) → (Iic n → I) × (ℕ → 𝓐 → R) := fun ω ↦ (fun i ↦ ω.1 i, ω.2) - change (μ₁.prod μ₂) (X ⁻¹' s ∩ Y ⁻¹' t) = (μ₁.prod μ₂) (X ⁻¹' s) * (μ₁.prod μ₂) (Y ⁻¹' t) - -- Rewrite using Fubini - rw [Measure.prod_apply (hs.preimage (by fun_prop : Measurable X)), - Measure.prod_apply (ht.preimage (by fun_prop : Measurable Y)), - Measure.prod_apply ((hs.preimage (by fun_prop : Measurable X)).inter - (ht.preimage (by fun_prop : Measurable Y)))] - -- Compute fibers - have hX_fst ω₁ : μ₂ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s)) = s.indicator 1 (ω₁ (n + 1)) := by - simp only [X, Set.preimage_preimage] - by_cases h : ω₁ (n + 1) ∈ s <;> simp [h] - have hY_fst ω₁ : μ₂ (Prod.mk ω₁ ⁻¹' (Y ⁻¹' t)) = μ₂ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} := rfl - have hXY ω₁ : μ₂ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s ∩ Y ⁻¹' t)) = - s.indicator 1 (ω₁ (n + 1)) * μ₂ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} := by - simp only [X, Y, Set.preimage_inter, Set.preimage_preimage] - by_cases h : ω₁ (n + 1) ∈ s - · simp [h] - congr - · simp [h] - simp_rw [hY_fst, hX_fst, hXY] - -- Factor the integral using independence - let g : (Iic n → I) → ENNReal := fun x ↦ μ₂ {y | (x, y) ∈ t} - have hg_meas : Measurable g := measurable_measure_prodMk_left ht - have hf_meas : Measurable (fun ω₁ : ℕ → I ↦ s.indicator (1 : I → ENNReal) (ω₁ (n + 1))) := - (measurable_one.indicator hs).comp (measurable_pi_apply _) - have hindep_fg : IndepFun (fun ω₁ ↦ s.indicator (1 : I → ENNReal) (ω₁ (n + 1))) - (fun ω₁ ↦ g (fun i ↦ ω₁ i)) μ₁ := - h_indep_n.comp (measurable_one.indicator hs) hg_meas - have h_eq (ω₁ : ℕ → I) : μ₂ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} = g (fun i ↦ ω₁ i) := rfl - simp_rw [h_eq] - exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun hf_meas (by fun_prop) hindep_fg + have h : IndepFun (fun ω : ℕ → I ↦ ω (n + 1)) (fun ω (i : Iic n) ↦ ω i) + (Measure.infinitePi fun _ ↦ volume) := by + refine (iIndepFun_infinitePi fun _ ↦ measurable_id).indepFun_of_measurable_iSup_comap + (fun _ ↦ measurable_pi_apply _) (S := Set.Iic n) (by simp) ?_ + rw [measurable_iff_comap_le, MeasurableSpace.comap_pi] + exact iSup_le fun i ↦ le_iSup₂_of_le (i : ℕ) (Set.mem_Iic.2 (Finset.mem_Iic.1 i.2)) le_rfl + exact h.fst_prod (ν := streamMeasure ν) (by fun_prop) (by fun_prop) variable [StandardBorelSpace R] [Nonempty R] @@ -655,284 +573,62 @@ lemma indepFun_fst_add_one_hist [Countable 𝓐] (alg : Algorithm 𝓐 R) IndepFun (fun ω ↦ ω.1 (n + 1)) (hist alg · n) (arrayMeasure ν) := (indepFun_fst_add_one_aux ν n).of_measurable_right (measurable_hist_comap alg n) --- proved by Claude -set_option backward.isDefEq.respectTransparency false in -omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [StandardBorelSpace R] in -lemma indepFun_snd_apply_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (m : ℕ) : - (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν] - (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b)) := by - unfold arrayMeasure - let μ₁ : Measure (ℕ → I) := Measure.infinitePi fun _ ↦ volume - let μ₂ : Measure (ℕ → 𝓐 → R) := Measure.infinitePi fun _ ↦ Measure.infinitePi ν - -- Independence within μ₂: coordinates ω i are independent - have h_indep₂ : iIndepFun (fun i (ω : ℕ → 𝓐 → R) ↦ ω i) μ₂ := - iIndepFun_infinitePi (fun _ ↦ measurable_id) - -- Independence within each infinitePi ν: coordinates f b are independent - have h_indep_inner : iIndepFun (fun (b : 𝓐) (f : 𝓐 → R) ↦ f b) (Measure.infinitePi ν) := - iIndepFun_infinitePi (fun _ ↦ measurable_id) - rw [indepFun_iff_measure_inter_preimage_eq_mul] - intro s t hs ht - let X : (ℕ → I) × (ℕ → 𝓐 → R) → R := fun ω ↦ ω.2 m a - let Y : (ℕ → I) × (ℕ → 𝓐 → R) → (ℕ → I) × (ℕ → 𝓐 → R) := - fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b) - have hX_meas : Measurable X := - (measurable_pi_apply a).comp ((measurable_pi_apply m).comp measurable_snd) - have hY_meas : Measurable Y := by - change Measurable (fun ω : (ℕ → I) × (ℕ → 𝓐 → R) ↦ - (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b)) - refine Measurable.prod measurable_fst ?_ - refine measurable_pi_lambda _ (fun k ↦ ?_) - refine measurable_pi_lambda _ (fun b ↦ ?_) - by_cases hb : b = a - · simp only [hb, ↓reduceIte] - by_cases hm : m ≠ 0 - · simp only [ne_eq, hm, not_false_eq_true, ↓reduceIte] - exact (measurable_pi_apply a).comp - ((measurable_pi_apply (min k (m - 1))).comp measurable_snd) - · simp only [hm, ↓reduceIte] - exact measurable_const - · simp only [hb, ↓reduceIte] - exact (measurable_pi_apply b).comp ((measurable_pi_apply k).comp measurable_snd) - change (μ₁.prod μ₂) (X ⁻¹' s ∩ Y ⁻¹' t) = (μ₁.prod μ₂) (X ⁻¹' s) * (μ₁.prod μ₂) (Y ⁻¹' t) - -- Use Fubini on μ₁.prod μ₂ - rw [Measure.prod_apply (hs.preimage hX_meas), - Measure.prod_apply (ht.preimage hY_meas), - Measure.prod_apply ((hs.preimage hX_meas).inter (ht.preimage hY_meas))] - -- X only depends on ω₂, so its fiber is constant in ω₁ - have hX_fst : ∀ ω₁, μ₂ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s)) = μ₂ ((fun ω₂ ↦ ω₂ m a) ⁻¹' s) := fun _ ↦ rfl - simp_rw [hX_fst] - -- The LHS integral: fiber of X ∩ Y at ω₁ - -- Key: X depends only on ω₂ m a, while Y's dependence on ω₂ avoids (m, a) - -- Define the "truncation" map on ω₂ - let trunc : (ℕ → 𝓐 → R) → (ℕ → 𝓐 → R) := - fun ω₂ k b ↦ if b = a then if m ≠ 0 then ω₂ (min k (m - 1)) b - else Nonempty.some inferInstance else ω₂ k b - -- The fiber of Y at ω₁ only depends on trunc(ω₂) - have hY_fiber : ∀ ω₁, Prod.mk ω₁ ⁻¹' (Y ⁻¹' t) = (fun ω₂ ↦ (ω₁, trunc ω₂)) ⁻¹' t := fun _ ↦ rfl - -- The fiber of X ∩ Y factors - have hXY_fiber : ∀ ω₁, Prod.mk ω₁ ⁻¹' (X ⁻¹' s ∩ Y ⁻¹' t) = - ((fun ω₂ ↦ ω₂ m a) ⁻¹' s) ∩ ((fun ω₂ ↦ (ω₁, trunc ω₂)) ⁻¹' t) := fun _ ↦ rfl - simp_rw [hXY_fiber, hY_fiber] - -- Now we use independence in μ₂: (ω₂ m a) is independent of (trunc ω₂) - -- because trunc only uses indices (k, a) with k < m, and (k, b) with b ≠ a - have h_trunc_meas : Measurable trunc := by - refine measurable_pi_lambda _ (fun k ↦ ?_) - refine measurable_pi_lambda _ (fun b ↦ ?_) - simp only [trunc] +omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [StandardBorelSpace R] [Nonempty R] in +/-- The reward `ω.2 m a` is independent of `truncRow a m`, which reads only other coordinates. -/ +lemma indepFun_snd_apply_truncRow (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (m : ℕ) : + (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν] (truncRow a m) := by + let T : (ℕ → 𝓐 → R) → (ℕ → 𝓐 → R) := + fun ω k b ↦ if b = a then ω (if k < m then k else m + 1 + k) b else ω k b + have hT : Measurable[⨆ p ∈ {p : ℕ × 𝓐 | p ≠ (m, a)}, + MeasurableSpace.comap (fun ω : ℕ → 𝓐 → R ↦ ω p.1 p.2) inferInstance] T := by + rw [measurable_iff_comap_le, MeasurableSpace.comap_pi] + refine iSup_le fun k ↦ ?_ + rw [MeasurableSpace.comap_pi] + refine iSup_le fun b ↦ ?_ by_cases hb : b = a - · simp only [hb, ↓reduceIte] - by_cases hm : m = 0 - · simp only [hm] - exact measurable_const - · simp only [ne_eq, hm, not_false_eq_true, ↓reduceIte] - exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1))) - · simp only [hb, ↓reduceIte] - exact (measurable_pi_apply b).comp (measurable_pi_apply k) - -- Key independence: (ω₂ m a) ⟂ trunc because trunc only uses coordinates ≠ (m, a) - have h_indep_trunc : IndepFun (fun ω₂ ↦ ω₂ m a) trunc μ₂ := by - -- Factor trunc through proj which extracts the relevant coordinates - let proj : (ℕ → 𝓐 → R) → ((ℕ → R) × (ℕ → {b : 𝓐 // b ≠ a} → R)) := fun ω₂ ↦ - (fun k ↦ if m ≠ 0 then ω₂ (min k (m - 1)) a else Nonempty.some inferInstance, - fun k ⟨b, _⟩ ↦ ω₂ k b) - have h_trunc_proj : ∀ ω₂, trunc ω₂ = (fun p k b ↦ - if h : b = a then if m ≠ 0 then p.1 k - else Nonempty.some inferInstance else p.2 k ⟨b, h⟩) (proj ω₂) := by - intro ω₂; ext k b; simp only [trunc, proj]; by_cases hb : b = a <;> simp [hb]; grind - have h_proj_meas : Measurable proj := by - refine Measurable.prod ?_ ?_ - · refine measurable_pi_lambda _ fun k ↦ ?_ - by_cases hm : m ≠ 0 - · simp only [proj, ne_eq, hm, not_false_eq_true, ↓reduceIte] - exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1))) - · simp [proj, hm] - · exact measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun ⟨b, _⟩ ↦ - (measurable_pi_apply b).comp (measurable_pi_apply k))) - have h_g_meas : Measurable (fun p : (ℕ → R) × (ℕ → {b : 𝓐 // b ≠ a} → R) ↦ - (fun k b ↦ if h : b = a then if m ≠ 0 then p.1 k else Nonempty.some inferInstance - else p.2 k ⟨b, h⟩)) := by - refine measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun b ↦ ?_)) - by_cases hb : b = a - · simp only [hb, ↓reduceDIte] - by_cases hm : m ≠ 0 - · simp only [ne_eq, hm, not_false_eq_true] - exact (measurable_pi_apply k).comp measurable_fst - · simp [hm] - · simp only [hb, ↓reduceDIte] - exact (measurable_pi_apply (⟨b, hb⟩ : {b : 𝓐 // b ≠ a})).comp - ((measurable_pi_apply k).comp measurable_snd) - -- Show (ω₂ m a) ⟂ proj: proj uses coordinates disjoint from (m, a) - have h_indep_proj : IndepFun (fun ω₂ ↦ ω₂ m a) proj μ₂ := by - have h_row_bound (hm : m ≠ 0) : ∀ k, min k (m - 1) < m := by - intro k - calc min k (m - 1) ≤ m - 1 := Nat.min_le_right k (m - 1) - _ < m := Nat.sub_lt (by grind) Nat.one_pos - rw [indepFun_iff_measure_inter_preimage_eq_mul] - intro s t' hs ht' - -- rows_lt_m extracts column a at rows < m, other_cols extracts columns ≠ a - let rows_lt_m : (ℕ → 𝓐 → R) → (Iio m → R) := fun ω₂ ⟨j, _⟩ ↦ ω₂ j a - let other_cols : (ℕ → 𝓐 → R) → (ℕ → {b : 𝓐 // b ≠ a} → R) := fun ω₂ k ⟨b, _⟩ ↦ ω₂ k b - have h_proj_factor : ∀ ω₂, proj ω₂ = - ((fun r k ↦ if hm : m ≠ 0 then r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩ - else Nonempty.some inferInstance) (rows_lt_m ω₂), - other_cols ω₂) := by - intro ω₂; ext1 - · ext k - by_cases hm : m ≠ 0 - · simp [proj, rows_lt_m, hm] - · simp [proj, hm] - · rfl - -- Use iIndepFun structure of the doubly-indexed infinite product - have h_iindep : iIndepFun (fun (p : ℕ × 𝓐) ω ↦ ω p.1 p.2) μ₂ := - iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (fun _ ↦ ν) (by fun_prop) - have h_rows_meas : Measurable rows_lt_m := - measurable_pi_lambda _ (fun ⟨j, _⟩ ↦ (measurable_pi_apply a).comp (measurable_pi_apply j)) - have h_other_meas : Measurable other_cols := - measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun ⟨b, _⟩ ↦ - (measurable_pi_apply b).comp (measurable_pi_apply k))) - -- Show (ω₂ m a) ⟂ (rows_lt_m, other_cols) via indep_iSup_of_disjoint - have h_indep_combined : IndepFun (fun ω₂ ↦ ω₂ m a) - (fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) μ₂ := by - rw [IndepFun_iff_Indep] - have h_comap_le : (MeasurableSpace.pi.prod MeasurableSpace.pi).comap - (fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) ≤ - ⨆ (p : {p : ℕ × 𝓐 // p ≠ (m, a)}), mR.comap (fun ω ↦ ω p.val.1 p.val.2) := by - rw [MeasurableSpace.comap_prodMk] - refine sup_le ?_ ?_ - · rw [MeasurableSpace.comap_pi] - refine iSup_le (fun ⟨j, hj⟩ ↦ ?_) - have h_ne : (j, a) ≠ (m, a) := fun h ↦ (Finset.mem_Iio.mp hj).ne (Prod.mk.inj h).1 - exact le_iSup_of_le ⟨(j, a), h_ne⟩ le_rfl - · rw [MeasurableSpace.comap_pi] - refine iSup_le (fun k ↦ ?_) - rw [MeasurableSpace.comap_pi] - refine iSup_le (fun ⟨b, hb⟩ ↦ ?_) - have h_ne : (k, b) ≠ (m, a) := fun h ↦ hb (Prod.mk.inj h).2 - exact le_iSup_of_le ⟨(k, b), h_ne⟩ le_rfl - refine indep_of_indep_of_le_right ?_ h_comap_le - have h_disjoint : Disjoint ({(m, a)} : Set (ℕ × 𝓐)) {p | p ≠ (m, a)} := by simp - have h_le : ∀ p : ℕ × 𝓐, mR.comap (fun ω : ℕ → 𝓐 → R ↦ ω p.1 p.2) ≤ - MeasurableSpace.pi (m := fun _ ↦ MeasurableSpace.pi) := fun p ↦ - Measurable.comap_le ((measurable_pi_apply p.2).comp (measurable_pi_apply p.1)) - have h_iindep' : iIndep (fun p : ℕ × 𝓐 ↦ mR.comap (fun ω : ℕ → 𝓐 → R ↦ ω p.1 p.2)) μ₂ := - h_iindep.iIndep - have h_indep := indep_iSup_of_disjoint h_le h_iindep' h_disjoint - convert h_indep using 2 - · simp only [Set.mem_singleton_iff, iSup_iSup_eq_left] - · simp only [ne_eq, Set.mem_ofPred_eq, iSup_subtype'] - have h_proj_preimage : proj ⁻¹' t' = (fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) ⁻¹' - {p | ((fun r k ↦ if hm : m ≠ 0 then - r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩ - else Nonempty.some inferInstance) p.1, p.2) ∈ t'} - := by ext ω₂; simp only [Set.mem_preimage, Set.mem_ofPred_eq, h_proj_factor] - rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_combined - rw [h_proj_preimage] - let T : Set ((Iio m → R) × (ℕ → {b : 𝓐 // b ≠ a} → R)) := - {p | ((fun r k ↦ if hm : m ≠ 0 then - r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩ - else Nonempty.some inferInstance) p.1, p.2) ∈ t'} - have hT_meas : MeasurableSet T := by - refine ht'.preimage (Measurable.prod ?_ measurable_snd) - refine measurable_pi_lambda _ (fun k ↦ ?_) - by_cases hm : m ≠ 0 - · simp only [ne_eq, hm, not_false_eq_true, ↓reduceDIte] - exact (measurable_pi_apply (⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩ : - Iio m)).comp measurable_fst - · simp [hm] - change μ₂ ((fun ω₂ ↦ ω₂ m a) ⁻¹' s ∩ (fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) ⁻¹' T) = - μ₂ ((fun ω₂ ↦ ω₂ m a) ⁻¹' s) * - μ₂ ((fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) ⁻¹' T) - exact h_indep_combined s T hs hT_meas - have h_eq : trunc = (fun p k b ↦ if h : b = a then if m ≠ 0 then p.1 k - else Nonempty.some inferInstance else p.2 k ⟨b, h⟩) ∘ proj := by - funext ω₂; exact h_trunc_proj ω₂ - rw [h_eq] - exact h_indep_proj.comp measurable_id h_g_meas - rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_trunc - have h_const : ∀ ω₁, μ₂ (((fun ω₂ ↦ ω₂ m a) ⁻¹' s) ∩ ((fun ω₂ ↦ (ω₁, trunc ω₂)) ⁻¹' t)) = - μ₂ ((fun ω₂ ↦ ω₂ m a) ⁻¹' s) * μ₂ ((fun ω₂ ↦ (ω₁, trunc ω₂)) ⁻¹' t) := fun ω₁ ↦ - h_indep_trunc s _ hs (ht.preimage (by fun_prop)) - simp_rw [h_const] - let c := μ₂ ((fun ω₂ ↦ ω₂ m a) ⁻¹' s) - change ∫⁻ x, c * μ₂ ((fun ω₂ ↦ (x, trunc ω₂)) ⁻¹' t) ∂μ₁ = - (∫⁻ _, c ∂μ₁) * ∫⁻ x, μ₂ ((fun ω₂ ↦ (x, trunc ω₂)) ⁻¹' t) ∂μ₁ - have h_preimage : ∀ x, (fun ω₂ ↦ (x, trunc ω₂)) ⁻¹' t = trunc ⁻¹' (Prod.mk x ⁻¹' t) := fun _ ↦ rfl - simp_rw [h_preimage] - have h_map : ∀ x, μ₂ (trunc ⁻¹' (Prod.mk x ⁻¹' t)) = (μ₂.map trunc) (Prod.mk x ⁻¹' t) := by - intro x; rw [Measure.map_apply h_trunc_meas (ht.preimage (by fun_prop))] - simp_rw [h_map] - rw [lintegral_const_mul _ (measurable_measure_prodMk_left_finite ht), - lintegral_const, measure_univ, mul_one] - -omit [StandardBorelSpace R] in + · simp only [T, hb, ↓reduceIte] + refine le_iSup₂_of_le (if k < m then k else m + 1 + k, a) ?_ (le_of_eq rfl) + simp only [Set.mem_ofPred_eq, ne_eq, Prod.mk.injEq, and_true] + split_ifs <;> omega + · simp only [T, hb, ↓reduceIte] + exact le_iSup₂_of_le (k, b) (by simp [hb]) (le_of_eq rfl) + have hTm : Measurable T := + hT.mono (iSup₂_le fun p _ ↦ Measurable.comap_le (by fun_prop)) le_rfl + have h := (iIndepFun_eval_streamMeasure ν).indepFun_of_measurable_iSup_comap + (fun _ ↦ by fun_prop) (i := (m, a)) (by simp) hT + exact h.snd_prod (μ := Measure.infinitePi fun _ ↦ volume) (by fun_prop) hTm + +omit [StandardBorelSpace R] [Nonempty R] in lemma indepFun_snd_apply_pullCount_action [Countable 𝓐] (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (m n : ℕ) : (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν] ({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1) := - (indepFun_snd_apply_aux ν a m).of_measurable_right (measurable_stepsUntil alg a m n) - -lemma indepFun_cond_comp {𝓐 β γ δ : Type*} {m𝓐 : MeasurableSpace 𝓐} {mβ : MeasurableSpace β} - {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure 𝓐} - {X : 𝓐 → β} {Y : 𝓐 → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y) - {Z : γ → δ} (hZ : Measurable Z) (z : δ) : - X ⟂ᵢ[μ[|(Z ∘ Y) ⁻¹' {z}]] Y := by - have h_preim : (Z ∘ Y) ⁻¹' {z} = Y ⁻¹' (Z ⁻¹' {z}) := by grind - simp_rw [h_preim] - exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z)) + (indepFun_snd_apply_truncRow ν a m).of_measurable_right + (measurable_indicator_action_eq_and_pullCount_eq alg a m n) lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (n m : ℕ) : (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]] (hist alg · n) := by - have h_meas := measurable_hist_truePast alg a n - refine IndepFun.of_measurable_right ?_ h_meas - have h_ae_eq : truePast alg a n =ᵐ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, + refine IndepFun.of_measurable_right ?_ (measurable_hist_truncRowPullCount alg a n) + have h_ae_eq : truncRowPullCount alg a n =ᵐ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]] - (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b)) := by - refine ae_cond_of_forall_mem ?_ fun x hx ↦ ?_ - · refine (measurableSet_singleton _).preimage ?_ - have h_meas_pc : Measurable fun ω ↦ - pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by - change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ - (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) - exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) - fun_prop + truncRow a m := by + refine ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) + fun x hx ↦ ?_ simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq] at hx - simp only [truePast] - congr with i b - by_cases hb : b = a - · simp only [hb, ↓reduceIte] - simp only [hx.1, true_and] at hx - congr! - · simp [hb] + obtain ⟨hxa, hxm⟩ := hx + rw [hxa] at hxm + simp only [truncRowPullCount, hxm] refine IndepFun.congr ?_ EventuallyEq.rfl h_ae_eq.symm - suffices (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(({ω | action alg (n + 1) ω = a ∧ - pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) ⁻¹' {1}]] - fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b - else Nonempty.some inferInstance else ω.2 k b) by - convert this using 1 - congr! - congr with ω - simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply, - Set.mem_ofPred_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false, - Classical.not_imp, Decidable.not_not, and_congr_right_iff] - intro ha - simp [ha] - have h_meas := measurable_stepsUntil alg a m n - obtain ⟨f, hf, hf_eq⟩ := h_meas.exists_eq_measurable_comp + rw [preimage_action_pullCount_eq] + obtain ⟨f, hf, hf_eq⟩ := + (measurable_indicator_action_eq_and_pullCount_eq alg a m n).exists_eq_measurable_comp simp_rw [hf_eq] - refine indepFun_cond_comp (Z := f) (z := 1) ?_ ?_ hf - · exact indepFun_snd_apply_aux ν a m - · refine Measurable.prodMk (by fun_prop) ?_ - simp_rw [measurable_pi_iff] - intro i b - refine Measurable.ite (MeasurableSet.const _) ?_ (by fun_prop) - refine Measurable.ite (MeasurableSet.const _) (by fun_prop) (by fun_prop) + exact indepFun_cond_comp (Z := f) (z := 1) (indepFun_snd_apply_truncRow ν a m) + (measurable_truncRow a m) hf end Independence @@ -940,19 +636,12 @@ section Laws variable [Countable 𝓐] -set_option backward.isDefEq.respectTransparency false in +omit [Countable 𝓐] in lemma hasLaw_action_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : - HasLaw (action alg 0) alg.p0 (arrayMeasure ν) where - map_eq := by - calc (arrayMeasure ν).map (fun ω ↦ initAlgFunction alg (ω.1 0)) - _ = ((arrayMeasure ν).fst.map (Function.eval 0)).map (initAlgFunction alg) := by - rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop), - Measure.map_map (by fun_prop) (by fun_prop)] - rfl - _ = (volume : Measure I).map (initAlgFunction alg) := by - simp only [arrayMeasure, Measure.fst_prod] - rw [(measurePreserving_eval_infinitePi (fun _ ↦ volume) 0).map_eq] - _ = alg.p0 := initAlgFunction_map alg + HasLaw (action alg 0) alg.p0 (arrayMeasure ν) := by + rw [action_zero] + exact (⟨(measurable_initAlgFunction alg).aemeasurable, initAlgFunction_map alg⟩ : + HasLaw (initAlgFunction alg) alg.p0 volume).comp (hasLaw_fst_apply_arrayMeasure ν 0) variable [StandardBorelSpace R] [Nonempty R] @@ -984,114 +673,23 @@ lemma hasCondDistrib_reward_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [ lemma hasCondDistrib_action' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (action alg (n + 1)) (hist alg · n) (alg.policy n) (arrayMeasure ν) := by - rw [action_add_one_eq] - have h_fun ω := algFunction_map alg n (hist alg ω n) - refine ⟨by fun_prop, ?_⟩ - have h_indep : (arrayMeasure ν).map (fun ω ↦ (ω.1 (n + 1), hist alg ω n)) = - (ℙ).prod ((arrayMeasure ν).map (hist alg · n)) := by - have h_indep' := indepFun_fst_add_one_hist alg ν n - rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)] at h_indep' - rw [h_indep'] - congr - simp only [arrayMeasure] - calc ((Measure.infinitePi fun x ↦ ℙ).prod (streamMeasure ν)).map (fun ω ↦ ω.1 (n + 1)) - _ = (Measure.infinitePi fun x ↦ ℙ).map (Function.eval (n + 1)) := by - nth_rw 2 [← Measure.fst_prod (μ := Measure.infinitePi fun x ↦ ℙ) - (ν := streamMeasure ν)] - rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop)] - rfl - _ = ℙ := by rw [Measure.infinitePi_map_eval] - have : (fun x ↦ (hist alg x n, algFunction alg n (hist alg x n) (x.1 (n + 1)))) = - (fun p ↦ (p.2, algFunction alg n (p.2) (p.1))) ∘ (fun x ↦ (x.1 (n + 1), hist alg x n)) := rfl - rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), h_indep] - have : (ℙ : Measure I).prod ((arrayMeasure ν).map (hist alg · n)) = - ((Kernel.const _ ℙ) ×ₖ Kernel.id) ∘ₘ ((arrayMeasure ν).map (hist alg · n)) := by - have h := Measure.compProd_const (μ := (arrayMeasure ν).map (hist alg · n)) - (ν := (ℙ : Measure I)) - rw [Measure.compProd_eq_comp_prod] at h - rw [← Measure.prod_swap, ← h, ← Measure.deterministic_comp_eq_map (by fun_prop), - Measure.comp_assoc, ← Kernel.swap, Kernel.swap_prod] - rw [this, ← Measure.deterministic_comp_eq_map (by fun_prop), - ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.compProd_eq_comp_prod, - Measure.comp_assoc, Measure.comp_assoc, Measure.comp_assoc] - congr 2 - ext ω : 1 - simp only [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap, Kernel.coe_comap, - Function.comp_apply] - rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.const_apply, Kernel.id_apply, - Kernel.prod_apply, Kernel.id_apply, ← h_fun] - calc (((ℙ).prod (Measure.dirac (hist alg ω n)))).map (fun p ↦ (p.2, algFunction alg n p.2 p.1)) - _ = (((ℙ).prod (Measure.dirac (hist alg ω n))).map Prod.swap).map - (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by - rw [Measure.map_map (by fun_prop) (by fun_prop)] + have hU : HasCondDistrib (fun ω ↦ ω.1 (n + 1)) (fun ω ↦ (hist alg ω n, hist alg ω n)) + (Kernel.const _ volume) (arrayMeasure ν) := + ((indepFun_fst_add_one_hist alg ν n).symm.comp (measurable_id.prodMk measurable_id) + measurable_id).hasCondDistrib_const (by fun_prop) (hasLaw_fst_apply_arrayMeasure ν (n + 1)) + have h := ((hasCondDistrib_self (X := (hist alg · n)) (by fun_prop)).prod hU).comp_left + (measurable_algFunction alg n) + have h_ker : alg.policy n = (Kernel.id ⊗ₖ Kernel.const _ volume).map + (Function.uncurry (algFunction alg n)) := by + ext h s hs + rw [Kernel.map_apply' _ (measurable_algFunction alg n) _ hs, + Kernel.compProd_apply (measurable_algFunction alg n hs), Kernel.id_apply] + simp only [Kernel.const_apply] + rw [lintegral_dirac' _ (measurable_measure_prodMk_left (measurable_algFunction alg n hs)), + ← algFunction_map alg n h, Measure.map_apply (by fun_prop) hs] rfl - _ = ((Measure.dirac (hist alg ω n)).prod ℙ).map (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by - rw [Measure.prod_swap] - _ = (Measure.dirac (hist alg ω n)).prod ((ℙ).map (algFunction alg n (hist alg ω n))) := by - ext s hs - rw [Measure.map_apply (by fun_prop) hs, Measure.prod_apply, lintegral_dirac, Measure.prod_apply, - lintegral_dirac, Measure.map_apply (by fun_prop)] - · congr - · exact hs.preimage (by fun_prop) - · exact hs - · exact hs.preimage (by fun_prop) - -/-- The conditional distribution of the reward at time `n + 1`, given the action at time `n + 1` -and the number of times that action has been pulled before time `n + 1`, is equal to -the kernel `ν`. -/ -lemma hasCondDistrib_reward_pullCount_action - (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : - HasCondDistrib (reward alg (n + 1)) - (fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) - (ν.prodMkRight _) (arrayMeasure ν) := by - have h_meas : Measurable fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by - change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ - (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) - exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) - refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ - refine (condDistrib_ae_eq_cond - (Measurable.prodMk (by fun_prop) (by fun_prop)) (by fun_prop)).trans ?_ - rw [Filter.EventuallyEq, ae_iff_of_countable] - intro ⟨a, m⟩ ham - simp only [Kernel.prodMkRight_apply] - calc - Measure.map (reward alg (n + 1)) - (arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, - pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}] - _ = Measure.map (fun ω ↦ ω.2 m a) - (arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, - pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}] := by - rw [reward_eq] - refine Measure.map_congr - (ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) (fun x hx ↦ ?_)) - simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq] at hx - simp only [hx.1] at hx ⊢ - simp [hx.2] - _ = Measure.map (fun ω ↦ ω.2 m a) - (arrayMeasure ν)[|({ω | action alg (n + 1) ω = a ∧ - pullCount (action alg) a (n + 1) ω = m}).indicator 1 ⁻¹' {1}] := by - congr with ω - simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply, - Set.mem_ofPred_eq, Pi.one_apply, ite_eq_left_iff, not_and, zero_ne_one, imp_false, - Classical.not_imp, Decidable.not_not, and_congr_right_iff] - intro ha - simp [ha] - _ = ν a := by - rw [cond_of_indepFun, map_snd_apply_arrayMeasure m a] - · exact (indepFun_snd_apply_pullCount_action alg ν a m n).symm - · refine Measurable.indicator (by fun_prop) ?_ - exact MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop)) - ((measurableSet_singleton _).preimage (by fun_prop)) - · fun_prop - · simp - · rw [Measure.map_apply (by fun_prop) (by simp)] at ham - convert ham - ext ω - simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply, - Set.mem_singleton_iff, ite_eq_left_iff, not_and, zero_ne_one, imp_false, Classical.not_imp, - Decidable.not_not, Prod.mk.injEq, and_congr_right_iff] - intro ha - simp [ha] + rw [action_add_one_eq, h_ker] + exact h omit [StandardBorelSpace R] [Nonempty R] in lemma reward_ae_eq_cond (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) (a : 𝓐) (n m : ℕ) : @@ -1100,11 +698,7 @@ lemma reward_ae_eq_cond (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) (a : 𝓐) (fun ω ↦ ω.2 m a) := by rw [reward_eq] refine ae_cond_of_forall_mem ?_ ?_ - · have : Measurable fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by - change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ - (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) - exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) - exact (measurableSet_singleton _).preimage (by fun_prop) + · exact (measurableSet_singleton _).preimage (by fun_prop) intro ω hω simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq] at hω simp only [hω.2] @@ -1119,10 +713,6 @@ lemma hasCondDistrib_reward_hist_action_pullCount (fun ω ↦ (hist alg ω n, action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ((ν.prodMkRight _).prodMkLeft _) (arrayMeasure ν) := by - have h_meas : Measurable fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by - change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ - (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) - exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine condDistrib_prod_of_forall_condDistrib_cond (by fun_prop) (by fun_prop) (by fun_prop) _ ?_ intro (a, m) ham @@ -1133,27 +723,12 @@ lemma hasCondDistrib_reward_hist_action_pullCount refine (condDistrib_of_indepFun ?_ (by fun_prop) (by fun_prop)).trans (ae_of_all _ fun ω ↦ ?_) · exact (indepFun_snd_hist_cond alg ν a n m).symm · simp only [Kernel.const_apply] - have : (fun ω ↦ (action alg (n + 1) ω, - pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)} = - ({ω | action alg (n + 1) ω = a ∧ - pullCount (action alg) a (n + 1) ω = m}).indicator 1 ⁻¹' {1} := by - ext ω - simp [Set.indicator_apply] - grind - rw [this, cond_of_indepFun, map_snd_apply_arrayMeasure m a] + rw [preimage_action_pullCount_eq, cond_of_indepFun, map_snd_apply_arrayMeasure m a] · exact (indepFun_snd_apply_pullCount_action alg ν a m n).symm - · refine Measurable.indicator (by fun_prop) ?_ - exact MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop)) - ((measurableSet_singleton _).preimage (by fun_prop)) + · exact Measurable.indicator (by fun_prop) (measurableSet_action_eq_and_pullCount_eq alg a n m) · fun_prop · simp - · convert ham - ext ω - simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply, - Set.mem_singleton_iff, ite_eq_left_iff, not_and, zero_ne_one, imp_false, Classical.not_imp, - Decidable.not_not, Prod.mk.injEq, and_congr_right_iff] - intro ha - simp [ha] + · rwa [preimage_action_pullCount_eq] at ham /-- The reward at time `n + 1` is conditionally independent of the history up to time `n`, given the action at time `n + 1` and the number of times that action has been pulled before @@ -1174,48 +749,23 @@ and the action at time `n + 1`, is equal to the kernel `ν`. -/ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (reward alg (n + 1)) (fun ω ↦ (hist alg ω n, action alg (n + 1) ω)) (ν.prodMkLeft _) (arrayMeasure ν) := by - let R' := reward alg (n + 1) - let H := (hist alg · n) - let A := action alg (n + 1) - let P := fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω - have hP : Measurable P := measurable_pullCount_action_add_one alg n - change HasCondDistrib R' (fun ω ↦ (H ω, A ω)) (ν.prodMkLeft _) _ - suffices HasCondDistrib R' (fun ω ↦ (A ω, H ω)) (ν.prodMkRight _) (arrayMeasure ν) by - have h_eq : (fun ω ↦ (H ω, A ω)) = MeasurableEquiv.prodComm ∘ (fun ω ↦ (A ω, H ω)) := rfl - rw [h_eq] - exact this.measurableEquiv_comp_right (κ := ν.prodMkRight _) _ - suffices HasCondDistrib R' (fun ω ↦ ((A ω, H ω), P ω)) - ((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by - -- use that `P` is measurable wrt `(A, H)` to drop it from the conditioning - have hP_meas : - Measurable[MeasurableSpace.comap (fun ω ↦ (A ω, H ω)) inferInstance] P := - measurable_pullCount_action_add_one_hist alg n - obtain ⟨f, hf_meas, hf_eq⟩ := hP_meas.exists_eq_measurable_comp - simp only [hf_eq, Function.comp_apply] at this - rwa [hasCondDistrib_prod_right_iff _ _ hf_meas] at this - suffices HasCondDistrib R' (fun ω ↦ ((A ω, P ω), H ω)) - ((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by - let e : ((𝓐 × ℕ) × (Iic n → 𝓐 × R)) ≃ᵐ ((𝓐 × (Iic n → 𝓐 × R)) × ℕ) := - { toFun := fun x ↦ ((x.1.1, x.2), x.1.2) - invFun := fun x ↦ ((x.1.1, x.2), x.1.2) - measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop - measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop } - exact this.measurableEquiv_comp_right e - suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by - have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' := - (condIndepFun_reward_hist alg ν n).symm - have h_condDistrib := this.condDistrib_eq - rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) (by fun_prop) - (by fun_prop)] at h_indep - refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ - refine h_indep.trans ?_ - rw [Filter.EventuallyEq, ae_map_iff] at h_condDistrib ⊢ - · simpa only [Kernel.prodMkRight_apply] - · fun_prop - · exact Kernel.measurableSet_eq _ _ - · fun_prop - · exact Kernel.measurableSet_eq _ _ - exact hasCondDistrib_reward_pullCount_action alg ν n + have h := (hasCondDistrib_reward_hist_action_pullCount alg ν n).measurableEquiv_comp_right + MeasurableEquiv.prodAssoc.symm + obtain ⟨f, hf, hf_eq⟩ := + (measurable_pullCount_action_add_one_hist alg n).exists_eq_measurable_comp + have h_eq : (MeasurableEquiv.prodAssoc.symm ∘ fun ω ↦ (hist alg ω n, action alg (n + 1) ω, + pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) = + fun ω ↦ ((hist alg ω n, action alg (n + 1) ω), + f (hist alg ω n, action alg (n + 1) ω)) := by + funext ω + exact Prod.ext rfl (congrFun hf_eq ω) + have h_ker : ((ν.prodMkRight ℕ).prodMkLeft (Iic n → 𝓐 × R)).comap + MeasurableEquiv.prodAssoc.symm.symm MeasurableEquiv.prodAssoc.symm.symm.measurable = + (ν.prodMkLeft _).prodMkRight ℕ := by + ext p : 1 + rfl + rw [h_eq, h_ker] at h + exact (hasCondDistrib_prod_right_iff _ _ hf).1 h lemma hasCondDistrib_action (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (action alg (n + 1)) From a6f88e9259bb8675f573d088410a51be07531541 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 3 Sep 2026 14:45:35 +0200 Subject: [PATCH 2/2] notation for reward space --- .../Online/Bandit/ArrayProbSpace.lean | 225 +++++++++--------- 1 file changed, 111 insertions(+), 114 deletions(-) diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 3506fd35..243bc6d6 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -28,9 +28,9 @@ arms and rewards specified in the bandit model determine their laws uniquely. * `streamMeasure ν`: probability measure on the space of infinite arrays of rewards, where the rewards in each row are i.i.d. according to `ν`. -* `probSpace 𝓐 R`: probability space for the array model of stochastic bandits with action space `𝓐` - and reward space `R`. -* `arrayMeasure ν`: probability measure on `probSpace 𝓐 R` for the array model of stochastic bandits +* `probSpace 𝓐 𝓡`: probability space for the array model of stochastic bandits with action space `𝓐` + and reward space `𝓡`. +* `arrayMeasure ν`: probability measure on `probSpace 𝓐 𝓡` for the array model of stochastic bandits with reward kernel `ν`. -/ @@ -43,31 +43,31 @@ open scoped ENNReal NNReal namespace Bandits -variable {𝓐 R : Type*} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} +variable {𝓐 𝓡 : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} section MeasureSpace /-- Measure of an infinite stream of rewards from each action. -/ noncomputable -def streamMeasure (ν : Kernel 𝓐 R) : Measure (ℕ → 𝓐 → R) := +def streamMeasure (ν : Kernel 𝓐 𝓡) : Measure (ℕ → 𝓐 → 𝓡) := Measure.infinitePi fun _ ↦ Measure.infinitePi ν -instance (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : IsProbabilityMeasure (streamMeasure ν) := by +instance (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : IsProbabilityMeasure (streamMeasure ν) := by unfold streamMeasure infer_instance section StreamMeasure -lemma hasLaw_eval_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : - HasLaw (fun h : ℕ → 𝓐 → R ↦ h n) (Measure.infinitePi ν) (streamMeasure ν) := +lemma hasLaw_eval_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : + HasLaw (fun h : ℕ → 𝓐 → 𝓡 ↦ h n) (Measure.infinitePi ν) (streamMeasure ν) := hasLaw_eval_infinitePi (fun _ ↦ Measure.infinitePi ν) n -lemma hasLaw_eval_eval_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : - HasLaw (fun h : ℕ → 𝓐 → R ↦ h n a) (ν a) (streamMeasure ν) := +lemma hasLaw_eval_eval_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : + HasLaw (fun h : ℕ → 𝓐 → 𝓡 ↦ h n a) (ν a) (streamMeasure ν) := (hasLaw_eval_infinitePi ν a).comp (hasLaw_eval_streamMeasure ν n) -lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : - IdentDistrib (fun h : ℕ → 𝓐 → R ↦ h n a) id (streamMeasure ν) (ν a) where +lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : + IdentDistrib (fun h : ℕ → 𝓐 → 𝓡 ↦ h n a) id (streamMeasure ν) (ν a) where aemeasurable_fst := Measurable.aemeasurable (by fun_prop) aemeasurable_snd := Measurable.aemeasurable (by fun_prop) map_eq := by @@ -84,26 +84,26 @@ lemma integral_eval_streamMeasure (ν : Kernel 𝓐 ℝ) [IsMarkovKernel ν] (n ∫ h, h n a ∂(streamMeasure ν) = (ν a)[id] := by simpa using (hasLaw_eval_eval_streamMeasure ν n a).integral_eq -lemma iIndepFun_eval_streamMeasure' (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma iIndepFun_eval_streamMeasure' (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : iIndepFun (fun n ω ↦ ω n) (streamMeasure ν) := iIndepFun_infinitePi fun _ ↦ measurable_id -lemma iIndepFun_eval_streamMeasure'' (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) : +lemma iIndepFun_eval_streamMeasure'' (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (a : 𝓐) : iIndepFun (fun n ω ↦ ω n a) (streamMeasure ν) := (iIndepFun_eval_streamMeasure' ν).comp (g := fun i ω ↦ ω a) (by fun_prop) -lemma iIndepFun_eval_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma iIndepFun_eval_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : iIndepFun (fun (p : ℕ × 𝓐) ω ↦ ω p.1 p.2) (streamMeasure ν) := iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (fun _ ↦ ν) (by fun_prop) -lemma indepFun_eval_streamMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] {n m : ℕ} {a b : 𝓐} +lemma indepFun_eval_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] {n m : ℕ} {a b : 𝓐} (h : n ≠ m ∨ a ≠ b) : IndepFun (fun ω ↦ ω n a) (fun ω ↦ ω m b) (streamMeasure ν) := by change IndepFun (fun ω ↦ ω (n, a).1 (n, a).2) (fun ω ↦ ω (m, b).1 (m, b).2) (streamMeasure ν) exact (iIndepFun_eval_streamMeasure ν).indepFun (by grind) -lemma indepFun_eval_streamMeasure' (ν : Kernel 𝓐 R) [IsMarkovKernel ν] {a b : 𝓐} (h : a ≠ b) : +lemma indepFun_eval_streamMeasure' (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] {a b : 𝓐} (h : a ≠ b) : IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (streamMeasure ν) := indepFun_proj_infinitePi_infinitePi h @@ -115,27 +115,27 @@ open unitInterval section ProbabilitySpace -variable (𝓐 R) in +variable (𝓐 𝓡) in /-- Probability space for the array model of stochastic bandits. -/ -abbrev probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → R) +abbrev probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → 𝓡) /-- Probability measure for the array model of stochastic bandits. -/ noncomputable -def arrayMeasure (ν : Kernel 𝓐 R) : Measure (probSpace 𝓐 R) := +def arrayMeasure (ν : Kernel 𝓐 𝓡) : Measure (probSpace 𝓐 𝓡) := (Measure.infinitePi fun _ ↦ volume).prod (streamMeasure ν) -instance (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : IsProbabilityMeasure (arrayMeasure ν) := +instance (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : IsProbabilityMeasure (arrayMeasure ν) := Measure.prod.instIsProbabilityMeasure _ _ -lemma hasLaw_fst_apply_arrayMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : - HasLaw (fun ω : probSpace 𝓐 R ↦ ω.1 n) volume (arrayMeasure ν) := +lemma hasLaw_fst_apply_arrayMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : + HasLaw (fun ω : probSpace 𝓐 𝓡 ↦ ω.1 n) volume (arrayMeasure ν) := (hasLaw_eval_infinitePi (fun _ ↦ volume) n).comp (hasLaw_fst_prod _ _) -lemma hasLaw_snd_apply_arrayMeasure (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : - HasLaw (fun ω : probSpace 𝓐 R ↦ ω.2 n a) (ν a) (arrayMeasure ν) := +lemma hasLaw_snd_apply_arrayMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : + HasLaw (fun ω : probSpace 𝓐 𝓡 ↦ ω.2 n a) (ν a) (arrayMeasure ν) := (hasLaw_eval_eval_streamMeasure ν n a).comp (hasLaw_snd_prod _ _) -lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 R} [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : +lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 𝓡} [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : (arrayMeasure ν).map (fun ω ↦ ω.2 n a) = ν a := (hasLaw_snd_apply_arrayMeasure ν n a).map_eq @@ -143,12 +143,12 @@ lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 R} [IsMarkovKernel ν] (n : in row `a` of the reward array, the entry at index `i` is kept if `i < m` and replaced by the entry at index `m + 1 + i` otherwise. The result does not depend on the coordinate `(m, a)` of the array. -/ -def truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 R) : probSpace 𝓐 R := +def truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 𝓡) : probSpace 𝓐 𝓡 := (ω.1, fun i b ↦ if b = a then ω.2 (if i < m then i else m + 1 + i) b else ω.2 i b) @[fun_prop] lemma measurable_truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) : - Measurable (truncRow a m : probSpace 𝓐 R → probSpace 𝓐 R) := by + Measurable (truncRow a m : probSpace 𝓐 𝓡 → probSpace 𝓐 𝓡) := by refine Measurable.prodMk measurable_fst (measurable_pi_lambda _ fun i ↦ measurable_pi_lambda _ fun b ↦ ?_) by_cases hb : b = a <;> simp only [hb, ↓reduceIte] <;> fun_prop @@ -157,27 +157,27 @@ variable [Nonempty 𝓐] [StandardBorelSpace 𝓐] /-- The initial action is the image of a uniform random variable by this function. -/ noncomputable -def initAlgFunction (alg : Algorithm 𝓐 R) : I → 𝓐 := +def initAlgFunction (alg : Algorithm 𝓐 𝓡) : I → 𝓐 := (Measure.exists_measurable_map_eq alg.p0).choose -lemma initAlgFunction_map (alg : Algorithm 𝓐 R) : volume.map (initAlgFunction alg) = alg.p0 := +lemma initAlgFunction_map (alg : Algorithm 𝓐 𝓡) : volume.map (initAlgFunction alg) = alg.p0 := (Measure.exists_measurable_map_eq alg.p0).choose_spec.2 @[fun_prop] -lemma measurable_initAlgFunction (alg : Algorithm 𝓐 R) : +lemma measurable_initAlgFunction (alg : Algorithm 𝓐 𝓡) : Measurable (initAlgFunction alg) := (Measure.exists_measurable_map_eq alg.p0).choose_spec.1 /-- The next action is the image of the history and a uniform random variable by this function. -/ noncomputable -def algFunction (alg : Algorithm 𝓐 R) (n : ℕ) : - (Iic n → 𝓐 × R) → I → 𝓐 := +def algFunction (alg : Algorithm 𝓐 𝓡) (n : ℕ) : + (Iic n → 𝓐 × 𝓡) → I → 𝓐 := (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose -lemma algFunction_map (alg : Algorithm 𝓐 R) (n : ℕ) (h : Iic n → 𝓐 × R) : +lemma algFunction_map (alg : Algorithm 𝓐 𝓡) (n : ℕ) (h : Iic n → 𝓐 × 𝓡) : volume.map (algFunction alg n h) = alg.policy n h := (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose_spec.2 h @[fun_prop] -lemma measurable_algFunction (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_algFunction (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable (Function.uncurry (algFunction alg n)) := (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose_spec.1 @@ -189,25 +189,25 @@ section HistoryActionReward /-- History of actions and rewards up to time `n` in the array model. -/ noncomputable -def hist [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) : (n : ℕ) → Iic n → 𝓐 × R +def hist [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) : (n : ℕ) → Iic n → 𝓐 × 𝓡 | 0 => fun _ ↦ (initAlgFunction alg (ω.1 0), ω.2 0 (initAlgFunction alg (ω.1 0))) | n + 1 => - let hn : Iic n → 𝓐 × R := hist alg ω n + let hn : Iic n → 𝓐 × 𝓡 := hist alg ω n let a : 𝓐 := algFunction alg n hn (ω.1 (n + 1)) fun i ↦ if hin : i ≤ n then hn ⟨i, by simp [hin]⟩ else (a, ω.2 (pullCount' n hn a) a) @[simp] -lemma hist_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) : +lemma hist_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) : hist alg ω 0 = fun _ ↦ (initAlgFunction alg (ω.1 0), ω.2 0 (initAlgFunction alg (ω.1 0))) := rfl -lemma hist_add_one [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) (n : ℕ) : +lemma hist_add_one [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : let a : 𝓐 := algFunction alg n (hist alg ω n) (ω.1 (n + 1)) hist alg ω (n + 1) = fun (i : Iic (n + 1)) ↦ if hin : i ≤ n then hist alg ω n ⟨i, by simp [hin]⟩ else (a, ω.2 (pullCount' n (hist alg ω n) a) a) := rfl -lemma hist_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) (n : ℕ) : +lemma hist_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω n = fun i : Iic n ↦ hist alg ω i ⟨i.1, by simp⟩ := by induction n with | zero => @@ -224,11 +224,11 @@ lemma hist_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R simp_rw [hn] · grind -lemma hist_add_one_eq_IicSuccProd' [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) +lemma hist_add_one_eq_IicSuccProd' [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : let a : 𝓐 := algFunction alg n (hist alg ω n) (ω.1 (n + 1)) hist alg ω (n + 1) = - (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × R) n).symm + (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓡) n).symm (hist alg ω n, (a, ω.2 (pullCount' n (hist alg ω n) a) a)) := by intro a rw [hist_add_one] @@ -241,15 +241,15 @@ lemma hist_add_one_eq_IicSuccProd' [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) ( /-- Action taken at time `n` in the array model. -/ noncomputable -def action [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) (ω : probSpace 𝓐 R) : 𝓐 := +def action [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) (ω : probSpace 𝓐 𝓡) : 𝓐 := (hist alg ω n ⟨n, by simp⟩).1 -lemma action_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) : +lemma action_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) : action alg 0 = fun ω ↦ initAlgFunction alg (ω.1 0) := by ext simp [action, hist_zero] -lemma action_add_one_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma action_add_one_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : action alg (n + 1) = fun ω ↦ algFunction alg n (hist alg ω n) (ω.1 (n + 1)) := by ext ω rw [action, hist_add_one] @@ -257,21 +257,21 @@ lemma action_add_one_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : /-- Reward received at time `n` in the array model. -/ noncomputable -def reward [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) (ω : probSpace 𝓐 R) : R := +def reward [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) (ω : probSpace 𝓐 𝓡) : 𝓡 := (hist alg ω n ⟨n, by simp⟩).2 -lemma reward_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) : +lemma reward_zero [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) : reward alg 0 = fun ω ↦ ω.2 0 (action alg 0 ω) := by ext simp [reward, hist_zero, action_zero] -lemma reward_add_one [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma reward_add_one [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : reward alg (n + 1) = fun ω ↦ ω.2 (pullCount' n (hist alg ω n) (action alg (n + 1) ω)) (action alg (n + 1) ω) := by ext ω simp [reward, hist_add_one, action_add_one_eq] -lemma reward_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma reward_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : reward alg n = fun ω ↦ ω.2 (pullCount (action alg) (action alg n ω) n ω) (action alg n ω) := by cases n with | zero => ext; simp [reward_zero, action_zero] @@ -296,11 +296,11 @@ lemma sumRewards_eq [DecidableEq 𝓐] (alg : Algorithm 𝓐 ℝ) (a : 𝓐) (n section Measurability -lemma measurable_action_add_one' [DecidableEq 𝓐] {alg : Algorithm 𝓐 R} +lemma measurable_action_add_one' [DecidableEq 𝓐] {alg : Algorithm 𝓐 𝓡} (n : ℕ) (h : Measurable (hist alg · n)) : Measurable (fun x ↦ algFunction alg n (hist alg x n) (x.1 (n + 1))) := by fun_prop -lemma measurable_pullCount'_action_add_one [DecidableEq 𝓐] {alg : Algorithm 𝓐 R} +lemma measurable_pullCount'_action_add_one [DecidableEq 𝓐] {alg : Algorithm 𝓐 𝓡} (n : ℕ) (h_hist : Measurable (hist alg · n)) : Measurable (fun x ↦ pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1)))) := by @@ -309,15 +309,15 @@ lemma measurable_pullCount'_action_add_one [DecidableEq 𝓐] {alg : Algorithm exact (measurable_uncurry_pullCount' (𝓐 := 𝓐) n).comp (h_hist.prodMk h_alg_meas) @[fun_prop] -lemma measurable_hist [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_hist [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable (fun ω ↦ hist alg ω n) := by induction n with | zero => simp_rw [hist_zero, measurable_pi_iff] refine fun _ ↦ Measurable.prodMk (by fun_prop) ?_ - change Measurable ((fun x : 𝓐 × ((ℕ → I) × (ℕ → 𝓐 → R)) ↦ x.2.2 0 x.1) ∘ - (fun x : (ℕ → I) × (ℕ → 𝓐 → R) ↦ (initAlgFunction alg (x.1 0), x))) - have : Measurable (fun x : 𝓐 × ((ℕ → I) × (ℕ → 𝓐 → R)) ↦ x.2.2 0 x.1) := + change Measurable ((fun x : 𝓐 × ((ℕ → I) × (ℕ → 𝓐 → 𝓡)) ↦ x.2.2 0 x.1) ∘ + (fun x : (ℕ → I) × (ℕ → 𝓐 → 𝓡) ↦ (initAlgFunction alg (x.1 0), x))) + have : Measurable (fun x : 𝓐 × ((ℕ → I) × (ℕ → 𝓐 → 𝓡)) ↦ x.2.2 0 x.1) := measurable_from_prod_countable_right fun p ↦ by simp only; fun_prop exact Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) (by fun_prop)) | succ n hn => @@ -328,36 +328,36 @@ lemma measurable_hist [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 exact hn ⟨i.1, by simp [hin]⟩ · simp only [hist, hin, ↓reduceDIte] refine Measurable.prodMk (by fun_prop) ?_ - change Measurable ((fun (x : (ℕ → 𝓐 → R) × ℕ × 𝓐) ↦ x.1 x.2.1 x.2.2) ∘ + change Measurable ((fun (x : (ℕ → 𝓐 → 𝓡) × ℕ × 𝓐) ↦ x.1 x.2.1 x.2.2) ∘ (fun x ↦ (x.2, pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1))), (algFunction alg n (hist alg x n) (x.1 (n + 1)))))) - have h1 : Measurable (fun (x : (ℕ → 𝓐 → R) × ℕ × 𝓐) ↦ x.1 x.2.1 x.2.2) := + have h1 : Measurable (fun (x : (ℕ → 𝓐 → 𝓡) × ℕ × 𝓐) ↦ x.1 x.2.1 x.2.2) := measurable_from_prod_countable_left fun p : ℕ × 𝓐 ↦ (by simp only; fun_prop) refine Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) ?_) refine Measurable.prodMk ?_ (by fun_prop) exact measurable_pullCount'_action_add_one n hn @[fun_prop] -lemma measurable_action [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_action [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable (action alg n) := by unfold action; fun_prop @[fun_prop] -lemma measurable_reward [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_reward [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable (reward alg n) := by unfold reward; fun_prop -lemma hist_add_one_eq_IicSuccProd [DecidableEq 𝓐] (alg : Algorithm 𝓐 R) (ω : probSpace 𝓐 R) +lemma hist_add_one_eq_IicSuccProd [DecidableEq 𝓐] (alg : Algorithm 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) = - (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × R) n).symm + (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓡) n).symm (hist alg ω n, (action alg (n + 1) ω, reward alg (n + 1) ω)) := by rw [hist_add_one_eq_IicSuccProd', reward_add_one, action_add_one_eq] @[fun_prop] -lemma measurable_pullCount_action_add_one [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 R) +lemma measurable_pullCount_action_add_one [DecidableEq 𝓐] [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by - change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ - (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) + change Measurable ((fun p : (probSpace 𝓐 𝓡) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ + (fun ω : probSpace 𝓐 𝓡 ↦ (ω, action alg (n + 1) ω))) exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) end Measurability @@ -369,7 +369,7 @@ variable [DecidableEq 𝓐] section Congruence -- very useful to prove measurability -lemma hist_congr (alg : Algorithm 𝓐 R) (n : ℕ) {ω ω' : probSpace 𝓐 R} +lemma hist_congr (alg : Algorithm 𝓐 𝓡) (n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ i ≤ n, ω.1 i = ω'.1 i) (hω2 : ∀ i a, i < pullCount (action alg) a (n + 1) ω → ω.2 i a = ω'.2 i a) : hist alg ω n = hist alg ω' n := by @@ -402,8 +402,8 @@ lemma hist_congr (alg : Algorithm 𝓐 R) (n : ℕ) {ω ω' : probSpace 𝓐 R} pullCount' n (fun i ↦ (action alg i ω, reward alg i ω)) (action alg (n + 1) ω') + 1 grind -lemma action_eq_and_pullCount_eq_congr_aux (alg : Algorithm 𝓐 R) - (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 R} +lemma action_eq_and_pullCount_eq_congr_aux (alg : Algorithm 𝓐 𝓡) + (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) (h_eq : action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m) : @@ -428,8 +428,8 @@ lemma action_eq_and_pullCount_eq_congr_aux (alg : Algorithm 𝓐 R) simp only at h_hist rw [h_hist] -lemma action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) - {ω ω' : probSpace 𝓐 R} +lemma action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (m n : ℕ) + {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) : (action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m) ↔ @@ -437,8 +437,8 @@ lemma action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n ⟨action_eq_and_pullCount_eq_congr_aux alg a m n hω1 hω2_ne hω2_eq, action_eq_and_pullCount_eq_congr_aux alg a m n (by grind) (by grind) (by grind)⟩ -lemma indicator_action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ) - {ω ω' : probSpace 𝓐 R} +lemma indicator_action_eq_and_pullCount_eq_congr (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (m n : ℕ) + {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ i, ω.1 i = ω'.1 i) (hω2_ne : ∀ i b, b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ i, i + 1 ≤ m → ω.2 i a = ω'.2 i a) : {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator (fun _ ↦ 1) @@ -452,7 +452,7 @@ end Congruence section MeasurabilityAdvanced -lemma measurable_hist_comap [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_hist_comap [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable[MeasurableSpace.comap (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) inferInstance] (hist alg · n) := by have h_eq : (hist alg · n) = @@ -465,7 +465,7 @@ lemma measurable_hist_comap [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) refine Measurable.prodMk ?_ (by fun_prop) rw [measurable_pi_iff] intro i - change Measurable ((fun p ↦ p ⟨min i n, by simp⟩) ∘ (fun x : (Iic n → I) × (ℕ → 𝓐 → R) ↦ x.1)) + change Measurable ((fun p ↦ p ⟨min i n, by simp⟩) ∘ (fun x : (Iic n → I) × (ℕ → 𝓐 → 𝓡) ↦ x.1)) exact Measurable.comp (by fun_prop) measurable_fst /-- `truncRow` at the number of pulls of `a` up to time `n`: the rewards of action `a` that have @@ -473,11 +473,11 @@ not been observed by time `n` are replaced. The history up to time `n` is measur to this function (see `measurable_hist_truncRowPullCount`), and on the event `pullCount (action alg) a (n + 1) = m` it coincides with `truncRow a m`. -/ noncomputable -def truncRowPullCount (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 R) : - probSpace 𝓐 R := +def truncRowPullCount (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 𝓡) : + probSpace 𝓐 𝓡 := truncRow a (pullCount (action alg) a (n + 1) ω) ω -lemma measurable_hist_truncRowPullCount [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) (n : ℕ) : +lemma measurable_hist_truncRowPullCount [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (n : ℕ) : Measurable[MeasurableSpace.comap (truncRowPullCount alg a n) inferInstance] (hist alg · n) := by have h_eq : (hist alg · n) = (hist alg · n) ∘ (truncRowPullCount alg a n) := by ext ω : 1 @@ -489,13 +489,13 @@ lemma measurable_hist_truncRowPullCount [Countable 𝓐] (alg : Algorithm 𝓐 R rw [h_eq] exact (measurable_hist alg n).comp (Measurable.of_comap_le le_rfl) -lemma measurableSet_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 R) (a : 𝓐) +lemma measurableSet_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : MeasurableSet {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m} := MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop)) ((measurableSet_singleton _).preimage (by fun_prop)) -lemma preimage_action_pullCount_eq (alg : Algorithm 𝓐 R) (a : 𝓐) (n m : ℕ) : +lemma preimage_action_pullCount_eq (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : (fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)} = {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator @@ -507,7 +507,7 @@ lemma preimage_action_pullCount_eq (alg : Algorithm 𝓐 R) (a : 𝓐) (n m : intro ha simp [ha] -lemma measurable_indicator_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 R) +lemma measurable_indicator_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) (a : 𝓐) (m n : ℕ) : Measurable[MeasurableSpace.comap (truncRow a m) inferInstance] (({ω | action alg (n + 1) ω = a ∧ @@ -523,7 +523,7 @@ lemma measurable_indicator_action_eq_and_pullCount_eq [Countable 𝓐] (alg : Al exact (Measurable.indicator (by fun_prop) (measurableSet_action_eq_and_pullCount_eq alg a n m)).comp (Measurable.of_comap_le le_rfl) -lemma measurable_pullCount_action_add_one_hist (alg : Algorithm 𝓐 R) (n : ℕ) : +lemma measurable_pullCount_action_add_one_hist (alg : Algorithm 𝓐 𝓡) (n : ℕ) : Measurable[MeasurableSpace.comap (fun ω ↦ (hist alg ω n, action alg (n + 1) ω)) inferInstance] (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by simp_rw [pullCount_eq_sum] @@ -535,7 +535,7 @@ lemma measurable_pullCount_action_add_one_hist (alg : Algorithm 𝓐 R) (n : ℕ unfold action refine Measurable.fst (mγ := inferInstance) ?_ have : (hist alg · i ⟨i, by grind⟩) = - (fun ω : (Iic n → 𝓐 × R) × 𝓐 ↦ ω.1 ⟨i, by grind⟩) ∘ + (fun ω : (Iic n → 𝓐 × 𝓡) × 𝓐 ↦ ω.1 ⟨i, by grind⟩) ∘ (fun ω ↦ (fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩, action alg (n + 1) ω)) := rfl rw [this] exact measurable_comp_comap _ (Measurable.prodMk (by fun_prop) (by fun_prop)) @@ -545,18 +545,18 @@ end MeasurabilityAdvanced section Independence omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in -lemma indepFun_fst_snd (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma indepFun_fst_snd (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : IndepFun Prod.fst Prod.snd (arrayMeasure ν) := indepFun_prod measurable_id measurable_id omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in -lemma indepFun_fst_zero_snd_zero_action (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) : +lemma indepFun_fst_zero_snd_zero_action (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (a : 𝓐) : IndepFun (fun ω ↦ ω.1 0) (fun ω ↦ ω.2 0 a) (arrayMeasure ν) := - indepFun_prod (X := fun ω : ℕ → I ↦ ω 0) (Y := fun ω : ℕ → 𝓐 → R ↦ ω 0 a) + indepFun_prod (X := fun ω : ℕ → I ↦ ω 0) (Y := fun ω : ℕ → 𝓐 → 𝓡 ↦ ω 0 a) (by fun_prop) (by fun_prop) omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] in -lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : (fun ω ↦ ω.1 (n + 1)) ⟂ᵢ[arrayMeasure ν] (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by have h : IndepFun (fun ω : ℕ → I ↦ ω (n + 1)) (fun ω (i : Iic n) ↦ ω i) (Measure.infinitePi fun _ ↦ volume) := by @@ -566,21 +566,21 @@ lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ exact iSup_le fun i ↦ le_iSup₂_of_le (i : ℕ) (Set.mem_Iic.2 (Finset.mem_Iic.1 i.2)) le_rfl exact h.fst_prod (ν := streamMeasure ν) (by fun_prop) (by fun_prop) -variable [StandardBorelSpace R] [Nonempty R] +variable [StandardBorelSpace 𝓡] [Nonempty 𝓡] -lemma indepFun_fst_add_one_hist [Countable 𝓐] (alg : Algorithm 𝓐 R) - (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma indepFun_fst_add_one_hist [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) + (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : IndepFun (fun ω ↦ ω.1 (n + 1)) (hist alg · n) (arrayMeasure ν) := (indepFun_fst_add_one_aux ν n).of_measurable_right (measurable_hist_comap alg n) -omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [StandardBorelSpace R] [Nonempty R] in +omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] in /-- The reward `ω.2 m a` is independent of `truncRow a m`, which reads only other coordinates. -/ -lemma indepFun_snd_apply_truncRow (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (m : ℕ) : +lemma indepFun_snd_apply_truncRow (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (a : 𝓐) (m : ℕ) : (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν] (truncRow a m) := by - let T : (ℕ → 𝓐 → R) → (ℕ → 𝓐 → R) := + let T : (ℕ → 𝓐 → 𝓡) → (ℕ → 𝓐 → 𝓡) := fun ω k b ↦ if b = a then ω (if k < m then k else m + 1 + k) b else ω k b have hT : Measurable[⨆ p ∈ {p : ℕ × 𝓐 | p ≠ (m, a)}, - MeasurableSpace.comap (fun ω : ℕ → 𝓐 → R ↦ ω p.1 p.2) inferInstance] T := by + MeasurableSpace.comap (fun ω : ℕ → 𝓐 → 𝓡 ↦ ω p.1 p.2) inferInstance] T := by rw [measurable_iff_comap_le, MeasurableSpace.comap_pi] refine iSup_le fun k ↦ ?_ rw [MeasurableSpace.comap_pi] @@ -598,17 +598,17 @@ lemma indepFun_snd_apply_truncRow (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : (fun _ ↦ by fun_prop) (i := (m, a)) (by simp) hT exact h.snd_prod (μ := Measure.infinitePi fun _ ↦ volume) (by fun_prop) hTm -omit [StandardBorelSpace R] [Nonempty R] in -lemma indepFun_snd_apply_pullCount_action [Countable 𝓐] (alg : Algorithm 𝓐 R) - (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (m n : ℕ) : +omit [StandardBorelSpace 𝓡] [Nonempty 𝓡] in +lemma indepFun_snd_apply_pullCount_action [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) + (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (a : 𝓐) (m n : ℕ) : (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν] ({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1) := (indepFun_snd_apply_truncRow ν a m).of_measurable_right (measurable_indicator_action_eq_and_pullCount_eq alg a m n) -lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 R) - (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐) (n m : ℕ) : +lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 𝓡) + (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (a : 𝓐) (n m : ℕ) : (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]] (hist alg · n) := by @@ -634,18 +634,15 @@ end Independence section Laws -variable [Countable 𝓐] - -omit [Countable 𝓐] in -lemma hasLaw_action_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma hasLaw_action_zero (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : HasLaw (action alg 0) alg.p0 (arrayMeasure ν) := by rw [action_zero] exact (⟨(measurable_initAlgFunction alg).aemeasurable, initAlgFunction_map alg⟩ : HasLaw (initAlgFunction alg) alg.p0 volume).comp (hasLaw_fst_apply_arrayMeasure ν 0) -variable [StandardBorelSpace R] [Nonempty R] +variable [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] -lemma hasCondDistrib_reward_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma hasCondDistrib_reward_zero (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) := by refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine (condDistrib_ae_eq_cond (by fun_prop) (by fun_prop)).trans ?_ @@ -671,7 +668,7 @@ lemma hasCondDistrib_reward_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [ · simp · rwa [Measure.map_apply (by fun_prop) (by simp)] at ha -lemma hasCondDistrib_action' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma hasCondDistrib_action' (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (action alg (n + 1)) (hist alg · n) (alg.policy n) (arrayMeasure ν) := by have hU : HasCondDistrib (fun ω ↦ ω.1 (n + 1)) (fun ω ↦ (hist alg ω n, hist alg ω n)) (Kernel.const _ volume) (arrayMeasure ν) := @@ -691,8 +688,8 @@ lemma hasCondDistrib_action' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa rw [action_add_one_eq, h_ker] exact h -omit [StandardBorelSpace R] [Nonempty R] in -lemma reward_ae_eq_cond (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) (a : 𝓐) (n m : ℕ) : +omit [StandardBorelSpace 𝓡] [Nonempty 𝓡] in +lemma reward_ae_eq_cond (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : reward alg (n + 1) =ᵐ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]] (fun ω ↦ ω.2 m a) := by @@ -708,7 +705,7 @@ lemma reward_ae_eq_cond (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) (a : 𝓐) the action at time `n + 1`, and the number of times that action has been pulled before time `n + 1`, is equal to the kernel `ν`. -/ lemma hasCondDistrib_reward_hist_action_pullCount - (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : + (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (reward alg (n + 1)) (fun ω ↦ (hist alg ω n, action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) @@ -716,7 +713,7 @@ lemma hasCondDistrib_reward_hist_action_pullCount refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine condDistrib_prod_of_forall_condDistrib_cond (by fun_prop) (by fun_prop) (by fun_prop) _ ?_ intro (a, m) ham - have h_eq : ((ν.prodMkRight _).prodMkLeft _).comap (fun ω : (Iic n → 𝓐 × R) ↦ (ω, a, m)) + have h_eq : ((ν.prodMkRight _).prodMkLeft _).comap (fun ω : (Iic n → 𝓐 × 𝓡) ↦ (ω, a, m)) (by fun_prop) = Kernel.const _ (ν a) := by ext; simp rw [h_eq, condDistrib_congr_left (reward_ae_eq_cond alg ν a n m)] @@ -733,7 +730,7 @@ lemma hasCondDistrib_reward_hist_action_pullCount /-- The reward at time `n + 1` is conditionally independent of the history up to time `n`, given the action at time `n + 1` and the number of times that action has been pulled before time `n + 1`. -/ -lemma condIndepFun_reward_hist (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma condIndepFun_reward_hist (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : (reward alg (n + 1)) ⟂ᵢ[(fun ω ↦ (action alg (n + 1) ω, pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)), Measurable.prodMk (by fun_prop) (measurable_pullCount_action_add_one alg n); @@ -746,7 +743,7 @@ lemma condIndepFun_reward_hist (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [Is /-- The conditional distribution of the reward at time `n + 1`, given the history up to time `n` and the action at time `n + 1`, is equal to the kernel `ν`. -/ -lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (reward alg (n + 1)) (fun ω ↦ (hist alg ω n, action alg (n + 1) ω)) (ν.prodMkLeft _) (arrayMeasure ν) := by have h := (hasCondDistrib_reward_hist_action_pullCount alg ν n).measurableEquiv_comp_right @@ -759,7 +756,7 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa f (hist alg ω n, action alg (n + 1) ω)) := by funext ω exact Prod.ext rfl (congrFun hf_eq ω) - have h_ker : ((ν.prodMkRight ℕ).prodMkLeft (Iic n → 𝓐 × R)).comap + have h_ker : ((ν.prodMkRight ℕ).prodMkLeft (Iic n → 𝓐 × 𝓡)).comap MeasurableEquiv.prodAssoc.symm.symm MeasurableEquiv.prodAssoc.symm.symm.measurable = (ν.prodMkLeft _).prodMkRight ℕ := by ext p : 1 @@ -767,7 +764,7 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa rw [h_eq, h_ker] at h exact (hasCondDistrib_prod_right_iff _ _ hf).1 h -lemma hasCondDistrib_action (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : +lemma hasCondDistrib_action (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (action alg (n + 1)) (fun ω (i : Iic n) ↦ (action alg i ω, reward alg i ω)) (alg.policy n) (arrayMeasure ν) := by @@ -777,7 +774,7 @@ lemma hasCondDistrib_action (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMar · simp only [reward] rw [hist_eq _ _ n] -lemma hasCondDistrib_reward (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] +lemma hasCondDistrib_reward (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (reward alg (n + 1)) (fun ω ↦ (fun (i : Iic n) ↦ (action alg i ω, reward alg i ω), action alg (n + 1) ω)) @@ -789,7 +786,7 @@ lemma hasCondDistrib_reward (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMar rw [hist_eq _ _ n] · rfl -lemma isAlgEnvSeq_arrayMeasure (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : +lemma isAlgEnvSeq_arrayMeasure (alg : Algorithm 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] : IsAlgEnvSeq (action alg) (reward alg) alg (stationaryEnv ν) (arrayMeasure ν) where hasLaw_action_zero := hasLaw_action_zero alg ν hasCondDistrib_feedback_zero := hasCondDistrib_reward_zero alg ν