From ac51cd189ca367e44ba706009326c46089709f78 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 11:05:56 +0100 Subject: [PATCH] feat: the chain rule for the divergence at a stopping time, with equality Prove that the chain rule at a stopping time is an equality when the hitting time is almost surely finite under both algorithm-environment pairs, for the series, integral and bandit (pull count) forms, through the chain rule at a bounded stopping time for the histories stopped at a fixed time. Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- LMLExplore/Probability/HasCondDistrib.lean | 23 +- .../DivergenceDecomposition.lean | 249 ++++++++++++++++-- .../SequentialLearning/StoppedHistory.lean | 231 +++++++++++++++- 3 files changed, 475 insertions(+), 28 deletions(-) diff --git a/LMLExplore/Probability/HasCondDistrib.lean b/LMLExplore/Probability/HasCondDistrib.lean index 23f0db28..3d890f1d 100644 --- a/LMLExplore/Probability/HasCondDistrib.lean +++ b/LMLExplore/Probability/HasCondDistrib.lean @@ -27,12 +27,16 @@ conditional distribution `η` given `f` of the first coordinate. `∫⁻ ω in X ⁻¹' s, g (Y ω) ∂P = ∫⁻ ω in X ⁻¹' s, ∫⁻ y, g y ∂(κ (X ω)) ∂P`. * `ProbabilityTheory.HasCondDistrib.lintegral_comp_prodMk_eq_lintegral_lintegral`: `∫⁻ ω, g (X ω, Y ω) ∂P = ∫⁻ ω, ∫⁻ y, g (X ω, y) ∂(κ (X ω)) ∂P`. +* `ProbabilityTheory.HasCondDistrib.restrict_preimage`: `κ` is still the conditional + distribution of `Y` given `X` under the restriction of `P` to an event `X ⁻¹' s`. * `ProbabilityTheory.HasCondDistrib.ae_mem`: if every conditional law is concentrated on a set, then `Y` lies in that set almost surely. * `ProbabilityTheory.hasCondDistrib_snd_compProd_comap`: under `μ ⊗ₘ η.comap f`, the second coordinate has conditional distribution `η` given `f` of the first coordinate. -The last statement is adapted from the LMLPapers project (same author). +The last statement is adapted from the LMLPapers project (same author), and +`HasCondDistrib.restrict_preimage` from the Essakine2026Tight project +(`RemyDegenne/Essakine2026Tight`, Apache 2.0, `ForLMLExplore/Probability/CondDistrib.lean`). -/ public section @@ -95,6 +99,23 @@ lemma HasCondDistrib.lintegral_comp_prodMk_eq_lintegral_lintegral (h : HasCondDi _ = ∫⁻ ω, ∫⁻ y, g (X ω, y) ∂(κ (X ω)) ∂P := lintegral_map' hg.lintegral_kernel_prod_right'.aemeasurable h.aemeasurable_fst +/-- If `κ` is the conditional distribution of `Y` given `X` under `P`, it is also the conditional +distribution of `Y` given `X` under the restriction of `P` to an event `X ⁻¹' s` determined by +`X`. -/ +lemma HasCondDistrib.restrict_preimage (h : HasCondDistrib Y X κ P) {s : Set 𝓧} + (hs : MeasurableSet s) : + HasCondDistrib Y X κ (P.restrict (X ⁻¹' s)) := by + refine ⟨h.aemeasurable.restrict, ?_⟩ + have h_pre : (fun ω ↦ (X ω, Y ω)) ⁻¹' (s ×ˢ Set.univ) = X ⁻¹' s := by + rw [Set.mk_preimage_prod, Set.preimage_univ, Set.inter_univ] + calc (P.restrict (X ⁻¹' s)).map (fun ω ↦ (X ω, Y ω)) + = (P.map (fun ω ↦ (X ω, Y ω))).restrict (s ×ˢ Set.univ) := by + rw [Measure.restrict_map_of_aemeasurable h.aemeasurable (hs.prod .univ), h_pre] + _ = (P.map X).restrict s ⊗ₘ κ := by + rw [h.map_eq, Measure.compProd_restrict_left _ _ hs] + _ = (P.restrict (X ⁻¹' s)).map X ⊗ₘ κ := by + rw [Measure.restrict_map_of_aemeasurable h.aemeasurable_fst hs] + omit [SFinite P] [IsSFiniteKernel κ] in /-- If `κ` is the conditional distribution of `Y` given `X` and every measure `κ x` is concentrated on a measurable set `t`, then `Y` lies in `t` almost surely. -/ diff --git a/LMLExplore/SequentialLearning/DivergenceDecomposition.lean b/LMLExplore/SequentialLearning/DivergenceDecomposition.lean index 37875865..7512ea42 100644 --- a/LMLExplore/SequentialLearning/DivergenceDecomposition.lean +++ b/LMLExplore/SequentialLearning/DivergenceDecomposition.lean @@ -36,6 +36,12 @@ against two stationary environments and an almost surely finite `τ`, it gives `KL ≤ ∑ a, E[N_a(τ)] KL(κ a ‖ κ' a)`. This is the change of measure behind the lower bounds of bandit identification. +The bound is an equality when `τ` is almost surely finite under both pairs. At a fixed time `M`, +the divergence between the laws of the histories stopped at `M`, the histories of the first +`min M τ` rounds, is the sum over the rounds `t < M` of the same terms, without any finiteness +assumption. For one algorithm against two stationary environments, the equality reads +`KL = ∑ a, E[N_a(τ)] KL(κ a ‖ κ' a)`. + ## Main statements * `Learning.IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount`: the divergence decomposition. @@ -46,9 +52,15 @@ bandit identification. * `Learning.klDiv_stoppedHistMeasure_le_tsum`: the chain rule at a stopping time for any two algorithm-environment pairs, as a series over the rounds of the divergences of the steps, with the law of the history restricted to the histories after which `S` has not stopped. -* `Learning.klDiv_stoppedHistMeasure_le_lintegral`: its integral form +* `Learning.IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory`: the chain rule at a bounded + stopping time, with equality, for the histories stopped at a fixed time `M`. +* `Learning.klDiv_stoppedHistMeasure_eq_tsum`: the chain rule at a stopping time is an equality + when the hitting time is almost surely finite under both pairs. +* `Learning.klDiv_stoppedHistMeasure_le_lintegral`, + `Learning.klDiv_stoppedHistMeasure_eq_lintegral`: their integral forms `KL ≤ E[∑ t < τ, KL(stepKernel alg env t (H t) ‖ stepKernel alg' env' t (H t))]`, for countably - generated spaces and an almost surely finite hitting time `τ`. + generated spaces and an almost surely finite hitting time `τ`, with equality when `τ` is also + almost surely finite under `(alg', env')`. * `Learning.IsAlgEnvSeq.klDiv_restrict_compProd_stepKernel_bandit`: for one algorithm against two stationary environments, the divergence of the step of round `t` on an event of the history of the first `t` rounds is the expected divergence between the reward kernels at the played action @@ -57,6 +69,8 @@ bandit identification. `KL(stoppedHistMeasure alg (Environment.bandit κ) S ‖ stoppedHistMeasure alg (Environment.bandit κ') S) ≤ ∑ a, E_κ[N_a(τ)] KL(κ a ‖ κ' a)` when the hitting time `τ` of `S` is almost surely finite under `κ`. +* `Learning.klDiv_stoppedHistMeasure_eq`: the same decomposition with equality when `τ` is also + almost surely finite under `κ'`. ## References @@ -71,6 +85,10 @@ bandit identification. * The proofs of the fixed-horizon statements are adapted from the formalization in the LMLPapers project (`LMLPapers/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean`). +* The proof of the equality at a stopping time, by induction over the histories stopped at a + fixed time and truncation of the stopped history, is adapted from the formalization in the + Essakine2026Tight project (`RemyDegenne/Essakine2026Tight`, Apache 2.0, + `ForLMLExplore/InformationTheory/KLStoppedPrefix.lean`). -/ public section @@ -89,12 +107,81 @@ environment `env'.piecewise` below follow `(alg', env')` until `τ` and `(alg, e Their stopped history has the same law as under `(alg', env')` (`stoppedHistMeasure_congr`), and the divergence between their trajectory and the trajectory under `(alg, env)` only collects the rounds before `τ` (`klDiv_compProd_piecewise`). The data processing inequality for the stopped -history, a function of the trajectory, concludes. -/ +history, a function of the trajectory, gives the bound. The partial sums of the series are the +divergences between the laws of the histories stopped at a fixed time +(`IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory`), which are truncations of the stopped +histories when `τ` is almost surely finite under both pairs: the data processing inequality for +the truncation gives the converse. -/ variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {alg alg' : Algorithm 𝓞 𝓐 𝓨} {env env' : Environment 𝓞 𝓐 𝓨} {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} +/-- **Chain rule at a bounded stopping time.** For two algorithms `alg`, `alg'` run against two +environments `env`, `env'` and a measurable stopping rule `S` with hitting time `τ`, the divergence +between the laws of the histories stopped at the time `M`, that is of the histories of the first +`min M τ` rounds, is the sum over the rounds `t < M` of the divergences of the step at round `t`, +where the law of the history of the first `t` rounds under `(alg, env)` is restricted to the +histories after which `S` has not stopped. -/ +theorem IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} + {mΩ' : MeasurableSpace Ω'} {P : Measure Ω} {P' : Measure Ω'} [IsProbabilityMeasure P] + [IsProbabilityMeasure P'] {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} + {O' : ℕ → Ω' → 𝓞} {X' : ℕ → Ω' → 𝓐} {Y' : ℕ → Ω' → 𝓨} + (h : IsAlgEnvSeq O X Y alg env P) (h' : IsAlgEnvSeq O' X' Y' alg' env' P') + (hS : MeasurableSet S) (M : ℕ) : + klDiv (P.map (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M)) + (P'.map (stoppedProcess (sigmaHistory O' X' Y') + (hittingAfter (sigmaHistory O' X' Y') S 0) M)) = + ∑ t ∈ range M, klDiv + ((P.map (history O X Y t)).restrict (notStoppedSet S t) ⊗ₘ stepKernel alg env t) + ((P.map (history O X Y t)).restrict (notStoppedSet S t) ⊗ₘ stepKernel alg' env' t) := by + have hO := h.measurable_obs + have hX := h.measurable_action + have hY := h.measurable_feedback + have hO' := h'.measurable_obs + have hX' := h'.measurable_action + have hY' := h'.measurable_feedback + induction M with + | zero => + simp only [stoppedProcess_sigmaHistory_zero, Measure.map_const, measure_univ, one_smul, + klDiv_self, range_zero, sum_empty] + | succ M ih => + have hN := measurableSet_notStoppedSet hS M + have hT : MeasurableSet (Sigma.mk M '' notStoppedSet S M) := + (measurableEmbedding_sigmaMk M).measurableSet_image.2 hN + -- The image by `Sigma.mk M` of a measure restricted to `notStoppedSet S M` lives on the + -- histories of `M` rounds in `notStoppedSet S M`. + have h_supp (μ : Measure (Hist 𝓞 𝓐 𝓨 M)) : + (μ.restrict (notStoppedSet S M)).map (Sigma.mk M) (Sigma.mk M '' notStoppedSet S M)ᶜ = + 0 := by + rw [Measure.map_apply (measurable_sigmaMk M) hT.compl, Set.preimage_compl, + Set.preimage_image_eq _ sigma_mk_injective, Measure.restrict_apply hN.compl, + Set.compl_inter_self, measure_empty] + -- Split the laws of the histories stopped at the times `M` and `M + 1` according to whether + -- round `M` is played. The two parts have disjoint supports, so that the divergences add up, + -- and on the event that round `M` is played the chain rule for the step of round `M` applies. + rw [sum_range_succ, ← ih, map_stoppedProcess_sigmaHistory_succ_eq_add hO hX hY hS M, + map_stoppedProcess_sigmaHistory_succ_eq_add hO' hX' hY' hS M, + map_stoppedProcess_sigmaHistory_eq_add (P := P) hO hX hY hS M, + map_stoppedProcess_sigmaHistory_eq_add (P := P') hO' hX' hY' hS M, + klDiv_add_add_of_measure_eq_zero (measurableSet_sigma_fst_le M) + (map_stoppedProcess_sigmaHistory_apply_compl_fst_le hO hX hY + (measurable_hittingAfter_sigmaHistory hO hX hY hS) M) + (map_stoppedProcess_sigmaHistory_apply_compl_fst_le hO' hX' hY' + (measurable_hittingAfter_sigmaHistory hO' hX' hY' hS) M) + (Measure.map_sigmaMk_succ_apply_fst_le _) (Measure.map_sigmaMk_succ_apply_fst_le _), + klDiv_add_add_of_measure_eq_zero hT.compl + (by rw [compl_compl] + exact map_restrict_stoppedProcess_sigmaHistory_apply_image_notStoppedSet hO hX hY hS M) + (by rw [compl_compl] + exact map_restrict_stoppedProcess_sigmaHistory_apply_image_notStoppedSet hO' hX' hY' + hS M) + (h_supp _) (h_supp _), + klDiv_map_measurableEmbedding _ _ (measurableEmbedding_sigmaMk (M + 1)), + klDiv_map_measurableEmbedding _ _ (measurableEmbedding_sigmaMk M), + h.map_restrict_history_succ hN, h'.map_restrict_history_succ hN, klDiv_map_measurableEquiv, + klDiv_compProd_eq_add, add_assoc] + /-- **Chain rule at a stopping time.** For two algorithms `alg`, `alg'` run against two environments `env`, `env'` and a measurable stopping rule `S`, the divergence between the laws of the histories stopped by `S` is at most the series over the rounds `t` of the divergences of the @@ -129,18 +216,50 @@ theorem klDiv_stoppedHistMeasure_le_tsum (hS : MeasurableSet S) : rw [h_chain] exact tsum_congr fun t ↦ by rw [stepKernel_piecewise, klDiv_compProd_piecewise] -/-- **Chain rule at a stopping time**, integral form. For two algorithms `alg`, `alg'` run against -two environments `env`, `env'` with countably generated spaces of observations, actions and -feedback, and a measurable stopping rule `S` whose hitting time `τ` is almost surely finite under -`(alg, env)`, the divergence between the laws of the histories stopped by `S` is at most -`E[∑ t < τ, KL(stepKernel alg env t (H t) ‖ stepKernel alg' env' t (H t))]`, where `H t` is the -history of the first `t` rounds under `(alg, env)`. -/ -theorem klDiv_stoppedHistMeasure_le_lintegral [MeasurableSpace.CountablyGenerated 𝓞] - [MeasurableSpace.CountablyGenerated 𝓐] [MeasurableSpace.CountablyGenerated 𝓨] - (hS : MeasurableSet S) +/-- **Chain rule at a stopping time**, with equality. For two algorithms `alg`, `alg'` run against +two environments `env`, `env'` and a measurable stopping rule `S` whose hitting time is almost +surely finite under both pairs, the divergence between the laws of the histories stopped by `S` +is the series over the rounds `t` of the divergences of the step at round `t`, where the law of +the history of the first `t` rounds under `(alg, env)` is restricted to the histories after which +`S` has not stopped. -/ +theorem klDiv_stoppedHistMeasure_eq_tsum (hS : MeasurableSet S) (hτ : ∀ᵐ ω ∂(trajMeasure alg env), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) + (hτ' : ∀ᵐ ω ∂(trajMeasure alg' env'), hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : - klDiv (stoppedHistMeasure alg env S) (stoppedHistMeasure alg' env' S) ≤ + klDiv (stoppedHistMeasure alg env S) (stoppedHistMeasure alg' env' S) = + ∑' t, klDiv + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg env t) + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg' env' t) := by + refine le_antisymm (klDiv_stoppedHistMeasure_le_tsum hS) + (ENNReal.tsum_le_of_sum_range_le fun M ↦ ?_) + have hτm := measurable_hittingAfter_sigmaHistory (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) + IT.measurable_obs IT.measurable_action IT.measurable_feedback hS + -- The sum over the rounds `t < M` is the divergence between the laws of the histories stopped + -- at the time `M`, which are the truncations to at most `M` rounds of the stopped histories. + rw [← (IT.isAlgEnvSeq_trajMeasure alg env).klDiv_map_stoppedProcess_sigmaHistory + (IT.isAlgEnvSeq_trajMeasure alg' env') hS M, + map_stoppedProcess_sigmaHistory_eq_map_truncHist IT.measurable_obs IT.measurable_action + IT.measurable_feedback hτm hτ M, + map_stoppedProcess_sigmaHistory_eq_map_truncHist IT.measurable_obs IT.measurable_action + IT.measurable_feedback hτm hτ' M, stoppedHistMeasure, stoppedHistMeasure] + exact klDiv_map_le _ _ (measurable_truncHist M) + +/-- For countably generated spaces and a hitting time `τ` of `S` that is almost surely finite +under `(alg, env)`, the series of the chain rule at a stopping time is +`E[∑ t < τ, KL(stepKernel alg env t (H t) ‖ stepKernel alg' env' t (H t))]`. -/ +private lemma tsum_klDiv_restrict_compProd_stepKernel_eq_lintegral + [MeasurableSpace.CountablyGenerated 𝓞] [MeasurableSpace.CountablyGenerated 𝓐] + [MeasurableSpace.CountablyGenerated 𝓨] (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg env), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + ∑' t, klDiv + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg env t) + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg' env' t) = ∫⁻ ω, ∑ t ∈ range (ENat.toNat (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)), klDiv (stepKernel alg env t (history IT.obs IT.action IT.feedback t ω)) @@ -153,12 +272,54 @@ theorem klDiv_stoppedHistMeasure_le_lintegral [MeasurableSpace.CountablyGenerate klDiv (stepKernel alg env t (history IT.obs IT.action IT.feedback t ω)) (stepKernel alg' env' t (history IT.obs IT.action IT.feedback t ω)) := (measurable_klDiv_kernel _ _).comp (hH t) - refine (klDiv_stoppedHistMeasure_le_tsum hS).trans_eq ((tsum_congr fun t ↦ ?_).trans + refine (tsum_congr fun t ↦ ?_).trans (tsum_setLIntegral_notStoppedSet IT.measurable_obs IT.measurable_action IT.measurable_feedback - hS hτ hf)) + hS hτ hf) rw [klDiv_compProd_right_eq_lintegral, setLIntegral_map (measurableSet_notStoppedSet hS t) (measurable_klDiv_kernel _ _) (hH t)] +/-- **Chain rule at a stopping time**, integral form. For two algorithms `alg`, `alg'` run against +two environments `env`, `env'` with countably generated spaces of observations, actions and +feedback, and a measurable stopping rule `S` whose hitting time `τ` is almost surely finite under +`(alg, env)`, the divergence between the laws of the histories stopped by `S` is at most +`E[∑ t < τ, KL(stepKernel alg env t (H t) ‖ stepKernel alg' env' t (H t))]`, where `H t` is the +history of the first `t` rounds under `(alg, env)`. -/ +theorem klDiv_stoppedHistMeasure_le_lintegral [MeasurableSpace.CountablyGenerated 𝓞] + [MeasurableSpace.CountablyGenerated 𝓐] [MeasurableSpace.CountablyGenerated 𝓨] + (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg env), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + klDiv (stoppedHistMeasure alg env S) (stoppedHistMeasure alg' env' S) ≤ + ∫⁻ ω, ∑ t ∈ range (ENat.toNat + (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)), + klDiv (stepKernel alg env t (history IT.obs IT.action IT.feedback t ω)) + (stepKernel alg' env' t (history IT.obs IT.action IT.feedback t ω)) + ∂(trajMeasure alg env) := + (klDiv_stoppedHistMeasure_le_tsum hS).trans_eq + (tsum_klDiv_restrict_compProd_stepKernel_eq_lintegral hS hτ) + +/-- **Chain rule at a stopping time**, integral form with equality. For two algorithms `alg`, +`alg'` run against two environments `env`, `env'` with countably generated spaces of +observations, actions and feedback, and a measurable stopping rule `S` whose hitting time `τ` is +almost surely finite under both pairs, the divergence between the laws of the histories stopped by +`S` is `E[∑ t < τ, KL(stepKernel alg env t (H t) ‖ stepKernel alg' env' t (H t))]`, where `H t` +is the history of the first `t` rounds under `(alg, env)`. -/ +theorem klDiv_stoppedHistMeasure_eq_lintegral [MeasurableSpace.CountablyGenerated 𝓞] + [MeasurableSpace.CountablyGenerated 𝓐] [MeasurableSpace.CountablyGenerated 𝓨] + (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg env), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) + (hτ' : ∀ᵐ ω ∂(trajMeasure alg' env'), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + klDiv (stoppedHistMeasure alg env S) (stoppedHistMeasure alg' env' S) = + ∫⁻ ω, ∑ t ∈ range (ENat.toNat + (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)), + klDiv (stepKernel alg env t (history IT.obs IT.action IT.feedback t ω)) + (stepKernel alg' env' t (history IT.obs IT.action IT.feedback t ω)) + ∂(trajMeasure alg env) := + (klDiv_stoppedHistMeasure_eq_tsum hS hτ hτ').trans + (tsum_klDiv_restrict_compProd_stepKernel_eq_lintegral hS hτ) + end ChainRule variable {𝓐 𝓨 : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} @@ -259,16 +420,19 @@ lemma IsAlgEnvSeq.klDiv_restrict_compProd_stepKernel_bandit variable {S : Set (Σ n : ℕ, Hist Unit 𝓐 𝓨 n)} -/-- **Divergence decomposition at a stopping time.** Let `τ` be the hitting time of a measurable -stopping rule `S` by an algorithm run against a stationary environment with reward kernel `κ`, and -suppose that `τ` is almost surely finite. Then the relative entropy between the laws of the history -stopped by `S` under the reward kernels `κ` and `κ'` is at most -`∑ a, E_κ[N_a(τ)] KL(κ a ‖ κ' a)`, where `N_a(τ)` is the number of pulls of `a` before `τ`. -/ -theorem klDiv_stoppedHistMeasure_le (hS : MeasurableSet S) +/-- For one algorithm against two stationary environments with reward kernels `κ` and `κ'` and a +hitting time `τ` of `S` that is almost surely finite under `κ`, the series of the chain rule at a +stopping time is `∑ a, E_κ[N_a(τ)] KL(κ a ‖ κ' a)`. -/ +private lemma tsum_klDiv_restrict_compProd_stepKernel_bandit_eq_sum (hS : MeasurableSet S) (hτ : ∀ᵐ ω ∂(trajMeasure alg (Environment.bandit κ)), hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : - klDiv (stoppedHistMeasure alg (Environment.bandit κ) S) - (stoppedHistMeasure alg (Environment.bandit κ') S) ≤ + ∑' t, klDiv + (((trajMeasure alg (Environment.bandit κ)).map + (history IT.obs IT.action IT.feedback t)).restrict (notStoppedSet S t) ⊗ₘ + stepKernel alg (Environment.bandit κ) t) + (((trajMeasure alg (Environment.bandit κ)).map + (history IT.obs IT.action IT.feedback t)).restrict (notStoppedSet S t) ⊗ₘ + stepKernel alg (Environment.bandit κ') t) = ∑ a, (∫⁻ ω, (pullCount IT.action a (ENat.toNat (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)) ω : ℝ≥0∞) ∂(trajMeasure alg (Environment.bandit κ))) * klDiv (κ a) (κ' a) := by @@ -278,14 +442,47 @@ theorem klDiv_stoppedHistMeasure_le (hS : MeasurableSet S) have hf (t : ℕ) : Measurable fun ω : ℕ → Round Unit 𝓐 𝓨 ↦ klDiv (κ (IT.action t ω)) (κ' (IT.action t ω)) := (measurable_klDiv_kernel κ κ').comp (IT.measurable_action t) - refine (klDiv_stoppedHistMeasure_le_tsum hS).trans_eq - (((tsum_congr fun t ↦ h.klDiv_restrict_compProd_stepKernel_bandit (κ' := κ') + refine ((tsum_congr fun t ↦ h.klDiv_restrict_compProd_stepKernel_bandit (κ' := κ') (measurableSet_notStoppedSet hS t)).trans (tsum_setLIntegral_notStoppedSet IT.measurable_obs IT.measurable_action - IT.measurable_feedback hS hτ hf)).trans ?_) + IT.measurable_feedback hS hτ hf)).trans ?_ exact (LMLExplore.sum_lintegral_pullCount_mul IT.measurable_action (Measurable.of_discrete.comp hτm) fun a ↦ klDiv (κ a) (κ' a)).symm +/-- **Divergence decomposition at a stopping time.** Let `τ` be the hitting time of a measurable +stopping rule `S` by an algorithm run against a stationary environment with reward kernel `κ`, and +suppose that `τ` is almost surely finite. Then the relative entropy between the laws of the history +stopped by `S` under the reward kernels `κ` and `κ'` is at most +`∑ a, E_κ[N_a(τ)] KL(κ a ‖ κ' a)`, where `N_a(τ)` is the number of pulls of `a` before `τ`. -/ +theorem klDiv_stoppedHistMeasure_le (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg (Environment.bandit κ)), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + klDiv (stoppedHistMeasure alg (Environment.bandit κ) S) + (stoppedHistMeasure alg (Environment.bandit κ') S) ≤ + ∑ a, (∫⁻ ω, (pullCount IT.action a + (ENat.toNat (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)) ω : + ℝ≥0∞) ∂(trajMeasure alg (Environment.bandit κ))) * klDiv (κ a) (κ' a) := + (klDiv_stoppedHistMeasure_le_tsum hS).trans_eq + (tsum_klDiv_restrict_compProd_stepKernel_bandit_eq_sum hS hτ) + +/-- **Divergence decomposition at a stopping time**, with equality. Let `τ` be the hitting time of +a measurable stopping rule `S` by an algorithm run against two stationary environments with reward +kernels `κ` and `κ'`, and suppose that `τ` is almost surely finite under both. Then the relative +entropy between the laws of the history stopped by `S` under `κ` and `κ'` is +`∑ a, E_κ[N_a(τ)] KL(κ a ‖ κ' a)`, where `N_a(τ)` is the number of pulls of `a` before `τ`. -/ +theorem klDiv_stoppedHistMeasure_eq (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg (Environment.bandit κ)), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) + (hτ' : ∀ᵐ ω ∂(trajMeasure alg (Environment.bandit κ')), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + klDiv (stoppedHistMeasure alg (Environment.bandit κ) S) + (stoppedHistMeasure alg (Environment.bandit κ') S) = + ∑ a, (∫⁻ ω, (pullCount IT.action a + (ENat.toNat (hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω)) ω : + ℝ≥0∞) ∂(trajMeasure alg (Environment.bandit κ))) * klDiv (κ a) (κ' a) := + (klDiv_stoppedHistMeasure_eq_tsum hS hτ hτ').trans + (tsum_klDiv_restrict_compProd_stepKernel_bandit_eq_sum hS hτ) + end StoppingTime end Learning diff --git a/LMLExplore/SequentialLearning/StoppedHistory.lean b/LMLExplore/SequentialLearning/StoppedHistory.lean index 8acc60f8..0cbca039 100644 --- a/LMLExplore/SequentialLearning/StoppedHistory.lean +++ b/LMLExplore/SequentialLearning/StoppedHistory.lean @@ -7,11 +7,13 @@ module public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace public import LeanMachineLearning.SequentialLearning.StoppedHistory +public import LMLExplore.Probability.HasCondDistrib +public import Mathlib.Data.Fin.Tuple.Take public import LMLExplore.Topology.Algebra.InfiniteSum.NatInt public import TauCeti.Probability.Kernel.Composition.MeasureCompProd /-! -# The law of a stopped history only depends on the rounds before stopping +# Stopped histories: dependence on the rounds before stopping, histories stopped at a fixed time Complements to LML's `LeanMachineLearning.SequentialLearning.StoppedHistory`. A stopping rule `S : Set (Σ n, Hist 𝓞 𝓐 𝓨 n)` stops the interaction after `n` rounds if the history of these @@ -26,10 +28,18 @@ pairs whose step kernels agree on `notStoppedSet S n` for every `n` give the sam stopped history. This is the basis of the change of measure at stopping times: an environment can be modified after the stopping time without changing the law of the stopped history. +The history stopped at a fixed time `M`, `stoppedProcess (sigmaHistory O X Y) τ M`, is the history +of the first `min M τ` rounds. Its law splits according to whether round `M` is played, which +gives the chain rule for the divergence at a bounded stopping time +(`Learning.IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory`); when `τ` is almost surely finite, +it is the image of the law of the stopped history by the truncation `truncHist M` to at most `M` +rounds. + ## Main definitions * `Learning.notStoppedSet S n`: the `n`-round histories after which the stopping rule `S` has not stopped, that is, none of whose prefixes belong to `S`. +* `Learning.truncHist M`: the truncation of a history of variable length to at most `M` rounds. ## Main statements @@ -41,6 +51,19 @@ can be modified after the stopping time without changing the law of the stopped * `Learning.stoppedHistMeasure_congr`: if the step kernels of `(alg, env)` and `(alg', env')` agree on `notStoppedSet S n` for every `n`, then `stoppedHistMeasure alg env S = stoppedHistMeasure alg' env' S`. +* `Learning.map_stoppedProcess_sigmaHistory_eq_map_truncHist`: for an almost surely finite `τ`, + the law of the history stopped at the time `M` is the image of the law of the stopped history by + `truncHist M`. +* `Learning.map_stoppedProcess_sigmaHistory_eq_add`, + `Learning.map_stoppedProcess_sigmaHistory_succ_eq_add`: the laws of the histories stopped at the + times `M` and `M + 1` split according to whether round `M` is played. +* `Learning.IsAlgEnvSeq.map_restrict_history_succ`: on an event of the history of the first `M` + rounds, the law of the history of the first `M + 1` rounds is the composition-product of the + restricted law of the history of the first `M` rounds with the step kernel of round `M`. + +The material on the histories stopped at a fixed time is adapted from the formalization of prefixes +of stopped processes in the Essakine2026Tight project (`RemyDegenne/Essakine2026Tight`, +Apache 2.0, `ForLMLExplore/Probability/Process/SigmaPrefix.lean`). -/ public section @@ -353,4 +376,210 @@ theorem stoppedHistMeasure_congr (hS : MeasurableSet S) end Congr + +section StoppedAtTime + +/-! ### Histories stopped at a fixed time + +Let `τ` be the hitting time of a stopping rule `S`. The history stopped at the time `M`, +`stoppedProcess (sigmaHistory O X Y) τ M`, is the history of the first `min M τ` rounds. Its law +splits according to whether round `M` is played, that is whether the history of the first `M` +rounds lies in `notStoppedSet S M`: if it is not, the history stopped at `M + 1` is the history +stopped at `M`; if it is, the history stopped at `M` is the history of the first `M` rounds and +the history stopped at `M + 1` is the history of the first `M + 1` rounds. When `τ` is finite, the +history stopped at `M` is the truncation `truncHist M` of the history stopped at `τ`. -/ + +/-- The truncation of a history of variable length to at most `M` rounds: a history of `n` +rounds is sent to the history of its first `min M n` rounds (`Fin.take`). -/ +def truncHist (M : ℕ) (h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + ⟨min M h.1, Fin.take (min M h.1) (min_le_right M h.1) h.2⟩ + +/-- Unfolding lemma for `truncHist`. -/ +lemma truncHist_def (M : ℕ) (h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) : + truncHist M h = ⟨min M h.1, Fin.take (min M h.1) (min_le_right M h.1) h.2⟩ := (rfl) + +/-- The truncation of histories of variable length is measurable. -/ +@[fun_prop] +lemma measurable_truncHist (M : ℕ) : Measurable (truncHist (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) M) := + measurable_sigma fun n ↦ (measurable_sigmaMk (min M n)).comp + (Measurable.of_eval fun i ↦ measurable_pi_apply (Fin.castLE (min_le_right M n) i)) + +/-- Truncating the history of the first `n` rounds to at most `M` rounds gives the history of the +first `min M n` rounds. -/ +@[simp] +lemma truncHist_sigmaHistory (M n : ℕ) (ω : Ω) : + truncHist M (sigmaHistory O X Y n ω) = sigmaHistory O X Y (min M n) ω := (rfl) + +/-- Truncating the history stopped at a finite time `τ` to at most `M` rounds gives the history +stopped at the time `M`. -/ +lemma truncHist_stoppedValue_sigmaHistory {τ : Ω → WithTop ℕ} (hτ : τ ω ≠ ⊤) (M : ℕ) : + truncHist M (stoppedValue (sigmaHistory O X Y) τ ω) = + stoppedProcess (sigmaHistory O X Y) τ M ω := by + obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 hτ + simp only [stoppedValue, stoppedProcess, ← hk, ← WithTop.coe_min, WithTop.untopD_coe, + truncHist_sigmaHistory] + +/-- The history stopped at the time `M` by a measurable time `τ` is measurable. -/ +@[fun_prop] +lemma measurable_stoppedProcess_sigmaHistory (hO : ∀ n, Measurable (O n)) + (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) {τ : Ω → WithTop ℕ} + (hτ : Measurable τ) (M : ℕ) : + Measurable (stoppedProcess (sigmaHistory O X Y) τ M) := + measurable_stoppedValue_sigmaHistory hO hX hY (measurable_const.min hτ) + +/-- For a measurable time `τ` that is almost surely finite, the law of the history stopped at the +time `M` is the image of the law of the history stopped at `τ` by the truncation to at most `M` +rounds. -/ +lemma map_stoppedProcess_sigmaHistory_eq_map_truncHist {P : Measure Ω} + (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) + {τ : Ω → WithTop ℕ} (hτm : Measurable τ) (hτ : ∀ᵐ ω ∂P, τ ω ≠ ⊤) (M : ℕ) : + P.map (stoppedProcess (sigmaHistory O X Y) τ M) = + (P.map (stoppedValue (sigmaHistory O X Y) τ)).map (truncHist M) := by + rw [Measure.map_map (measurable_truncHist M) + (measurable_stoppedValue_sigmaHistory hO hX hY hτm)] + refine Measure.map_congr ?_ + filter_upwards [hτ] with ω hω + exact (truncHist_stoppedValue_sigmaHistory hω M).symm + +/-- The history stopped at the time `0` is the empty history. -/ +lemma stoppedProcess_sigmaHistory_zero (τ : Ω → WithTop ℕ) : + stoppedProcess (sigmaHistory O X Y) τ 0 = fun _ ↦ ⟨0, default⟩ := by + funext ω + rw [stoppedProcess_eq_of_le (i := 0) bot_le, sigmaHistory_apply, history_zero] + +/-- If round `M` is played, the history stopped at the time `M` is the history of the first `M` +rounds. -/ +lemma stoppedProcess_sigmaHistory_of_mem_notStoppedSet {M : ℕ} + (hω : history O X Y M ω ∈ notStoppedSet S M) : + stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M ω = + sigmaHistory O X Y M ω := + stoppedProcess_eq_of_le (history_mem_notStoppedSet_iff.1 hω).le + +/-- If round `M` is played, the history stopped at the time `M + 1` is the history of the first +`M + 1` rounds. -/ +lemma stoppedProcess_sigmaHistory_succ_of_mem_notStoppedSet {M : ℕ} + (hω : history O X Y M ω ∈ notStoppedSet S M) : + stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) (M + 1) ω = + sigmaHistory O X Y (M + 1) ω := by + refine stoppedProcess_eq_of_le ?_ + have h_lt := history_mem_notStoppedSet_iff.1 hω + exact_mod_cast Order.add_one_le_of_lt (α := ℕ∞) h_lt + +/-- If round `M` is not played, the history stopped at the time `M + 1` is the history stopped at +the time `M`. -/ +lemma stoppedProcess_sigmaHistory_succ_of_notMem_notStoppedSet {M : ℕ} + (hω : history O X Y M ω ∉ notStoppedSet S M) : + stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) (M + 1) ω = + stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M ω := by + have h_le : hittingAfter (sigmaHistory O X Y) S 0 ω ≤ M := + not_lt.1 (history_mem_notStoppedSet_iff.not.1 hω) + rw [stoppedProcess_eq_of_ge (i := M) h_le, + stoppedProcess_eq_of_ge (i := M + 1) (h_le.trans (by simp))] + +/-- If round `M` is not played, the history stopped at the time `M` is not a history of `M` rounds +in `notStoppedSet S M`. -/ +lemma stoppedProcess_sigmaHistory_notMem_image_notStoppedSet {M : ℕ} + (hω : history O X Y M ω ∉ notStoppedSet S M) : + stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M ω ∉ + Sigma.mk M '' notStoppedSet S M := by + have h_le : hittingAfter (sigmaHistory O X Y) S 0 ω ≤ M := + not_lt.1 (history_mem_notStoppedSet_iff.not.1 hω) + obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 (h_le.trans_lt (WithTop.coe_lt_top M)).ne + rw [stoppedProcess_eq_of_ge (i := M) h_le, ← hk] + simp only [WithTop.untopA, WithTop.untopD_coe, sigmaHistory_apply] + rintro ⟨x, hx, hxk⟩ + -- The rule `S` stops after exactly `M` rounds, so the history of these rounds lies outside + -- `notStoppedSet S M`. + obtain ⟨rfl, hx'⟩ := Sigma.mk.inj_iff.1 hxk + exact hω (eq_of_heq hx' ▸ hx) + +variable {P : Measure Ω} + +/-- The law of the history stopped at the time `M` is the sum of its restriction to the event +that round `M` is not played and of the image by `Sigma.mk M` of the law of the history of the +first `M` rounds, restricted to `notStoppedSet S M`. -/ +lemma map_stoppedProcess_sigmaHistory_eq_add (hO : ∀ n, Measurable (O n)) + (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) (hS : MeasurableSet S) (M : ℕ) : + P.map (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M) = + (P.restrict (history O X Y M ⁻¹' notStoppedSet S M)ᶜ).map + (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M) + + ((P.map (history O X Y M)).restrict (notStoppedSet S M)).map (Sigma.mk M) := by + have hH := measurable_history hO hX hY M + have hE : MeasurableSet (history O X Y M ⁻¹' notStoppedSet S M) := + hH (measurableSet_notStoppedSet hS M) + have hm := measurable_stoppedProcess_sigmaHistory hO hX hY + (measurable_hittingAfter_sigmaHistory hO hX hY hS) M + conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) hE, Measure.map_add _ _ hm] + rw [add_comm, Measure.restrict_map hH (measurableSet_notStoppedSet hS M), + Measure.map_map (measurable_sigmaMk M) hH] + congr 1 + refine Measure.map_congr ((ae_restrict_iff' hE).2 (.of_forall fun ω hω ↦ ?_)) + exact stoppedProcess_sigmaHistory_of_mem_notStoppedSet hω + +/-- The law of the history stopped at the time `M + 1` is the sum of the restriction to the event +that round `M` is not played of the law of the history stopped at the time `M`, and of the image +by `Sigma.mk (M + 1)` of the law of the history of the first `M + 1` rounds on the event that +round `M` is played. -/ +lemma map_stoppedProcess_sigmaHistory_succ_eq_add (hO : ∀ n, Measurable (O n)) + (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) (hS : MeasurableSet S) (M : ℕ) : + P.map (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) (M + 1)) = + (P.restrict (history O X Y M ⁻¹' notStoppedSet S M)ᶜ).map + (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M) + + ((P.restrict (history O X Y M ⁻¹' notStoppedSet S M)).map (history O X Y (M + 1))).map + (Sigma.mk (M + 1)) := by + have hE : MeasurableSet (history O X Y M ⁻¹' notStoppedSet S M) := + measurable_history hO hX hY M (measurableSet_notStoppedSet hS M) + have hm := measurable_stoppedProcess_sigmaHistory hO hX hY + (measurable_hittingAfter_sigmaHistory hO hX hY hS) (M + 1) + conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) hE, Measure.map_add _ _ hm] + rw [add_comm, Measure.map_map (measurable_sigmaMk (M + 1)) (measurable_history hO hX hY _)] + congr 1 + · refine Measure.map_congr ((ae_restrict_iff' hE.compl).2 (.of_forall fun ω hω ↦ ?_)) + exact stoppedProcess_sigmaHistory_succ_of_notMem_notStoppedSet hω + · refine Measure.map_congr ((ae_restrict_iff' hE).2 (.of_forall fun ω hω ↦ ?_)) + exact stoppedProcess_sigmaHistory_succ_of_mem_notStoppedSet hω + +/-- On the event that round `M` is not played, the history stopped at the time `M` is not a +history of `M` rounds in `notStoppedSet S M`. -/ +lemma map_restrict_stoppedProcess_sigmaHistory_apply_image_notStoppedSet + (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) + (hS : MeasurableSet S) (M : ℕ) : + (P.restrict (history O X Y M ⁻¹' notStoppedSet S M)ᶜ).map + (stoppedProcess (sigmaHistory O X Y) (hittingAfter (sigmaHistory O X Y) S 0) M) + (Sigma.mk M '' notStoppedSet S M) = 0 := by + have hm := measurable_stoppedProcess_sigmaHistory hO hX hY + (measurable_hittingAfter_sigmaHistory hO hX hY hS) M + have hT : MeasurableSet (Sigma.mk M '' notStoppedSet S M) := + (measurableEmbedding_sigmaMk M).measurableSet_image.2 (measurableSet_notStoppedSet hS M) + rw [Measure.map_apply hm hT, Measure.restrict_apply (hm hT)] + refine measure_mono_null (fun ω hω ↦ ?_) measure_empty + exact stoppedProcess_sigmaHistory_notMem_image_notStoppedSet hω.2 hω.1 + +/-- The history stopped at the time `M` has at most `M` rounds. -/ +lemma map_stoppedProcess_sigmaHistory_apply_compl_fst_le (hO : ∀ n, Measurable (O n)) + (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) {τ : Ω → WithTop ℕ} + (hτ : Measurable τ) (M : ℕ) : + P.map (stoppedProcess (sigmaHistory O X Y) τ M) {x | x.1 ≤ M}ᶜ = 0 := by + have hm := measurable_stoppedProcess_sigmaHistory hO hX hY hτ M + rw [Measure.map_apply hm (measurableSet_sigma_fst_le M).compl] + refine measure_mono_null (fun ω hω ↦ hω ?_) measure_empty + exact (fst_sigmaHistory _ ω).trans_le (WithTop.untopA_le (min_le_left _ _)) + +/-- On the event that the history of the first `M` rounds lies in a measurable set `s`, the law of +the history of the first `M + 1` rounds is the composition-product of the restriction to `s` of +the law of the history of the first `M` rounds with the step kernel of round `M`, read as a +history of `M + 1` rounds. -/ +lemma IsAlgEnvSeq.map_restrict_history_succ {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} + [IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) {M : ℕ} {s : Set (Hist 𝓞 𝓐 𝓨 M)} + (hs : MeasurableSet s) : + (P.restrict (history O X Y M ⁻¹' s)).map (history O X Y (M + 1)) = + ((P.map (history O X Y M)).restrict s ⊗ₘ stepKernel alg env M).map + (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm := by + rw [history_succ, ← Measure.map_map (MeasurableEquiv.finSuccProd _ M).symm.measurable + ((h.measurable_history M).prodMk (h.measurable_step M)), + ((h.hasCondDistrib_step M).restrict_preimage hs).map_eq, + Measure.restrict_map (h.measurable_history M) hs] + +end StoppedAtTime + end Learning