From 71ac3847063510e95d53a2b33afec3838b3dd26f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 8 Sep 2025 14:57:06 +0200 Subject: [PATCH 01/20] progress on the law of Y --- LeanBandits/Bandit.lean | 8 ++- LeanBandits/ETC.lean | 14 ++-- LeanBandits/Regret.lean | 8 +++ LeanBandits/RewardByCountMeasure.lean | 75 ++++++++++++++++++++- blueprint/lean_decls | 6 +- blueprint/src/chapters/bandit.tex | 95 ++++++++++++++++++++++++--- blueprint/src/chapters/etc.tex | 2 +- 7 files changed, 185 insertions(+), 23 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index eb25efc4..f47e8fa4 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -130,7 +130,7 @@ lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := by unfold hist; fun_prop /-- Filtration of the bandit process. -/ -def ℱ (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] : +protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] : Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) := MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R) @@ -152,6 +152,12 @@ lemma condDistrib_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n := by sorry +lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : + HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) where + map_eq := by + sorry + end MeasureSpace end Bandits diff --git a/LeanBandits/ETC.lean b/LeanBandits/ETC.lean index b805f469..6af21402 100644 --- a/LeanBandits/ETC.lean +++ b/LeanBandits/ETC.lean @@ -43,14 +43,12 @@ def etcAlgorithm (hK : 0 < K) (m : ℕ) : Algorithm (Fin K) ℝ where p0 := Measure.dirac ⟨0, hK⟩ lemma ETC.arm_zero (hK : 0 < K) (m : ℕ) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] : - arm 0 =ᵐ[Bandit.trajMeasure (etcAlgorithm hK m) ν] fun h ↦ ⟨0, hK⟩ := by - suffices h : (Bandit.trajMeasure (etcAlgorithm hK m) ν).map (arm 0) = (etcAlgorithm hK m).p0 by - have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (etcAlgorithm hK m) ν).map (arm 0)), x = ⟨0, hK⟩ := by - rw [h] - simp [etcAlgorithm] - exact ae_of_ae_map (by fun_prop) h_eq - -- extract lemma - sorry + arm 0 =ᵐ[Bandit.trajMeasure (etcAlgorithm hK m) ν] fun _ ↦ ⟨0, hK⟩ := by + have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (etcAlgorithm hK m) ν).map (arm 0)), x = ⟨0, hK⟩ := by + have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK + rw [(hasLaw_arm_zero _ _).map_eq] + simp [etcAlgorithm] + exact ae_of_ae_map (by fun_prop) h_eq lemma ETC.arm_ae_eq_etcNextArm (hK : 0 < K) (m : ℕ) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (n : ℕ) : diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean index ecd03cb6..1af6f8b0 100644 --- a/LeanBandits/Regret.lean +++ b/LeanBandits/Regret.lean @@ -144,6 +144,14 @@ lemma rewardByCount_eq_ite (a : α) (m : ℕ) (h : ℕ → α × ℝ) (z : ℕ unfold rewardByCount cases stepsUntil (arm · h) a m <;> simp +lemma rewardByCount_of_stepsUntil_eq_top {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)} + (h : stepsUntil (arm · ω.1) a m = ⊤) : + rewardByCount a m ω.1 ω.2 = ω.2 m a := by simp [rewardByCount_eq_ite, h] + +lemma rewardByCount_of_stepsUntil_eq_coe {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)} + (h : stepsUntil (arm · ω.1) a m = n) : + rewardByCount a m ω.1 ω.2 = reward n ω.1 := by simp [rewardByCount_eq_ite, h] + lemma rewardByCount_pullCount_add_one_eq_reward (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : rewardByCount (arm t h) (pullCount (arm · h) (arm t h) t + 1) h z = reward t h := by rw [rewardByCount, ← pullCount_eq_pullCount_add_one, stepsUntil_pullCount_eq] diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 8f948cfa..c2b1fa26 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -54,6 +54,37 @@ lemma ProbabilityTheory.condDistrib_const [IsFiniteMeasure μ] filter_upwards [condDistrib_comp hX (by fun_prop : Measurable (fun _ ↦ c))] with b hb rw [hb] +lemma ProbabilityTheory.condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β] + [IsFiniteMeasure μ] + (hX : Measurable X) (hY : Measurable Y) : + condDistrib Y X μ =ᵐ[μ.map X] fun b ↦ (μ[|X ⁻¹' {b}]).map Y := by + rw [Filter.EventuallyEq, ae_iff_of_countable] + intro b hb + ext s hs + rw [condDistrib_apply_of_ne_zero hY, + Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs, + Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs), + cond_apply (hX (measurableSet_singleton _))] + · congr + · exact hb + +lemma ProbabilityTheory.ae_cond_of_forall_mem {μ : Measure α} {s : Set α} + (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : + ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ + +omit [StandardBorelSpace Ω] [Nonempty Ω] in +lemma ProbabilityTheory.cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) + (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) + (hμs : μ (X ⁻¹' s) ≠ 0) : + (μ[|X ⁻¹' s]).map Y = μ.map Y := by + ext t ht + rw [Measure.map_apply (by fun_prop) ht, Measure.map_apply (by fun_prop) ht, cond_apply (hX hs), + IndepSet.measure_inter_eq_mul, ← mul_assoc, ENNReal.inv_mul_cancel, one_mul] + · exact hμs + · simp + · rw [indepFun_iff_indepSet_preimage hX hY] at h + exact h s t hs ht + @[fun_prop] lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) : Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf @@ -126,16 +157,56 @@ lemma measurable_rewardByCount (a : α) (m : ℕ) : (measurable_stepsUntil' a m).toNat.prodMk (by fun_prop) exact Measurable.comp (by fun_prop) this +omit [DecidableEq α] [MeasurableSingletonClass α] in +lemma hasLaw_Z {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) : + HasLaw (fun ω ↦ ω.2 m a) (ν a) (Bandit.measure alg ν) where + map_eq := by + calc ((Bandit.trajMeasure alg ν).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.2 m a) + _ = (((Bandit.trajMeasure alg ν).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.2)).map + (fun ω ↦ ω m a) := by + rw [Measure.map_map (by fun_prop) (by fun_prop)] + rfl + _ = (Bandit.streamMeasure ν).map (fun ω ↦ ω m a) := by simp [Measure.map_snd_prod] + _ = ((Measure.infinitePi fun _ ↦ Measure.infinitePi ν).map (fun ω ↦ ω m)).map + (fun ω ↦ ω a) := by + rw [Bandit.streamMeasure, Measure.map_map (by fun_prop) (by fun_prop)] + rfl + _ = ν a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq] + lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace α] [Nonempty α] {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) (hm : m ≠ 0) : condDistrib (fun ω ↦ rewardByCount a m ω.1 ω.2) (fun ω ↦ stepsUntil (arm · ω.1) a m) (Bandit.measure alg ν) =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil (arm · ω.1) a m)] Kernel.const _ (ν a) := by - sorry + let μ := Bandit.measure alg ν + refine (condDistrib_ae_eq_cond (μ := μ) + (X := fun ω ↦ stepsUntil (arm · ω.1) a m) (by fun_prop) (by fun_prop)).trans ?_ + rw [Filter.EventuallyEq, ae_iff_of_countable] + intro n hn + simp only [Kernel.const_apply] + cases n with + | top => + rw [Measure.map_congr (g := fun ω ↦ ω.2 m a)] + swap + · refine ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_ + simp only [Set.mem_preimage, Set.mem_singleton_iff] + exact fun ω ↦ rewardByCount_of_stepsUntil_eq_top + rw [cond_of_indepFun _ (by fun_prop) (by fun_prop) (measurableSet_singleton _)] + · exact (hasLaw_Z a m).map_eq + · rwa [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hn + · exact indepFun_prod (X := fun ω : ℕ → α × ℝ ↦ stepsUntil (arm · ω) a m) + (Y := fun ω : ℕ → α → ℝ ↦ ω m a) (by fun_prop) (by fun_prop) + | coe n => + rw [Measure.map_congr (g := fun ω ↦ reward n ω.1)] + swap + · refine ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_ + simp only [Set.mem_preimage, Set.mem_singleton_iff] + exact fun ω ↦ rewardByCount_of_stepsUntil_eq_coe + sorry /-- The reward received at the `m`-th pull of arm `a` has law `ν a`. -/ lemma hasLaw_rewardByCount [StandardBorelSpace α] [Nonempty α] - {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) (hm : m ≠ 0): + {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) (hm : m ≠ 0) : HasLaw (fun ω ↦ rewardByCount a m ω.1 ω.2) (ν a) (Bandit.measure alg ν) where map_eq := by have h_condDistrib : diff --git a/blueprint/lean_decls b/blueprint/lean_decls index fc9eaeeb..bfc67f6c 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -3,17 +3,21 @@ Bandits.Bandit.measure Bandits.arm Bandits.reward Bandits.hist +Bandits.pullCount +Bandits.filtration Bandits.condDistrib_reward +Bandits.hasLaw_arm_zero Bandits.condDistrib_arm Bandits.stepsUntil Bandits.rewardByCount +Bandits.hasLaw_rewardByCount +Bandits.iIndepFun_rewardByCount Bandits.stepsUntil_pullCount_le Bandits.stepsUntil_pullCount_eq Bandits.rewardByCount_pullCount_add_one_eq_reward Bandits.sum_rewardByCount_eq_sum_reward Bandits.regret Bandits.gap -Bandits.pullCount Bandits.regret_eq_sum_pullCount_mul_gap ProbabilityTheory.HasSubgaussianMGF ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index ff2faeb7..2b8f7f5d 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -56,6 +56,14 @@ \section{Algorithm, bandit and probability space} \end{definition} +\begin{definition}[Pull counts]\label{def:pullCount} + \uses{def:armAndReward} + \leanok + \lean{Bandits.pullCount} +For an arm $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that arm $a$ has been pulled before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. +\end{definition} + + \begin{remark}[Building vs analyzing algorithms] When we describe an algorithm, we give the data of the policies $\pi_t$, which are functions of the partial history up to time $t$, in $(\mathcal{A} \times \mathcal{R})^{t+1}$. That means that any tool used to define a policy must be a function defined on $(\mathcal{A} \times \mathcal{R})^{t+1}$. @@ -68,6 +76,35 @@ \section{Algorithm, bandit and probability space} \end{remark} +\begin{definition}[Filtration]\label{def:banditFiltration} + \uses{def:armAndReward} + \leanok + \lean{Bandits.filtration} +The filtration $\mathcal{F}_B$ on $\Omega_B$ generated by the history of pulls and rewards is the increasing family of $\sigma$-algebras +$\mathcal{F}_{B,t} = \sigma(H_0, \ldots, H_t)$, for $t \in \mathbb{N}$. +\end{definition} + + +\begin{lemma}\label{lem:adapted_hist} + \uses{def:banditFiltration,def:armAndReward} +Seen as processes defined on $\Omega_B$, the processes $(H_t)_{t \in \mathbb{N}}$, $(A_t)_{t \in \mathbb{N}}$, and $(X_t)_{t \in \mathbb{N}}$ are adapted to the filtration $\mathcal{F}_B$. +\end{lemma} + +\begin{proof} + +\end{proof} + + +\begin{lemma}\label{lem:predictable_pullCount} + \uses{def:banditFiltration,def:pullCount} +Let $a \in \mathcal{A}$. Seen as a process defined on $\Omega_B$, $(N_{t,a})_{t \in \mathbb{N}}$ is predictable with respect to the filtration $\mathcal{F}_B$ (that is, $(N_{t,a})_{t \in \mathbb{N}}$ is adapted to $(\mathcal{F}_{B, t-1})_{t \in \mathbb{N}}$). +\end{lemma} + +\begin{proof} + +\end{proof} + + \begin{lemma}\label{lem:condDistrib_reward} \uses{def:Bandit.measure,def:armAndReward} \leanok @@ -82,6 +119,8 @@ \section{Algorithm, bandit and probability space} \begin{lemma}\label{lem:law_arm_zero} \uses{def:Bandit.measure,def:armAndReward} + \leanok + \lean{Bandits.hasLaw_arm_zero} The law of the arm $A_0$ in the bandit probability space $(\Omega, \mathbb{P})$ is $P_0$. \end{lemma} @@ -128,9 +167,53 @@ \section{Alternative model}\label{sec:alt_model} \end{definition} -\begin{lemma}\label{lem:iid_rewardByCount} +\begin{lemma}\label{lem:isStoppingTime_stepsUntil} + \uses{def:stepsUntil} +$T_{n,a}$ is a stopping time for the filtration generated by the history of pulls and rewards. +\end{lemma} + +\begin{proof} +It is the hitting time of a measurable set by the adapted process $(N_{n+1, a})_{n \in \mathbb{N}}$, hence a stopping time. +\end{proof} + + +\begin{lemma}\label{lem:hasLaw_rewardByCount} + \uses{def:rewardByCount} + \leanok + \lean{Bandits.hasLaw_rewardByCount} +For $n > 0$ and $a \in \mathcal{A}$, the law of $Y_{n,a}$ is $\nu(a)$. +\end{lemma} + +\begin{proof} +It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. +If $t = \infty$, then +\begin{align*} + \mathcal{L}(Y_{n,a} \mid T_{n,a} = t) + = \mathcal{L}(Z_{n,a} \mid T_{n,a} = t) + = \mathcal{L}(Z_{n,a}) + = \nu(a) +\end{align*} +If $t < \infty$, then +\begin{align*} + \mathcal{L}(Y_{n,a} \mid T_{n,a} = t) + &= \mathcal{L}(X_t \mid T_{n,a} = t) + \\ + &= \mathcal{L}(X_t \mid T_{n,a} = t, A_t = a) + \\ + &= \mathcal{L}(X_t \mid A_t = a) + \\ + &= \nu(a) + \: . +\end{align*} +TODO: explain that chain of equalities. There is independence involved. +\end{proof} + + +\begin{lemma}\label{lem:iIndepFun_rewardByCount} \uses{def:rewardByCount} -The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent and identically distributed random variables, with distribution $\nu(a)$. + \leanok + \lean{Bandits.iIndepFun_rewardByCount} +The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent. \end{lemma} \begin{proof} @@ -231,14 +314,6 @@ \section{Regret and other bandit quantities} \end{definition} -\begin{definition}\label{def:pullCount} - \uses{def:bandit} - \leanok - \lean{Bandits.pullCount} -For an arm $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that arm $a$ has been pulled before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. -\end{definition} - - \begin{lemma}\label{lem:regret_eq_sum_pullCount_mul_gap} \uses{def:regret,def:gap,def:pullCount} \leanok diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index 113bf6ed..e885c8cf 100644 --- a/blueprint/src/chapters/etc.tex +++ b/blueprint/src/chapters/etc.tex @@ -40,7 +40,7 @@ \section{Explore-Then-Commit} \end{lemma} \begin{proof} - \uses{lem:iid_rewardByCount, lem:independent_rewardByCount, lem:sum_rewardByCount, thm:hoeffding} + \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount, lem:independent_rewardByCount, lem:sum_rewardByCount, thm:hoeffding} \begin{align*} \mathbb{P}(\hat{A}_m^* = a) &\le \mathbb{P}(\hat{\mu}_a \ge \hat{\mu}_{a^*}) From 6939a8ac7c06c294388336c65f4828ddf2374031 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 8 Sep 2025 15:04:26 +0200 Subject: [PATCH 02/20] add uses --- blueprint/src/chapters/bandit.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 2b8f7f5d..41dab130 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -185,6 +185,7 @@ \section{Alternative model}\label{sec:alt_model} \end{lemma} \begin{proof} + \uses{lem:condDistrib_reward} It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. If $t = \infty$, then \begin{align*} @@ -296,7 +297,7 @@ \section{Regret and other bandit quantities} \begin{definition}[Regret]\label{def:regret} - \uses{def:armMean} + \uses{def:armMean, def:armAndReward} \leanok \lean{Bandits.regret} The regret $R_T$ of a sequence of arms $A_0, \ldots, A_{T-1}$ after $T$ pulls is the difference between the cumulative reward of always playing the best arm and the cumulative reward of the sequence: From f6ad60ff3e07484e237f178a72d657e697584097 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 8 Sep 2025 19:49:58 +0200 Subject: [PATCH 03/20] work --- LeanBandits/Regret.lean | 9 +++ LeanBandits/RewardByCountMeasure.lean | 104 ++++++++++++++++++++++++-- 2 files changed, 105 insertions(+), 8 deletions(-) diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean index 1af6f8b0..7df22ec9 100644 --- a/LeanBandits/Regret.lean +++ b/LeanBandits/Regret.lean @@ -130,6 +130,15 @@ lemma arm_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount (arm · h) a (s rwa [← pullCount_eq_pullCount] exact h_ne +lemma arm_eq_of_stepsUntil_eq_coe {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)} (hm : m ≠ 0) + (h : stepsUntil (arm · ω.1) a m = n) : + arm n ω.1 = a := by + have : n = (stepsUntil (fun x ↦ arm x ω.1) a m).toNat := by simp [h] + rw [this, arm_stepsUntil hm] + by_contra! h_contra + rw [← stepsUntil_eq_top_iff] at h_contra + simp [h_contra] at h + /-- Reward obtained when pulling arm `a` for the `m`-th time. -/ noncomputable def rewardByCount (a : α) (m : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : ℝ := diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index c2b1fa26..a1526f5d 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -72,6 +72,11 @@ lemma ProbabilityTheory.ae_cond_of_forall_mem {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ +lemma ProbabilityTheory.condDistrib_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) + (hX : Measurable X) (hY : Measurable Y) : + condDistrib Y X μ =ᵐ[μ.map X] fun _ ↦ μ.map Y := by + sorry + omit [StandardBorelSpace Ω] [Nonempty Ω] in lemma ProbabilityTheory.cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) @@ -85,6 +90,37 @@ lemma ProbabilityTheory.cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : In · rw [indepFun_iff_indepSet_preimage hX hY] at h exact h s t hs ht +lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} + [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] + (hG : G ≤ mα) : + CondIndep G F H hG μ + ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by + sorry + +lemma ProbabilityTheory.condDistrib_of_condIndepFun + [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] + (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) + (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : + condDistrib Y (fun ω ↦ (X ω, Z ω)) μ + =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] fun p ↦ condDistrib Y Z μ p.2 := by + sorry + +lemma ProbabilityTheory.cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] + (hZ : Measurable Z) + (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) + (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) {t : Set Ω'} + (ht : MeasurableSet t) (hμs : μ (Z ⁻¹' t) ≠ 0) : + (μ[|X ⁻¹' s ∩ Z ⁻¹' t]).map Y = (μ[|Z ⁻¹' t]).map Y := by + ext u hu + rw [Measure.map_apply (by fun_prop) hu, Measure.map_apply (by fun_prop) hu, cond_apply, + cond_apply] + rotate_left + · exact hZ ht + · exact (hX hs).inter (hZ ht) + rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hY hX] at h + specialize h u s hu hs + sorry + @[fun_prop] lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) : Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf @@ -157,8 +193,10 @@ lemma measurable_rewardByCount (a : α) (m : ℕ) : (measurable_stepsUntil' a m).toNat.prodMk (by fun_prop) exact Measurable.comp (by fun_prop) this +variable {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] + omit [DecidableEq α] [MeasurableSingletonClass α] in -lemma hasLaw_Z {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) : +lemma hasLaw_Z (a : α) (m : ℕ) : HasLaw (fun ω ↦ ω.2 m a) (ν a) (Bandit.measure alg ν) where map_eq := by calc ((Bandit.trajMeasure alg ν).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.2 m a) @@ -173,8 +211,55 @@ lemma hasLaw_Z {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] rfl _ = ν a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq] -lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace α] [Nonempty α] - {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) (hm : m ≠ 0) : +-- Notation for the law of a random variable conditioned on an event +notation "𝓛[" Y " | " s ";" μ "]" => Measure.map Y (μ[|s]) +notation "𝓛[" Y " | " X " in " s ";" μ "]" => Measure.map Y (μ[|X ⁻¹' s]) +notation "𝓛[" Y " | " X " ← " x ";" μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) + +lemma reward_cond_arm [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (n : ℕ) + (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : + 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by + let μ := Bandit.measure alg ν + have h_ra : (condDistrib (fun ω ↦ reward n ω.1) (fun ω ↦ arm n ω.1) μ) + =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν := by + have h_ra' := condDistrib_reward alg ν n + sorry + have h_eq := condDistrib_ae_eq_cond (μ := μ) + (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop) + rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq + specialize h_ra a hμa + specialize h_eq a hμa + rw [h_ra] at h_eq + exact h_eq.symm + +lemma reward_condIndepFun_stepsUntil_arm [StandardBorelSpace α] [Countable α] [Nonempty α] + (a : α) (m n : ℕ) : + CondIndepFun (MeasurableSpace.comap (fun ω ↦ arm n ω.1) inferInstance) + (Measurable.comap_le <| by fun_prop) (fun ω ↦ reward n ω.1) + (fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m) (Bandit.measure alg ν) := by + let μ := Bandit.measure alg ν + sorry + +lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ) + (hm : m ≠ 0) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : + 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m ← (n : ℕ∞); + Bandit.measure alg ν] = ν a := by + let μ := Bandit.measure alg ν + calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m ← (n : ℕ∞); μ] + _ = (μ[|(fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map + (fun ω ↦ reward n ω.1) := by + congr with ω + simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and] + exact arm_eq_of_stepsUntil_eq_coe hm + _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by + rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop) + (measurableSet_singleton _) (measurableSet_singleton _)] + · rwa [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hμa + · exact reward_condIndepFun_stepsUntil_arm a m n + _ = ν a := reward_cond_arm a n hμa + +lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α] + (a : α) (m : ℕ) (hm : m ≠ 0) : condDistrib (fun ω ↦ rewardByCount a m ω.1 ω.2) (fun ω ↦ stepsUntil (arm · ω.1) a m) (Bandit.measure alg ν) =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil (arm · ω.1) a m)] Kernel.const _ (ν a) := by @@ -202,11 +287,15 @@ lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace α] [Nonempty α] · refine ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_ simp only [Set.mem_preimage, Set.mem_singleton_iff] exact fun ω ↦ rewardByCount_of_stepsUntil_eq_coe - sorry + refine reward_cond_stepsUntil a m n hm ?_ + rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hn ⊢ + refine fun h_zero ↦ hn (measure_mono_null (fun ω ↦ ?_) h_zero) + simp only [Set.mem_preimage, Set.mem_singleton_iff] + exact arm_eq_of_stepsUntil_eq_coe hm /-- The reward received at the `m`-th pull of arm `a` has law `ν a`. -/ -lemma hasLaw_rewardByCount [StandardBorelSpace α] [Nonempty α] - {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (m : ℕ) (hm : m ≠ 0) : +lemma hasLaw_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] + (a : α) (m : ℕ) (hm : m ≠ 0) : HasLaw (fun ω ↦ rewardByCount a m ω.1 ω.2) (ν a) (Bandit.measure alg ν) where map_eq := by have h_condDistrib : @@ -228,8 +317,7 @@ lemma hasLaw_rewardByCount [StandardBorelSpace α] [Nonempty α] isProbabilityMeasure_map (by fun_prop) simp -lemma identDistrib_rewardByCount [StandardBorelSpace α] [Nonempty α] - {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] (a : α) (n m : ℕ) +lemma identDistrib_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] (a : α) (n m : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) : IdentDistrib (fun ω ↦ rewardByCount a n ω.1 ω.2) (fun ω ↦ rewardByCount a m ω.1 ω.2) (Bandit.measure alg ν) (Bandit.measure alg ν) where From 76d196acf6fd652b9bfc9a9330cadfc9cd855049 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 8 Sep 2025 19:52:55 +0200 Subject: [PATCH 04/20] more notation --- LeanBandits/RewardByCountMeasure.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index a1526f5d..42e1261f 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -212,9 +212,11 @@ lemma hasLaw_Z (a : α) (m : ℕ) : _ = ν a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq] -- Notation for the law of a random variable conditioned on an event -notation "𝓛[" Y " | " s ";" μ "]" => Measure.map Y (μ[|s]) -notation "𝓛[" Y " | " X " in " s ";" μ "]" => Measure.map Y (μ[|X ⁻¹' s]) -notation "𝓛[" Y " | " X " ← " x ";" μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) +notation "𝓛[" Y " | " s "; " μ "]" => Measure.map Y (μ[|s]) +notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s]) +notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) +notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ +notation "𝓛[" Y "; " μ "]" => Measure.map Y μ lemma reward_cond_arm [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (n : ℕ) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : From 8f1ff7a39b3ac8b8a2ddac461637a39a9f242c84 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 8 Sep 2025 19:57:22 +0200 Subject: [PATCH 05/20] docstrings --- LeanBandits/RewardByCountMeasure.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 42e1261f..14fbfead 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -211,11 +211,15 @@ lemma hasLaw_Z (a : α) (m : ℕ) : rfl _ = ν a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq] --- Notation for the law of a random variable conditioned on an event +/-- Law of `Y` conditioned on the event `s`.-/ notation "𝓛[" Y " | " s "; " μ "]" => Measure.map Y (μ[|s]) +/-- Law of `Y` conditioned on the event that `X` is in `s`. -/ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s]) +/-- Law of `Y` conditioned on the event that `X` equals `x`. -/ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) +/-- Law of `Y` conditioned on `X`. -/ notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ +/-- Law of `Y`. -/ notation "𝓛[" Y "; " μ "]" => Measure.map Y μ lemma reward_cond_arm [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (n : ℕ) From 76effbcccb92b449e61e72cdf1f3574a21731e7e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 08:38:23 +0200 Subject: [PATCH 06/20] create aux file --- LeanBandits.lean | 1 + LeanBandits/ForMathlib/CondDistrib.lean | 135 ++++++++++++++++++++++++ LeanBandits/RewardByCountMeasure.lean | 120 +-------------------- 3 files changed, 137 insertions(+), 119 deletions(-) create mode 100644 LeanBandits/ForMathlib/CondDistrib.lean diff --git a/LeanBandits.lean b/LeanBandits.lean index ab3c610e..c2443ec0 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -1,6 +1,7 @@ import LeanBandits.AlgorithmBuilding import LeanBandits.Bandit import LeanBandits.ETC +import LeanBandits.ForMathlib.CondDistrib import LeanBandits.Regret import LeanBandits.RewardByCountMeasure import LeanBandits.UCB diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean new file mode 100644 index 00000000..f49c2c3e --- /dev/null +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +import Mathlib.Probability.Independence.Basic +import Mathlib.Probability.Independence.Conditional +import Mathlib.Probability.Kernel.CompProdEqIff +import Mathlib.Probability.Kernel.Condexp + + +open MeasureTheory ProbabilityTheory Finset +open scoped ENNReal NNReal + +variable {α β γ Ω Ω' : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + {mα : MeasurableSpace α} {μ : Measure α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + [MeasurableSpace Ω'] [StandardBorelSpace Ω'] [Nonempty Ω'] + {X : α → β} {Y : α → Ω} {Z : α → Ω'} {T : α → γ} + +@[fun_prop] +lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) : + Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf + +@[fun_prop] +lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat) := + Measurable.comp (by fun_prop) hf + +namespace MeasureTheory.Measure + +lemma comp_congr {κ η : Kernel α β} (h : ∀ᵐ a ∂μ, κ a = η a) : + κ ∘ₘ μ = η ∘ₘ μ := + bind_congr_right h + +lemma copy_comp_map (hX : AEMeasurable X μ) : + Kernel.copy β ∘ₘ (μ.map X) = μ.map (fun a ↦ (X a, X a)) := by + rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] + congr + +lemma compProd_deterministic [SFinite μ] (hX : Measurable X) : + μ ⊗ₘ (Kernel.deterministic X hX) = μ.map (fun a ↦ (a, X a)) := by + rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic, + deterministic_comp_eq_map] + rfl + +end MeasureTheory.Measure + +namespace ProbabilityTheory + +lemma condDistrib_comp_map [IsFiniteMeasure μ] + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by + rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX] + +lemma condDistrib_comp [IsFiniteMeasure μ] + (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : + condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by + rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop), + Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] + congr + +lemma condDistrib_const [IsFiniteMeasure μ] + (hX : AEMeasurable X μ) (c : Ω) : + condDistrib (fun _ ↦ c) X μ =ᵐ[μ.map X] Kernel.deterministic (fun _ ↦ c) (by fun_prop) := by + have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl + conv_lhs => rw [this] + filter_upwards [condDistrib_comp hX (by fun_prop : Measurable (fun _ ↦ c))] with b hb + rw [hb] + +lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β] + [IsFiniteMeasure μ] + (hX : Measurable X) (hY : Measurable Y) : + condDistrib Y X μ =ᵐ[μ.map X] fun b ↦ (μ[|X ⁻¹' {b}]).map Y := by + rw [Filter.EventuallyEq, ae_iff_of_countable] + intro b hb + ext s hs + rw [condDistrib_apply_of_ne_zero hY, + Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs, + Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs), + cond_apply (hX (measurableSet_singleton _))] + · congr + · exact hb + +lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α} + (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : + ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ + +lemma condDistrib_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) + (hX : Measurable X) (hY : Measurable Y) : + condDistrib Y X μ =ᵐ[μ.map X] fun _ ↦ μ.map Y := by + sorry + +lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ) + (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s) + (hμs : μ (X ⁻¹' s) ≠ 0) : + (μ[|X ⁻¹' s]).map T = μ.map T := by + ext t ht + rw [Measure.map_apply (by fun_prop) ht, Measure.map_apply (by fun_prop) ht, cond_apply (hX hs), + IndepSet.measure_inter_eq_mul, ← mul_assoc, ENNReal.inv_mul_cancel, one_mul] + · exact hμs + · simp + · rw [indepFun_iff_indepSet_preimage hX hT] at h + exact h s t hs ht + +lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} + [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] + (hG : G ≤ mα) : + CondIndep G F H hG μ + ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by + sorry + +lemma condDistrib_of_condIndepFun + [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] + (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) + (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : + condDistrib Y (fun ω ↦ (X ω, Z ω)) μ + =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] fun p ↦ condDistrib Y Z μ p.2 := by + sorry + +lemma cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] + (hZ : Measurable Z) + (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) + (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) {t : Set Ω'} + (ht : MeasurableSet t) (hμs : μ (Z ⁻¹' t) ≠ 0) : + (μ[|X ⁻¹' s ∩ Z ⁻¹' t]).map Y = (μ[|Z ⁻¹' t]).map Y := by + ext u hu + rw [Measure.map_apply (by fun_prop) hu, Measure.map_apply (by fun_prop) hu, cond_apply, + cond_apply] + rotate_left + · exact hZ ht + · exact (hX hs).inter (hZ ht) + rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hY hX] at h + specialize h u s hu hs + sorry + +end ProbabilityTheory diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 14fbfead..db000f01 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ import LeanBandits.Bandit +import LeanBandits.ForMathlib.CondDistrib import LeanBandits.Regret /-! # Laws of `stepsUntil` and `rewardByCount` @@ -12,125 +13,6 @@ import LeanBandits.Regret open MeasureTheory ProbabilityTheory Finset open scoped ENNReal NNReal -section Aux - -variable {α β γ Ω Ω' : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] - {mα : MeasurableSpace α} {μ : Measure α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} - [MeasurableSpace Ω'] [StandardBorelSpace Ω'] [Nonempty Ω'] - {X : α → β} {Y : α → Ω} {Z : α → Ω'} - -lemma MeasureTheory.Measure.comp_congr {κ η : Kernel α β} (h : ∀ᵐ a ∂μ, κ a = η a) : - κ ∘ₘ μ = η ∘ₘ μ := - Measure.bind_congr_right h - -lemma MeasureTheory.Measure.copy_comp_map (hX : AEMeasurable X μ) : - Kernel.copy β ∘ₘ (μ.map X) = μ.map (fun a ↦ (X a, X a)) := by - rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] - congr - -lemma MeasureTheory.Measure.compProd_deterministic [SFinite μ] (hX : Measurable X) : - μ ⊗ₘ (Kernel.deterministic X hX) = μ.map (fun a ↦ (a, X a)) := by - rw [Measure.compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic, - Measure.deterministic_comp_eq_map] - rfl - -lemma ProbabilityTheory.condDistrib_comp_map [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : - condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by - rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX] - -lemma ProbabilityTheory.condDistrib_comp [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : - condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by - rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop), - Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] - congr - -lemma ProbabilityTheory.condDistrib_const [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) (c : Ω) : - condDistrib (fun _ ↦ c) X μ =ᵐ[μ.map X] Kernel.deterministic (fun _ ↦ c) (by fun_prop) := by - have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl - conv_lhs => rw [this] - filter_upwards [condDistrib_comp hX (by fun_prop : Measurable (fun _ ↦ c))] with b hb - rw [hb] - -lemma ProbabilityTheory.condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β] - [IsFiniteMeasure μ] - (hX : Measurable X) (hY : Measurable Y) : - condDistrib Y X μ =ᵐ[μ.map X] fun b ↦ (μ[|X ⁻¹' {b}]).map Y := by - rw [Filter.EventuallyEq, ae_iff_of_countable] - intro b hb - ext s hs - rw [condDistrib_apply_of_ne_zero hY, - Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs, - Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs), - cond_apply (hX (measurableSet_singleton _))] - · congr - · exact hb - -lemma ProbabilityTheory.ae_cond_of_forall_mem {μ : Measure α} {s : Set α} - (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : - ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ - -lemma ProbabilityTheory.condDistrib_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) - (hX : Measurable X) (hY : Measurable Y) : - condDistrib Y X μ =ᵐ[μ.map X] fun _ ↦ μ.map Y := by - sorry - -omit [StandardBorelSpace Ω] [Nonempty Ω] in -lemma ProbabilityTheory.cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) - (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) - (hμs : μ (X ⁻¹' s) ≠ 0) : - (μ[|X ⁻¹' s]).map Y = μ.map Y := by - ext t ht - rw [Measure.map_apply (by fun_prop) ht, Measure.map_apply (by fun_prop) ht, cond_apply (hX hs), - IndepSet.measure_inter_eq_mul, ← mul_assoc, ENNReal.inv_mul_cancel, one_mul] - · exact hμs - · simp - · rw [indepFun_iff_indepSet_preimage hX hY] at h - exact h s t hs ht - -lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} - [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] - (hG : G ≤ mα) : - CondIndep G F H hG μ - ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by - sorry - -lemma ProbabilityTheory.condDistrib_of_condIndepFun - [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] - (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) - (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : - condDistrib Y (fun ω ↦ (X ω, Z ω)) μ - =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] fun p ↦ condDistrib Y Z μ p.2 := by - sorry - -lemma ProbabilityTheory.cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] - (hZ : Measurable Z) - (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) - (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) {t : Set Ω'} - (ht : MeasurableSet t) (hμs : μ (Z ⁻¹' t) ≠ 0) : - (μ[|X ⁻¹' s ∩ Z ⁻¹' t]).map Y = (μ[|Z ⁻¹' t]).map Y := by - ext u hu - rw [Measure.map_apply (by fun_prop) hu, Measure.map_apply (by fun_prop) hu, cond_apply, - cond_apply] - rotate_left - · exact hZ ht - · exact (hX hs).inter (hZ ht) - rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hY hX] at h - specialize h u s hu hs - sorry - -@[fun_prop] -lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) : - Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf - -@[fun_prop] -lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat) := - Measurable.comp (by fun_prop) hf - -end Aux - namespace Bandits variable {α : Type*} {mα : MeasurableSpace α} [DecidableEq α] [MeasurableSingletonClass α] From 71893a2b4339a746965d27f5750e78dbe08fed6d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 09:11:23 +0200 Subject: [PATCH 07/20] more condDistrib lemmas --- LeanBandits/ForMathlib/CondDistrib.lean | 57 +++++++++++++++++++++---- 1 file changed, 49 insertions(+), 8 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index f49c2c3e..c419bd10 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne -/ import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional -import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Condexp @@ -37,7 +36,7 @@ lemma copy_comp_map (hX : AEMeasurable X μ) : congr lemma compProd_deterministic [SFinite μ] (hX : Measurable X) : - μ ⊗ₘ (Kernel.deterministic X hX) = μ.map (fun a ↦ (a, X a)) := by + μ ⊗ₘ Kernel.deterministic X hX = μ.map (fun a ↦ (a, X a)) := by rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic, deterministic_comp_eq_map] rfl @@ -51,12 +50,43 @@ lemma condDistrib_comp_map [IsFiniteMeasure μ] condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX] +lemma condDistrib_congr [IsFiniteMeasure μ] {X' : α → β} {Y' : α → Ω} + (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') : + condDistrib Y X μ = condDistrib Y' X' μ := by + rw [condDistrib, condDistrib] + congr 1 + rw [Measure.map_congr] + filter_upwards [hX, hY] with a ha hb using by rw [ha, hb] + +lemma condDistrib_congr_right [IsFiniteMeasure μ] {X' : α → β} (hX : X =ᵐ[μ] X') : + condDistrib Y X μ = condDistrib Y X' μ := + condDistrib_congr (by rfl) hX + +lemma condDistrib_congr_left [IsFiniteMeasure μ] {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') : + condDistrib Y X μ = condDistrib Y' X μ := + condDistrib_congr hY (by rfl) + +lemma condDistrib_ae_eq_of_measure_eq_compProd₀ [IsFiniteMeasure μ] + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ] + (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : + ∀ᵐ x ∂μ.map X, κ x = condDistrib Y X μ x := by + suffices ∀ᵐ x ∂μ.map (hX.mk X), κ x = condDistrib (hY.mk Y) (hX.mk X) μ x by + rw [Measure.map_congr hX.ae_eq_mk] + convert this using 3 with b + rw [condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk] + refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) hX.measurable_mk hY.measurable_mk κ + ((Eq.trans ?_ hκ).trans ?_) + · refine Measure.map_congr ?_ + filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY] + · rw [Measure.map_congr hX.ae_eq_mk] + lemma condDistrib_comp [IsFiniteMeasure μ] (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by - rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop), - Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] - congr + symm + refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_ + rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] + rfl lemma condDistrib_const [IsFiniteMeasure μ] (hX : AEMeasurable X μ) (c : Ω) : @@ -85,9 +115,20 @@ lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α} ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ lemma condDistrib_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) - (hX : Measurable X) (hY : Measurable Y) : - condDistrib Y X μ =ᵐ[μ.map X] fun _ ↦ μ.map Y := by - sorry + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by + symm + refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_ + simp only [Measure.compProd_const] + exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h + +lemma indepFun_iff_condDistrib_eq_const [IsZeroOrProbabilityMeasure μ] + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by + refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩ + rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY, + Measure.compProd_congr h] + simp lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ) (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s) From 9013b208c6ea6ba3c034768207ebbf5006dff19e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 10:43:59 +0200 Subject: [PATCH 08/20] more indepedence work --- LeanBandits/ForMathlib/CondDistrib.lean | 185 ++++++++++++++++++------ 1 file changed, 139 insertions(+), 46 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index c419bd10..9b8960cb 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -5,6 +5,7 @@ Authors: Rémy Degenne -/ import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional +import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Condexp @@ -45,28 +46,30 @@ end MeasureTheory.Measure namespace ProbabilityTheory -lemma condDistrib_comp_map [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : +section CondDistrib + +variable [IsFiniteMeasure μ] + +lemma condDistrib_comp_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX] -lemma condDistrib_congr [IsFiniteMeasure μ] {X' : α → β} {Y' : α → Ω} - (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') : +lemma condDistrib_congr {X' : α → β} {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') : condDistrib Y X μ = condDistrib Y' X' μ := by rw [condDistrib, condDistrib] congr 1 rw [Measure.map_congr] filter_upwards [hX, hY] with a ha hb using by rw [ha, hb] -lemma condDistrib_congr_right [IsFiniteMeasure μ] {X' : α → β} (hX : X =ᵐ[μ] X') : +lemma condDistrib_congr_right {X' : α → β} (hX : X =ᵐ[μ] X') : condDistrib Y X μ = condDistrib Y X' μ := condDistrib_congr (by rfl) hX -lemma condDistrib_congr_left [IsFiniteMeasure μ] {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') : +lemma condDistrib_congr_left {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') : condDistrib Y X μ = condDistrib Y' X μ := condDistrib_congr hY (by rfl) -lemma condDistrib_ae_eq_of_measure_eq_compProd₀ [IsFiniteMeasure μ] +lemma condDistrib_ae_eq_of_measure_eq_compProd₀ (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ] (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : ∀ᵐ x ∂μ.map X, κ x = condDistrib Y X μ x := by @@ -80,22 +83,145 @@ lemma condDistrib_ae_eq_of_measure_eq_compProd₀ [IsFiniteMeasure μ] filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY] · rw [Measure.map_congr hX.ae_eq_mk] -lemma condDistrib_comp [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : +lemma condDistrib_comp (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by symm refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_ rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] rfl -lemma condDistrib_const [IsFiniteMeasure μ] - (hX : AEMeasurable X μ) (c : Ω) : +lemma condDistrib_const (hX : AEMeasurable X μ) (c : Ω) : condDistrib (fun _ ↦ c) X μ =ᵐ[μ.map X] Kernel.deterministic (fun _ ↦ c) (by fun_prop) := by have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl conv_lhs => rw [this] filter_upwards [condDistrib_comp hX (by fun_prop : Measurable (fun _ ↦ c))] with b hb rw [hb] +lemma condDistrib_of_indepFun (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by + symm + refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_ + simp only [Measure.compProd_const] + exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h + +lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by + refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩ + rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY, + Measure.compProd_congr h] + simp + +lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} + [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} : + (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by + rw [Kernel.prod_apply, Measure.prod_prod] + +theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} + {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ} + {μ : Measure Ω'} [IsFiniteMeasure μ] + {κ : Kernel Ω' α} [IsFiniteKernel κ] + -- TODO: relax this to CountableOrCountablyGenerated once it is fixed + [StandardBorelSpace β] [StandardBorelSpace γ] + (hf : Measurable X) (hg : Measurable T) : + IndepFun X T κ μ ↔ κ.map (fun ω ↦ (X ω, T ω)) =ᵐ[μ] ((κ.map X) ×ₖ (κ.map T)) := by + classical + rw [indepFun_iff_measure_inter_preimage_eq_mul] + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · rw [← Kernel.compProd_eq_iff] + have : (μ ⊗ₘ κ.map fun ω ↦ (X ω, T ω)) = μ ⊗ₘ (κ.map X ×ₖ κ.map T) + ↔ ∀ {u : Set Ω'} {s : Set β} {t : Set γ}, + MeasurableSet u → MeasurableSet s → MeasurableSet t → + (μ ⊗ₘ κ.map (fun ω ↦ (X ω, T ω))) (u ×ˢ s ×ˢ t) + = (μ ⊗ₘ (κ.map X ×ₖ κ.map T)) (u ×ˢ s ×ˢ t) := by + refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩ + sorry + rw [this] + intro u s t hu hs ht + rw [Measure.compProd_apply (hu.prod (hs.prod ht)), + Measure.compProd_apply (hu.prod (hs.prod ht))] + refine lintegral_congr_ae ?_ + have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp + simp_rw [h_set_eq] + filter_upwards [h s t hs ht] with ω hω + by_cases hωu : ω ∈ u + swap; · simp [hωu] + simp only [hωu, ↓reduceIte] + rw [Kernel.map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht)] + rw [Set.mk_preimage_prod, hω, Kernel.prod_apply_prod, Kernel.map_apply' _ (by fun_prop), + Kernel.map_apply' _ (by fun_prop)] + exacts [ht, hs] + · intro s t hs ht + filter_upwards [h] with ω hω + calc (κ ω) (X ⁻¹' s ∩ T ⁻¹' t) + _ = (κ.map (fun ω ↦ (X ω, T ω))) ω (s ×ˢ t) := by + rw [← Kernel.deterministic_comp_eq_map, ← deterministic_prod_deterministic hf hg, + Kernel.comp_apply, Measure.bind_apply (hs.prod ht) (by fun_prop)] + simp_rw [Kernel.prod_apply_prod, Kernel.deterministic_apply' hf _ hs, + Kernel.deterministic_apply' hg _ ht] + calc (κ ω) (X ⁻¹' s ∩ T ⁻¹' t) + _ = ∫⁻ a, (X ⁻¹' s ∩ T ⁻¹' t).indicator (fun x ↦ 1) a ∂κ ω := by + simp [lintegral_indicator ((hf hs).inter (hg ht))] + _ = ∫⁻ a, (X ⁻¹' s).indicator (fun x ↦ 1) a * (T ⁻¹' t).indicator (fun x ↦ 1) a ∂κ ω := by + congr with a + simp only [Set.indicator_apply, Set.mem_inter_iff, Set.mem_preimage, mul_ite, mul_one, + mul_zero] + by_cases has : X a ∈ s <;> simp [has] + _ = ∫⁻ a, s.indicator (fun x ↦ 1) (X a) * t.indicator (fun x ↦ 1) (T a) ∂κ ω := rfl + _ = ((κ.map X) ×ₖ (κ.map T)) ω (s ×ˢ t) := by rw [hω] + _ = (κ ω) (X ⁻¹' s) * (κ ω) (T ⁻¹' t) := by + rw [Kernel.prod_apply_prod, Kernel.map_apply' _ (by fun_prop), + Kernel.map_apply' _ (by fun_prop)] + exacts [ht, hs] + +theorem Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map{Ω' α β γ : Type*} + {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ} + {μ : Measure Ω'} [IsFiniteMeasure μ] + {κ : Kernel Ω' α} [IsFiniteKernel κ] + -- TODO: relax this to CountableOrCountablyGenerated once it is fixed + [StandardBorelSpace β] [StandardBorelSpace γ] + (hf : Measurable X) (hg : Measurable T) : + IndepFun X T κ μ ↔ (μ ⊗ₘ κ.map fun ω ↦ (X ω, T ω)) = μ ⊗ₘ (κ.map X ×ₖ κ.map T) := by + rw [Kernel.indepFun_iff_map_prod_eq_prod_map_map hf hg, Kernel.compProd_eq_iff] + +theorem condIndepFun_iff_map_prod_eq_prod_map_map {α : Type*} {m mα : MeasurableSpace α} + [StandardBorelSpace α] + {X : α → β} {T : α → γ} + {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ] + -- TODO: relax this to CountableOrCountablyGenerated once it is fixed + [StandardBorelSpace β] [StandardBorelSpace γ] + (hX : Measurable X) (hT : Measurable T) : + CondIndepFun m hm X T μ + ↔ (condExpKernel μ m).map (fun ω ↦ (X ω, T ω)) + =ᵐ[μ.trim hm] (((condExpKernel μ m).map X) ×ₖ ((condExpKernel μ m).map T)) := + Kernel.indepFun_iff_map_prod_eq_prod_map_map hX hT + +lemma condDistrib_of_condIndepFun [StandardBorelSpace α] + (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) + (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : + condDistrib Y (fun ω ↦ (X ω, Z ω)) μ + =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] Kernel.prodMkLeft _ (condDistrib Y Z μ) := by + symm + refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) (hX.prodMk hZ).aemeasurable + hY.aemeasurable _ ?_ + sorry + +end CondDistrib + +lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} + [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] + (hG : G ≤ mα) : + CondIndep G F H hG μ + ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by + sorry + +section Cond + +lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α} + (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : + ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ + lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β] [IsFiniteMeasure μ] (hX : Measurable X) (hY : Measurable Y) : @@ -110,26 +236,6 @@ lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β] · congr · exact hb -lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α} - (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : - ∀ᵐ x ∂μ[|s], p x := Measure.ae_smul_measure (ae_restrict_of_forall_mem hs h) _ - -lemma condDistrib_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X Y μ) - (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : - condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by - symm - refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_ - simp only [Measure.compProd_const] - exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h - -lemma indepFun_iff_condDistrib_eq_const [IsZeroOrProbabilityMeasure μ] - (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : - IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by - refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩ - rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY, - Measure.compProd_congr h] - simp - lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ) (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s) (hμs : μ (X ⁻¹' s) ≠ 0) : @@ -142,21 +248,6 @@ lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ) · rw [indepFun_iff_indepSet_preimage hX hT] at h exact h s t hs ht -lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} - [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] - (hG : G ≤ mα) : - CondIndep G F H hG μ - ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by - sorry - -lemma condDistrib_of_condIndepFun - [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] - (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) - (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : - condDistrib Y (fun ω ↦ (X ω, Z ω)) μ - =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] fun p ↦ condDistrib Y Z μ p.2 := by - sorry - lemma cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) @@ -173,4 +264,6 @@ lemma cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure specialize h u s hu hs sorry +end Cond + end ProbabilityTheory From 820f6e19a4cb4e2715af305b385610828a7c25c4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 12:02:29 +0200 Subject: [PATCH 09/20] more indep lemmas --- LeanBandits/ForMathlib/CondDistrib.lean | 92 +++++++++++++++++++++++-- 1 file changed, 87 insertions(+), 5 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 9b8960cb..13cdbcf9 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -5,6 +5,7 @@ Authors: Rémy Degenne -/ import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional +import Mathlib.Probability.Kernel.Composition.Lemmas import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Condexp @@ -116,6 +117,20 @@ lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by rw [Kernel.prod_apply, Measure.prod_prod] +lemma Measure.ext_prod₃ {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (h : ∀ {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) + (hu : MeasurableSet u), μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) : + μ = ν := by + sorry + +lemma Measure.ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : + μ = ν ↔ (∀ {s : Set α} {t : Set β} {u : Set γ}, + MeasurableSet s → MeasurableSet t → MeasurableSet u → + μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) := + ⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩ + theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ} @@ -135,7 +150,7 @@ theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} (μ ⊗ₘ κ.map (fun ω ↦ (X ω, T ω))) (u ×ˢ s ×ˢ t) = (μ ⊗ₘ (κ.map X ×ₖ κ.map T)) (u ×ˢ s ×ˢ t) := by refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩ - sorry + exact Measure.ext_prod₃ h rw [this] intro u s t hu hs ht rw [Measure.compProd_apply (hu.prod (hs.prod ht)), @@ -186,17 +201,84 @@ theorem Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map{Ω' α β rw [Kernel.indepFun_iff_map_prod_eq_prod_map_map hf hg, Kernel.compProd_eq_iff] theorem condIndepFun_iff_map_prod_eq_prod_map_map {α : Type*} {m mα : MeasurableSpace α} - [StandardBorelSpace α] - {X : α → β} {T : α → γ} + [StandardBorelSpace α] {X : α → β} {T : α → γ} {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ] -- TODO: relax this to CountableOrCountablyGenerated once it is fixed [StandardBorelSpace β] [StandardBorelSpace γ] (hX : Measurable X) (hT : Measurable T) : CondIndepFun m hm X T μ - ↔ (condExpKernel μ m).map (fun ω ↦ (X ω, T ω)) - =ᵐ[μ.trim hm] (((condExpKernel μ m).map X) ×ₖ ((condExpKernel μ m).map T)) := + ↔ (condExpKernel μ m).map (fun ω ↦ (X ω, T ω)) + =ᵐ[μ.trim hm] (((condExpKernel μ m).map X) ×ₖ ((condExpKernel μ m).map T)) := Kernel.indepFun_iff_map_prod_eq_prod_map_map hX hT +theorem condIndepFun_iff_map_prod_eq_prod_comp_trim + {α : Type*} {m mα : MeasurableSpace α} [StandardBorelSpace α] {X : α → β} {T : α → γ} + {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ] + -- TODO: relax this to CountableOrCountablyGenerated once it is fixed + [StandardBorelSpace β] [StandardBorelSpace γ] + (hX : Measurable X) (hT : Measurable T) : + CondIndepFun m hm X T μ + ↔ @Measure.map _ _ _ (m.prod _) (fun ω ↦ (ω, X ω, T ω)) μ + = (Kernel.id ×ₖ ((condExpKernel μ m).map X ×ₖ (condExpKernel μ m).map T)) ∘ₘ μ.trim hm := by + unfold CondIndepFun + rw [Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hX hT] + congr! + · calc (μ.trim hm ⊗ₘ (condExpKernel μ m).map fun ω ↦ (X ω, T ω)) + _ = (Kernel.id ∥ₖ Kernel.deterministic (fun ω ↦ (X ω, T ω)) (by fun_prop)) + ∘ₘ (μ.trim hm ⊗ₘ (condExpKernel μ m)) := by + rw [Measure.compProd_eq_parallelComp_comp_copy_comp, ← Kernel.deterministic_comp_eq_map, + ← Kernel.parallelComp_id_left_comp_parallelComp, Measure.comp_assoc, Kernel.comp_assoc, + Kernel.parallelComp_comp_copy, ← Measure.comp_assoc, Measure.compProd_eq_comp_prod] + _ = (Kernel.id ∥ₖ Kernel.deterministic (fun ω ↦ (X ω, T ω)) (by fun_prop)) + ∘ₘ (@Measure.map _ _ mα (m.prod mα) (fun ω ↦ (ω, ω)) μ) := by + congr + exact compProd_trim_condExpKernel hm + _ = _ := by + rw [← Measure.deterministic_comp_eq_map, Measure.comp_assoc, + ← Kernel.deterministic_prod_deterministic (g := fun ω ↦ ω), + Kernel.parallelComp_comp_prod, Kernel.deterministic_comp_deterministic, Kernel.id_comp, + Kernel.deterministic_prod_deterministic, Measure.deterministic_comp_eq_map] + · rfl + · exact Measurable.mono measurable_id le_rfl hm + · fun_prop + · rw [Measure.compProd_eq_comp_prod] + +theorem condIndepFun_comap_iff_map_prod_eq_compProd_condDistrib_prod_condDistrib + {α : Type*} {mα : MeasurableSpace α} [StandardBorelSpace α] + {X : α → β} {T : α → γ} {Z : α → Ω'} {μ : Measure α} [IsFiniteMeasure μ] + [StandardBorelSpace β] [StandardBorelSpace γ] [Nonempty β] [Nonempty γ] + (hX : Measurable X) (hT : Measurable T) (hZ : Measurable Z) : + CondIndepFun _ hZ.comap_le X T μ + ↔ μ.map (fun ω ↦ (Z ω, X ω, T ω)) + = (Kernel.id ×ₖ (condDistrib X Z μ ×ₖ condDistrib T Z μ)) ∘ₘ μ.map Z := by + rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hX hT] + simp_rw [Measure.ext_prod₃_iff] + have hZ_meas {s : Set Ω'} (hs : MeasurableSet s) : + MeasurableSet[MeasurableSpace.comap Z inferInstance] (Z ⁻¹' s) := by + rw [MeasurableSpace.measurableSet_comap] + exact ⟨s, hs, rfl⟩ + have h_left {s : Set Ω'} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) + (hu : MeasurableSet u) : + (μ.map (fun ω ↦ (Z ω, X ω, T ω))) (s ×ˢ t ×ˢ u) + = (@Measure.map _ _ _ ((MeasurableSpace.comap Z inferInstance).prod inferInstance) + (fun ω ↦ (ω, X ω, T ω)) μ) ((Z ⁻¹' s) ×ˢ t ×ˢ u) := by + rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)), + Measure.map_apply _ ((hZ_meas hs).prod (ht.prod hu))] + · simp [Set.mk_preimage_prod] + · refine Measurable.prodMk ?_ (by fun_prop) + exact Measurable.mono measurable_id le_rfl hZ.comap_le + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · intro s t u hs ht hu + specialize h (s := Z ⁻¹' s) (hZ_meas hs) ht hu + convert h + · exact h_left hs ht hu + · sorry + · rintro _ t u ⟨s, hs, rfl⟩ ht hu + specialize h hs ht hu + convert h + · exact (h_left hs ht hu).symm + · sorry + lemma condDistrib_of_condIndepFun [StandardBorelSpace α] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : From d4c5116e29d4e34fa6b3d4bacd27b0a2a89fcc5b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 15:04:57 +0200 Subject: [PATCH 10/20] more condDistrib --- LeanBandits/ForMathlib/CondDistrib.lean | 90 +++++++++++++++++++++++-- 1 file changed, 83 insertions(+), 7 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 13cdbcf9..a9b0bd74 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -43,6 +43,11 @@ lemma compProd_deterministic [SFinite μ] (hX : Measurable X) : deterministic_comp_eq_map] rfl +lemma trim_comap_apply (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) : + μ.trim hX.comap_le (X ⁻¹' s) = μ.map X s := by + rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs] + exact ⟨s, hs, rfl⟩ + end MeasureTheory.Measure namespace ProbabilityTheory @@ -131,6 +136,7 @@ lemma Measure.ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) := ⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩ +-- todo: use this to refactor `indepFun_iff_map_prod_eq_prod_map_map` theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ} @@ -189,7 +195,7 @@ theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} Kernel.map_apply' _ (by fun_prop)] exacts [ht, hs] -theorem Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map{Ω' α β γ : Type*} +lemma Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map {Ω' α β γ : Type*} {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ} {μ : Measure Ω'} [IsFiniteMeasure μ] @@ -211,7 +217,7 @@ theorem condIndepFun_iff_map_prod_eq_prod_map_map {α : Type*} {m mα : Measurab =ᵐ[μ.trim hm] (((condExpKernel μ m).map X) ×ₖ ((condExpKernel μ m).map T)) := Kernel.indepFun_iff_map_prod_eq_prod_map_map hX hT -theorem condIndepFun_iff_map_prod_eq_prod_comp_trim +lemma condIndepFun_iff_map_prod_eq_prod_comp_trim {α : Type*} {m mα : MeasurableSpace α} [StandardBorelSpace α] {X : α → β} {T : α → γ} {hm : m ≤ mα} {μ : Measure α} [IsFiniteMeasure μ] -- TODO: relax this to CountableOrCountablyGenerated once it is fixed @@ -243,7 +249,26 @@ theorem condIndepFun_iff_map_prod_eq_prod_comp_trim · fun_prop · rw [Measure.compProd_eq_comp_prod] -theorem condIndepFun_comap_iff_map_prod_eq_compProd_condDistrib_prod_condDistrib +lemma condDistrib_apply_ae_eq_condExpKernel_map + {α : Type*} {mα : MeasurableSpace α} [StandardBorelSpace α] + [StandardBorelSpace β] [Nonempty β] + {X : α → β} {T : α → γ} {μ : Measure α} [IsFiniteMeasure μ] + (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s) : + (fun a ↦ condDistrib X T μ (T a) s) + =ᵐ[μ] fun a ↦ (condExpKernel μ (MeasurableSpace.comap T inferInstance)).map X a s := by + have hT_meas {s : Set γ} (hs : MeasurableSet s) : + MeasurableSet[MeasurableSpace.comap T inferInstance] (T ⁻¹' s) := by + rw [MeasurableSpace.measurableSet_comap] + exact ⟨s, hs, rfl⟩ + have h1 := condDistrib_ae_eq_condExp hT hX (μ := μ) hs + simp_rw [Kernel.map_apply _ hX, Measure.map_apply hX hs] + have h2 := condExpKernel_ae_eq_condExp hT.comap_le (μ := μ) (hX hs) + filter_upwards [h1, h2] with a ha₁ ha₂ + rw [Measure.real] at ha₁ ha₂ + rw [← ENNReal.toReal_eq_toReal (by simp) (by simp), ha₁, ha₂] + +omit [Nonempty Ω'] in +theorem condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib {α : Type*} {mα : MeasurableSpace α} [StandardBorelSpace α] {X : α → β} {T : α → γ} {Z : α → Ω'} {μ : Measure α} [IsFiniteMeasure μ] [StandardBorelSpace β] [StandardBorelSpace γ] [Nonempty β] [Nonempty γ] @@ -267,19 +292,39 @@ theorem condIndepFun_comap_iff_map_prod_eq_compProd_condDistrib_prod_condDistrib · simp [Set.mk_preimage_prod] · refine Measurable.prodMk ?_ (by fun_prop) exact Measurable.mono measurable_id le_rfl hZ.comap_le + have h_right {s : Set Ω'} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) + (hu : MeasurableSet u) : + ((Kernel.id ×ₖ (condDistrib X Z μ ×ₖ condDistrib T Z μ)) ∘ₘ μ.map Z) (s ×ˢ t ×ˢ u) + = ((Kernel.id ×ₖ + ((condExpKernel μ (MeasurableSpace.comap Z inferInstance)).map X ×ₖ + (condExpKernel μ (MeasurableSpace.comap Z inferInstance)).map T)) ∘ₘ + μ.trim hZ.comap_le) ((Z ⁻¹' s) ×ˢ t ×ˢ u) := by + rw [Measure.bind_apply ((hZ_meas hs).prod (ht.prod hu)) (by fun_prop), + Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop), + lintegral_trim] + rotate_left + · exact Kernel.measurable_coe _ ((hZ_meas hs).prod (ht.prod hu)) + · exact Kernel.measurable_coe _ (hs.prod (ht.prod hu)) + refine lintegral_congr_ae ?_ + filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hX hZ ht, + condDistrib_apply_ae_eq_condExpKernel_map hT hZ hu] with a haX haT + simp_rw [Kernel.prod_apply_prod] + simp only [Kernel.id_apply, Measure.dirac_apply] + rw [@Measure.dirac_apply' _ (MeasurableSpace.comap Z inferInstance) _ _ (hZ_meas hs)] + congr refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ · intro s t u hs ht hu specialize h (s := Z ⁻¹' s) (hZ_meas hs) ht hu convert h · exact h_left hs ht hu - · sorry + · exact h_right hs ht hu · rintro _ t u ⟨s, hs, rfl⟩ ht hu specialize h hs ht hu convert h · exact (h_left hs ht hu).symm - · sorry + · exact (h_right hs ht hu).symm -lemma condDistrib_of_condIndepFun [StandardBorelSpace α] +lemma condDistrib_prod_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ @@ -287,7 +332,38 @@ lemma condDistrib_of_condIndepFun [StandardBorelSpace α] symm refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) (hX.prodMk hZ).aemeasurable hY.aemeasurable _ ?_ - sorry + rw [condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hY hX hZ] at h + rw [Measure.compProd_eq_comp_prod] + calc μ.map (fun x ↦ ((X x, Z x), Y x)) + _ = ((condDistrib X Z μ ×ₖ Kernel.id) ×ₖ condDistrib Y Z μ) ∘ₘ μ.map Z := by + -- up to shuffling, this is the previous lemma + sorry + _ = (Kernel.id ×ₖ Kernel.prodMkLeft β (condDistrib Y Z μ)) ∘ₘ Kernel.swap _ _ + ∘ₘ (μ.map Z ⊗ₘ condDistrib X Z μ) := by + rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc, Measure.comp_assoc] + congr + rw [Kernel.comp_assoc, Kernel.swap_prod] + ext ω : 1 + simp_rw [Kernel.prod_apply] + rw [Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply, ← Measure.compProd_eq_comp_prod] + ext s hs + rw [Measure.compProd_apply hs, Measure.prod_apply hs] + simp only [Kernel.prodMkLeft_apply] + rw [lintegral_prod, lintegral_prod] + · simp_rw [lintegral_dirac] + · refine Measurable.aemeasurable ?_ + have : Measurable fun a ↦ (Kernel.prodMkLeft _ (condDistrib Y Z μ) a) (Prod.mk a ⁻¹' s) := + Kernel.measurable_kernel_prodMk_left hs + exact this + · refine Measurable.aemeasurable ?_ + have : Measurable fun x ↦ (Kernel.const _ ((condDistrib Y Z μ) ω) x) (Prod.mk x ⁻¹' s) := + Kernel.measurable_kernel_prodMk_left hs + exact this + _ = (Kernel.id ×ₖ Kernel.prodMkLeft β (condDistrib Y Z μ)) ∘ₘ μ.map (fun a ↦ (X a, Z a)) := by + congr + rw [compProd_map_condDistrib hX.aemeasurable, Measure.swap_comp, + Measure.map_map (by fun_prop) (by fun_prop)] + rfl end CondDistrib From de9081087cb4097db78fafdfdc9c1af25e6768f4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 15:34:35 +0200 Subject: [PATCH 11/20] remove some sorry --- LeanBandits/ForMathlib/CondDistrib.lean | 76 ++++++++++++------------- LeanBandits/RewardByCountMeasure.lean | 26 ++++++--- 2 files changed, 55 insertions(+), 47 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index a9b0bd74..7d1833d3 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -48,10 +48,29 @@ lemma trim_comap_apply (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) : rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs] exact ⟨s, hs, rfl⟩ +lemma ext_prod₃ {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (h : ∀ {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) + (hu : MeasurableSet u), μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) : + μ = ν := by + sorry + +lemma ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : + μ = ν ↔ (∀ {s : Set α} {t : Set β} {u : Set γ}, + MeasurableSet s → MeasurableSet t → MeasurableSet u → + μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) := + ⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩ + end MeasureTheory.Measure namespace ProbabilityTheory +lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} + [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} : + (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by + rw [Kernel.prod_apply, Measure.prod_prod] + section CondDistrib variable [IsFiniteMeasure μ] @@ -117,25 +136,6 @@ lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasura Measure.compProd_congr h] simp -lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} - [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} : - (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by - rw [Kernel.prod_apply, Measure.prod_prod] - -lemma Measure.ext_prod₃ {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} - {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (h : ∀ {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) - (hu : MeasurableSet u), μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) : - μ = ν := by - sorry - -lemma Measure.ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} - {mγ : MeasurableSpace γ} {μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : - μ = ν ↔ (∀ {s : Set α} {t : Set β} {u : Set γ}, - MeasurableSet s → MeasurableSet t → MeasurableSet u → - μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) := - ⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩ - -- todo: use this to refactor `indepFun_iff_map_prod_eq_prod_map_map` theorem Kernel.indepFun_iff_map_prod_eq_prod_map_map {Ω' α β γ : Type*} {mΩ' : MeasurableSpace Ω'} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} @@ -367,13 +367,6 @@ lemma condDistrib_prod_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpa end CondDistrib -lemma condIndep_iff_condExpKernel_eq {α : Type*} {F G H mα : MeasurableSpace α} - [StandardBorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] - (hG : G ≤ mα) : - CondIndep G F H hG μ - ↔ condExpKernel μ (F ⊔ G) =ᵐ[@Measure.map _ _ mα H id μ] condExpKernel μ G := by - sorry - section Cond lemma ae_cond_of_forall_mem {μ : Measure α} {s : Set α} @@ -406,21 +399,26 @@ lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ) · rw [indepFun_iff_indepSet_preimage hX hT] at h exact h s t hs ht -lemma cond_of_condIndepFun [StandardBorelSpace α] [IsZeroOrProbabilityMeasure μ] +lemma cond_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β] [Countable β] + [Countable Ω'] + [IsZeroOrProbabilityMeasure μ] (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) - (hX : Measurable X) (hY : Measurable Y) {s : Set β} (hs : MeasurableSet s) {t : Set Ω'} - (ht : MeasurableSet t) (hμs : μ (Z ⁻¹' t) ≠ 0) : - (μ[|X ⁻¹' s ∩ Z ⁻¹' t]).map Y = (μ[|Z ⁻¹' t]).map Y := by - ext u hu - rw [Measure.map_apply (by fun_prop) hu, Measure.map_apply (by fun_prop) hu, cond_apply, - cond_apply] - rotate_left - · exact hZ ht - · exact (hX hs).inter (hZ ht) - rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hY hX] at h - specialize h u s hu hs - sorry + (hX : Measurable X) (hY : Measurable Y) {b : β} {ω : Ω'} + (hμ : μ (X ⁻¹' {b} ∩ Z ⁻¹' {ω}) ≠ 0) : + (μ[|X ⁻¹' {b} ∩ Z ⁻¹' {ω}]).map Y = (μ[|Z ⁻¹' {ω}]).map Y := by + have h := condDistrib_prod_of_condIndepFun hX hY hZ h + have h_left := condDistrib_ae_eq_cond (hX.prodMk hZ) hY (μ := μ) + have h_right := condDistrib_ae_eq_cond hZ hY (μ := μ) + rw [Filter.EventuallyEq, ae_iff_of_countable] at h h_left h_right + specialize h (b, ω) + specialize h_left (b, ω) + specialize h_right ω + rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at h h_left h_right + rw [← Set.singleton_prod_singleton, Set.mk_preimage_prod] at h h_left + have hZ_ne : μ (Z ⁻¹' {ω}) ≠ 0 := fun h ↦ hμ (measure_mono_null Set.inter_subset_right h) + rw [← h_right hZ_ne, ← h_left hμ, h hμ] + simp end Cond diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index db000f01..eb36e067 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -129,10 +129,24 @@ lemma reward_condIndepFun_stepsUntil_arm [StandardBorelSpace α] [Countable α] sorry lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ) - (hm : m ≠ 0) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : + (hm : m ≠ 0) + (hμn : (Bandit.measure alg ν) ((fun ω ↦ stepsUntil (arm · ω.1) a m) ⁻¹' {↑n}) ≠ 0) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m ← (n : ℕ∞); Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν + have hμna : + μ ((fun ω ↦ stepsUntil (arm · ω.1) a m) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) ≠ 0 := by + suffices ((fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ + stepsUntil (arm · ω.1) a m) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) + = (fun ω ↦ stepsUntil (arm · ω.1) a m) ⁻¹' {↑n} by simpa [this] using hμn + ext ω + simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, and_iff_left_iff_imp] + exact arm_eq_of_stepsUntil_eq_coe hm + have hμa : μ.map (fun ω ↦ arm n ω.1) {a} ≠ 0 := by + rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] + refine fun h_zero ↦ hμn (measure_mono_null (fun ω ↦ ?_) h_zero) + simp only [Set.mem_preimage, Set.mem_singleton_iff] + exact arm_eq_of_stepsUntil_eq_coe hm calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m ← (n : ℕ∞); μ] _ = (μ[|(fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map (fun ω ↦ reward n ω.1) := by @@ -140,9 +154,8 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and] exact arm_eq_of_stepsUntil_eq_coe hm _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by - rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop) - (measurableSet_singleton _) (measurableSet_singleton _)] - · rwa [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hμa + rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop)] + · exact hμna · exact reward_condIndepFun_stepsUntil_arm a m n _ = ν a := reward_cond_arm a n hμa @@ -176,10 +189,7 @@ lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α simp only [Set.mem_preimage, Set.mem_singleton_iff] exact fun ω ↦ rewardByCount_of_stepsUntil_eq_coe refine reward_cond_stepsUntil a m n hm ?_ - rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hn ⊢ - refine fun h_zero ↦ hn (measure_mono_null (fun ω ↦ ?_) h_zero) - simp only [Set.mem_preimage, Set.mem_singleton_iff] - exact arm_eq_of_stepsUntil_eq_coe hm + rwa [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hn /-- The reward received at the `m`-th pull of arm `a` has law `ν a`. -/ lemma hasLaw_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] From 9b21c10b619abcc692e2073ea292ed4a86ba86bd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 16:49:58 +0200 Subject: [PATCH 12/20] prove a sorry --- LeanBandits/ForMathlib/CondDistrib.lean | 23 ++++++++++++++++++++ LeanBandits/RewardByCountMeasure.lean | 28 ++++++++++++++++++------- 2 files changed, 44 insertions(+), 7 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 7d1833d3..4c39d2de 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -324,6 +324,7 @@ theorem condIndepFun_comap_iff_map_prod_eq_prod_condDistrib_prod_condDistrib · exact (h_left hs ht hu).symm · exact (h_right hs ht hu).symm +-- todo: should be an iff lemma condDistrib_prod_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ) : @@ -365,6 +366,28 @@ lemma condDistrib_prod_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpa Measure.map_map (by fun_prop) (by fun_prop)] rfl +lemma condDistrib_fst_prod (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) + (ν : Measure γ) [IsProbabilityMeasure ν] : + condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν) =ᵐ[μ.map X] condDistrib Y X μ := by + refine condDistrib_ae_eq_of_measure_eq_compProd₀ (μ := μ) hX hY _ ?_ + have hX_map : (μ.prod ν).map (fun ω ↦ X ω.1) = μ.map X := by + calc (μ.prod ν).map (fun ω ↦ X ω.1) + _ = ((μ.prod ν).map Prod.fst).map X := by + rw [AEMeasurable.map_map_of_aemeasurable ?_ (by fun_prop)] + · rfl + · rw [Measure.map_fst_prod] + exact hX.smul_measure _ + _ = μ.map X := by simp [Measure.map_fst_prod] + rw [← hX_map, compProd_map_condDistrib] + · calc μ.map (fun x ↦ (X x, Y x)) + _ = ((μ.prod ν).map Prod.fst).map (fun a ↦ (X a, Y a)) := by simp [Measure.map_fst_prod] + _ = (μ.prod ν).map (fun a ↦ (X a.1, Y a.1)) := by + rw [AEMeasurable.map_map_of_aemeasurable ?_ (by fun_prop)] + · rfl + · simp only [Measure.map_fst_prod, measure_univ, one_smul] + fun_prop + · fun_prop + end CondDistrib section Cond diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index eb36e067..0df8dafa 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -104,14 +104,29 @@ notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ /-- Law of `Y`. -/ notation "𝓛[" Y "; " μ "]" => Measure.map Y μ +omit [DecidableEq α] in lemma reward_cond_arm [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (n : ℕ) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν - have h_ra : (condDistrib (fun ω ↦ reward n ω.1) (fun ω ↦ arm n ω.1) μ) - =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν := by - have h_ra' := condDistrib_reward alg ν n - sorry + have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[𝓛[fun ω ↦ arm n ω.1; μ]] ν := by + have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] + =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] ν := + condDistrib_reward alg ν n + have h_law : 𝓛[fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1; μ] + = 𝓛[arm n; Bandit.trajMeasure alg ν] := by + calc μ.map (fun ω ↦ arm n ω.1) + _ = (((Bandit.trajMeasure alg ν).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.1)).map + (fun ω ↦ arm n ω) := by + rw [Measure.map_map (by fun_prop) (by fun_prop)] + rfl + _ = _ := by simp [Measure.map_fst_prod] + rw [h_law] + have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] + =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] := + condDistrib_fst_prod (by fun_prop) (by fun_prop) _ + filter_upwards [h_ra', h_prod] with ω h_eq h_prod + rw [h_prod, h_eq] have h_eq := condDistrib_ae_eq_cond (μ := μ) (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop) rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq @@ -154,9 +169,8 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and] exact arm_eq_of_stepsUntil_eq_coe hm _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by - rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop)] - · exact hμna - · exact reward_condIndepFun_stepsUntil_arm a m n + rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop) hμna] + exact reward_condIndepFun_stepsUntil_arm a m n _ = ν a := reward_cond_arm a n hμa lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α] From 5be80f3a6109f3c16e394274aa2d128a4a7ea6fa Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 16:54:22 +0200 Subject: [PATCH 13/20] lint --- LeanBandits/RewardByCountMeasure.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 0df8dafa..fa030a75 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -105,7 +105,7 @@ notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ notation "𝓛[" Y "; " μ "]" => Measure.map Y μ omit [DecidableEq α] in -lemma reward_cond_arm [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (n : ℕ) +lemma reward_cond_arm [Countable α] (a : α) (n : ℕ) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν From 1cf82d2ee28c6c934e3b530dccce051c106775ac Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 17:01:44 +0200 Subject: [PATCH 14/20] remove a false statement --- LeanBandits/RewardByCountMeasure.lean | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index fa030a75..766f5890 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -135,14 +135,6 @@ lemma reward_cond_arm [Countable α] (a : α) (n : ℕ) rw [h_ra] at h_eq exact h_eq.symm -lemma reward_condIndepFun_stepsUntil_arm [StandardBorelSpace α] [Countable α] [Nonempty α] - (a : α) (m n : ℕ) : - CondIndepFun (MeasurableSpace.comap (fun ω ↦ arm n ω.1) inferInstance) - (Measurable.comap_le <| by fun_prop) (fun ω ↦ reward n ω.1) - (fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m) (Bandit.measure alg ν) := by - let μ := Bandit.measure alg ν - sorry - lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ) (hm : m ≠ 0) (hμn : (Bandit.measure alg ν) ((fun ω ↦ stepsUntil (arm · ω.1) a m) ⁻¹' {↑n}) ≠ 0) : @@ -169,8 +161,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and] exact arm_eq_of_stepsUntil_eq_coe hm _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by - rw [cond_of_condIndepFun (by fun_prop) ?_ (by fun_prop) (by fun_prop) hμna] - exact reward_condIndepFun_stepsUntil_arm a m n + sorry _ = ν a := reward_cond_arm a n hμa lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α] From 2f8e4b83c31d78aa784054b3f8766abe8e7fe19a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 17:20:15 +0200 Subject: [PATCH 15/20] extract lemma --- LeanBandits/RewardByCountMeasure.lean | 41 +++++++++++++++------------ 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 766f5890..355b5fd7 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -104,29 +104,34 @@ notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ /-- Law of `Y`. -/ notation "𝓛[" Y "; " μ "]" => Measure.map Y μ +omit [DecidableEq α] [MeasurableSingletonClass α] in +lemma condDistrib_reward' (n : ℕ) : + 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν] + =ᵐ[𝓛[fun ω ↦ arm n ω.1; Bandit.measure alg ν]] ν := by + let μ := Bandit.measure alg ν + have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] + =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] ν := condDistrib_reward alg ν n + have h_law : 𝓛[fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1; μ] + = 𝓛[arm n; Bandit.trajMeasure alg ν] := by + calc μ.map (fun ω ↦ arm n ω.1) + _ = (μ.map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by + rw [Measure.map_map (by fun_prop) (by fun_prop)] + rfl + _ = _ := by unfold μ Bandit.measure; simp [Measure.map_fst_prod] + rw [h_law] + have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] + =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] := + condDistrib_fst_prod (by fun_prop) (by fun_prop) _ + filter_upwards [h_ra', h_prod] with ω h_eq h_prod + rw [h_prod, h_eq] + omit [DecidableEq α] in lemma reward_cond_arm [Countable α] (a : α) (n : ℕ) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν - have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[𝓛[fun ω ↦ arm n ω.1; μ]] ν := by - have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] - =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] ν := - condDistrib_reward alg ν n - have h_law : 𝓛[fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1; μ] - = 𝓛[arm n; Bandit.trajMeasure alg ν] := by - calc μ.map (fun ω ↦ arm n ω.1) - _ = (((Bandit.trajMeasure alg ν).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.1)).map - (fun ω ↦ arm n ω) := by - rw [Measure.map_map (by fun_prop) (by fun_prop)] - rfl - _ = _ := by simp [Measure.map_fst_prod] - rw [h_law] - have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] - =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] := - condDistrib_fst_prod (by fun_prop) (by fun_prop) _ - filter_upwards [h_ra', h_prod] with ω h_eq h_prod - rw [h_prod, h_eq] + have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[𝓛[fun ω ↦ arm n ω.1; μ]] ν := + condDistrib_reward' n have h_eq := condDistrib_ae_eq_cond (μ := μ) (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop) rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq From efe3f7a748665d752ee3eccdf30aac021a0fd539 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 17:25:01 +0200 Subject: [PATCH 16/20] add CondIndepFun lemma --- LeanBandits/Bandit.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index f47e8fa4..cf016d7b 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -158,6 +158,13 @@ lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace map_eq := by sorry +lemma condIndepFun_reward_arm_hist [StandardBorelSpace α] [StandardBorelSpace R] + {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) : + CondIndepFun (MeasurableSpace.comap (hist n) inferInstance) + (Measurable.comap_le (by fun_prop)) + (reward n) (arm n) (Bandit.trajMeasure alg ν) := by + sorry + end MeasureSpace end Bandits From cc884b13884d736a8e151e1b52588911a59bf8ab Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 9 Sep 2025 17:26:50 +0200 Subject: [PATCH 17/20] minor --- LeanBandits/Bandit.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index cf016d7b..05667f53 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -161,8 +161,7 @@ lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace lemma condIndepFun_reward_arm_hist [StandardBorelSpace α] [StandardBorelSpace R] {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) : CondIndepFun (MeasurableSpace.comap (hist n) inferInstance) - (Measurable.comap_le (by fun_prop)) - (reward n) (arm n) (Bandit.trajMeasure alg ν) := by + (measurable_hist n).comap_le (reward n) (arm n) (Bandit.trajMeasure alg ν) := by sorry end MeasureSpace From cd7f53c838ae357f8f7c61d83fec782d3d26133f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 10 Sep 2025 10:59:59 +0200 Subject: [PATCH 18/20] CondIndepFun progress --- LeanBandits/Bandit.lean | 7 +-- LeanBandits/ForMathlib/CondDistrib.lean | 9 ++++ LeanBandits/Regret.lean | 20 +++++-- LeanBandits/RewardByCountMeasure.lean | 71 ++++++++++++++++++++++++- 4 files changed, 98 insertions(+), 9 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 05667f53..7f981c3f 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -158,10 +158,11 @@ lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace map_eq := by sorry -lemma condIndepFun_reward_arm_hist [StandardBorelSpace α] [StandardBorelSpace R] +/-- The reward at time `n+1` is independent of the history up to time `n` given the arm at `n+1`. -/ +lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [StandardBorelSpace R] {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) : - CondIndepFun (MeasurableSpace.comap (hist n) inferInstance) - (measurable_hist n).comap_le (reward n) (arm n) (Bandit.trajMeasure alg ν) := by + CondIndepFun (MeasurableSpace.comap (arm (n + 1)) inferInstance) + (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) := by sorry end MeasureSpace diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 4c39d2de..f1a8b6db 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -71,6 +71,15 @@ lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by rw [Kernel.prod_apply, Measure.prod_prod] +lemma CondIndepFun.prod_right + {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + {mδ : MeasurableSpace δ} [StandardBorelSpace α] + {μ : Measure α} [IsFiniteMeasure μ] {X : α → β} {Y : α → γ} {Z : α → δ} + (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) + (h : CondIndepFun (mδ.comap Z) hZ.comap_le X Y μ) : + CondIndepFun (mδ.comap Z) hZ.comap_le X (fun ω ↦ (Y ω, Z ω)) μ := by + sorry + section CondDistrib variable [IsFiniteMeasure μ] diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean index 7df22ec9..6d5d363c 100644 --- a/LeanBandits/Regret.lean +++ b/LeanBandits/Regret.lean @@ -130,15 +130,27 @@ lemma arm_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount (arm · h) a (s rwa [← pullCount_eq_pullCount] exact h_ne -lemma arm_eq_of_stepsUntil_eq_coe {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)} (hm : m ≠ 0) - (h : stepsUntil (arm · ω.1) a m = n) : - arm n ω.1 = a := by - have : n = (stepsUntil (fun x ↦ arm x ω.1) a m).toNat := by simp [h] +lemma arm_eq_of_stepsUntil_eq_coe {ω : ℕ → α × ℝ} (hm : m ≠ 0) + (h : stepsUntil (arm · ω) a m = n) : + arm n ω = a := by + have : n = (stepsUntil (fun x ↦ arm x ω) a m).toNat := by simp [h] rw [this, arm_stepsUntil hm] by_contra! h_contra rw [← stepsUntil_eq_top_iff] at h_contra simp [h_contra] at h +lemma stepsUntil_eq_congr {k' : ℕ → α} (h : ∀ i ≤ n, k i = k' i) : + stepsUntil k a m = n ↔ stepsUntil k' a m = n := by + sorry + +lemma pullCount_stepsUntil_add_one (h_exists : ∃ s, pullCount k a (s + 1) = m) : + pullCount k a (stepsUntil k a m + 1).toNat = m := by + sorry + +lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount k a (s + 1) = m) : + pullCount k a (stepsUntil k a m).toNat = m - 1 := by + sorry + /-- Reward obtained when pulling arm `a` for the `m`-th time. -/ noncomputable def rewardByCount (a : α) (m : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : ℝ := diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index 355b5fd7..be63b971 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -140,6 +140,62 @@ lemma reward_cond_arm [Countable α] (a : α) (n : ℕ) rw [h_ra] at h_eq exact h_eq.symm +lemma condIndepFun_reward_stepsUntil_arm [StandardBorelSpace α] [Countable α] [Nonempty α] + (a : α) (m n : ℕ) (hm : m ≠ 0) : + CondIndepFun (mα.comap (fun ω ↦ arm n ω.1)) ((measurable_arm n).comp measurable_fst).comap_le + (fun ω ↦ reward n ω.1) ({ω | stepsUntil (arm · ω.1) a m = ↑n}.indicator (fun _ ↦ 1)) + (Bandit.measure alg ν) := by + -- first restrict to the `trajMeasure` side + suffices h_indep : + CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le + (reward n) ({ω | stepsUntil (arm · ω) a m = ↑n}.indicator (fun _ ↦ 1)) + (Bandit.trajMeasure alg ν) by + sorry + -- Now prove the independence : the indicator of `stepsUntil ... = n` is a function of + -- `hist (n-1)` and `arm n`. + -- It thus suffices to prove the independence of `reward n` and `hist (n-1)` conditionally + -- on `arm n`. + have hn : n ≠ 0 := by + sorry -- assume it? + have h_indep : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n) + (hist (n - 1)) (Bandit.trajMeasure alg ν) := by + convert condIndepFun_reward_hist_arm (alg := alg) (ν := ν) (n - 1) + <;> rw [Nat.sub_add_cancel (by grind)] + have h_indep' : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n) + (fun ω ↦ (hist (n - 1) ω, arm n ω)) (Bandit.trajMeasure alg ν) := + h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop) + suffices ∃ φ : ((Iic (n - 1) → α × ℝ) × α) → ℕ, Measurable φ ∧ + ({ω : ℕ → α × ℝ | stepsUntil (arm · ω) a m = ↑n}.indicator (fun _ ↦ 1)) + = φ ∘ (fun ω : ℕ → α × ℝ ↦ (hist (n - 1) ω, arm n ω)) by + obtain ⟨φ, hφ_meas, h_eq⟩ := this + rw [h_eq] + exact h_indep'.comp measurable_id hφ_meas + -- it would follow from measurability wrt the sigma-algebra generated by + -- `hist (n-1)` and `arm n`, but we can also give an explicit function + let k : ((Iic (n - 1) → α × ℝ) × α) → (ℕ → α) := fun x i ↦ + if hi : i ∈ Iic (n - 1) then (x.1 ⟨i, hi⟩).1 else if i = n then x.2 else a -- a is arbitrary + let φ : ((Iic (n - 1) → α × ℝ) × α) → ℕ := fun x ↦ if stepsUntil (k x) a m = ↑n then 1 else 0 + classical + have hφ_meas : Measurable φ := by + refine Measurable.ite ?_ (by fun_prop) (by fun_prop) + refine (measurableSet_singleton _).preimage ?_ + refine (measurable_stepsUntil a m).comp ?_ + unfold k + rw [measurable_pi_iff] + intro i + split_ifs <;> fun_prop + refine ⟨φ, hφ_meas, ?_⟩ + ext ω + classical + simp only [Set.indicator_apply, Set.mem_setOf_eq, Function.comp_apply, φ] + congr 1 + rw [stepsUntil_eq_congr] + intro i hin + simp only [arm, mem_Iic, hist, dite_eq_ite, left_eq_ite_iff, not_le, k] + intro hni + have : i = n := by grind + simp [this] + lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ) (hm : m ≠ 0) (hμn : (Bandit.measure alg ν) ((fun ω ↦ stepsUntil (arm · ω.1) a m) ⁻¹' {↑n}) ≠ 0) : @@ -159,14 +215,25 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α refine fun h_zero ↦ hμn (measure_mono_null (fun ω ↦ ?_) h_zero) simp only [Set.mem_preimage, Set.mem_singleton_iff] exact arm_eq_of_stepsUntil_eq_coe hm - calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m ← (n : ℕ∞); μ] + calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil (arm · ω.1) a m ← (n : ℕ∞); μ] _ = (μ[|(fun ω ↦ stepsUntil (fun x ↦ arm x ω.1) a m) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map (fun ω ↦ reward n ω.1) := by congr with ω simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and] exact arm_eq_of_stepsUntil_eq_coe hm + _ = (μ[|{ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) | stepsUntil (arm · ω.1) a m = ↑n}.indicator 1 ⁻¹' {1} + ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map (fun ω ↦ reward n ω.1) := by + congr 3 with ω + simp [Set.indicator_apply] _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by - sorry + rw [cond_of_condIndepFun (by fun_prop)] + · exact condIndepFun_reward_stepsUntil_arm a m n hm + · refine measurable_one.indicator ?_ + exact measurableSet_eq_fun' (by fun_prop) (by fun_prop) + · fun_prop + · convert hμna + ext ω + simp [Set.indicator_apply] _ = ν a := reward_cond_arm a n hμa lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α] From e7d7a0b7bd867282edec81c72f0c7f6dde27a617 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 10 Sep 2025 11:10:39 +0200 Subject: [PATCH 19/20] remove a notation --- LeanBandits/RewardByCountMeasure.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index be63b971..a4d8185d 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -101,18 +101,16 @@ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) /-- Law of `Y` conditioned on `X`. -/ notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ -/-- Law of `Y`. -/ -notation "𝓛[" Y "; " μ "]" => Measure.map Y μ omit [DecidableEq α] [MeasurableSingletonClass α] in lemma condDistrib_reward' (n : ℕ) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν] - =ᵐ[𝓛[fun ω ↦ arm n ω.1; Bandit.measure alg ν]] ν := by + =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ arm n ω.1)] ν := by let μ := Bandit.measure alg ν have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] - =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] ν := condDistrib_reward alg ν n - have h_law : 𝓛[fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1; μ] - = 𝓛[arm n; Bandit.trajMeasure alg ν] := by + =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := condDistrib_reward alg ν n + have h_law : μ.map (fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1) + = (Bandit.trajMeasure alg ν).map (arm n) := by calc μ.map (fun ω ↦ arm n ω.1) _ = (μ.map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by rw [Measure.map_map (by fun_prop) (by fun_prop)] @@ -120,7 +118,7 @@ lemma condDistrib_reward' (n : ℕ) : _ = _ := by unfold μ Bandit.measure; simp [Measure.map_fst_prod] rw [h_law] have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] - =ᵐ[𝓛[arm n; Bandit.trajMeasure alg ν]] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] := + =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] := condDistrib_fst_prod (by fun_prop) (by fun_prop) _ filter_upwards [h_ra', h_prod] with ω h_eq h_prod rw [h_prod, h_eq] @@ -130,7 +128,7 @@ lemma reward_cond_arm [Countable α] (a : α) (n : ℕ) (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν - have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[𝓛[fun ω ↦ arm n ω.1; μ]] ν := + have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν := condDistrib_reward' n have h_eq := condDistrib_ae_eq_cond (μ := μ) (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop) From ecf6245cdcf353ff49b3f43718f304ebe512c6ba Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 10 Sep 2025 11:11:25 +0200 Subject: [PATCH 20/20] minor --- LeanBandits/RewardByCountMeasure.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index a4d8185d..35db1592 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -109,8 +109,7 @@ lemma condDistrib_reward' (n : ℕ) : let μ := Bandit.measure alg ν have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := condDistrib_reward alg ν n - have h_law : μ.map (fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦ arm n ω.1) - = (Bandit.trajMeasure alg ν).map (arm n) := by + have h_law : μ.map (fun ω ↦ arm n ω.1) = (Bandit.trajMeasure alg ν).map (arm n) := by calc μ.map (fun ω ↦ arm n ω.1) _ = (μ.map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by rw [Measure.map_map (by fun_prop) (by fun_prop)]