[RemyDegenne]

This PR proves that the chain rule for the Kullback–Leibler divergence at a stopping time is an equality when the hitting time of the stopping rule is almost surely finite under both algorithm-environment pairs. It targets Identification, Layer 2.1, "Divergence decomposition at a stopping time": the first bullet's "with equality when τ is also almost surely finite under the second pair" for any two pairs (alg, env), (alg', env'), and the third bullet's equality KL = ∑ a, E_ν[N_a(τ)] KL(ν_a, ν'_a) for one algorithm against two stationary bandits. LMLExplore already had the inequalities (Learning.klDiv_stoppedHistMeasure_le_tsum, _le_lintegral, _le). The equalities are stated in the same shape, with stoppedHistMeasure and notStoppedSet. After this PR, Layer 2.1 lacks only the joint law of the stopped history and the output for two arbitrary pairs; LMLExplore states it only for one algorithm against two bandits (klDiv_histOutputMeasure_le).

Roadmap: Identification

The proof of the converse goes through the chain rule at a bounded stopping time, which holds with no finiteness assumption. Learning.IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory says that for any two algorithm-environment sequences, on any probability spaces, the divergence between the laws of the histories stopped at a fixed time M, the histories of the first min M τ rounds, equals ∑ t < M, KL(μ_t ⊗ₘ stepKernel alg env t ‖ μ_t ⊗ₘ stepKernel alg' env' t). Here μ_t is the law of the t-round history restricted to notStoppedSet S t. It is proved by induction on M. The laws of the histories stopped at M and at M + 1 split, according to whether round M is played, into parts with disjoint supports (LML's klDiv_add_add_of_measure_eq_zero), and Mathlib's klDiv_compProd_eq_add handles the step of round M. When τ is almost surely finite under both pairs, the history stopped at M is the truncation truncHist M of the stopped history. Data processing then bounds every partial sum by the divergence of the stopped histories, which gives the converse of klDiv_stoppedHistMeasure_le_tsum.

New declarations:

• LMLExplore/SequentialLearning/DivergenceDecomposition.lean: Learning.IsAlgEnvSeq.klDiv_map_stoppedProcess_sigmaHistory, Learning.klDiv_stoppedHistMeasure_eq_tsum, Learning.klDiv_stoppedHistMeasure_eq_lintegral and Learning.klDiv_stoppedHistMeasure_eq. The existing _le_lintegral and _le now share with them two private series identities instead of repeating the computation. Their statements are unchanged.
• LMLExplore/SequentialLearning/StoppedHistory.lean adds the histories stopped at a fixed time:
  • Learning.truncHist, built on Mathlib's Fin.take, with truncHist_def, measurable_truncHist, truncHist_sigmaHistory and truncHist_stoppedValue_sigmaHistory;
  • measurable_stoppedProcess_sigmaHistory, map_stoppedProcess_sigmaHistory_eq_map_truncHist and stoppedProcess_sigmaHistory_zero;
  • the pointwise lemmas stoppedProcess_sigmaHistory_{of,succ_of}_mem_notStoppedSet, stoppedProcess_sigmaHistory_succ_of_notMem_notStoppedSet and stoppedProcess_sigmaHistory_notMem_image_notStoppedSet;
  • the law splits map_stoppedProcess_sigmaHistory_eq_add and map_stoppedProcess_sigmaHistory_succ_eq_add, the support lemmas map_restrict_stoppedProcess_sigmaHistory_apply_image_notStoppedSet and map_stoppedProcess_sigmaHistory_apply_compl_fst_le, and IsAlgEnvSeq.map_restrict_history_succ.
• LMLExplore/Probability/HasCondDistrib.lean: ProbabilityTheory.HasCondDistrib.restrict_preimage, which says a conditional law given X survives restricting the measure to an event X ⁻¹' s.

No public declaration is removed or renamed.

This is a port of item R19 of the paper project RemyDegenne/Essakine2026Tight, at commit 73a8c16c42ec1c41f8d38c5d2af232f36c2cff15, under the Apache 2.0 license. It adapts ForLMLExplore/InformationTheory/KLStoppedPrefix.lean, ForLMLExplore/Probability/Process/SigmaPrefix.lean and ForLMLExplore/SequentialLearning/DivergenceDecomposition.lean, and HasCondDistrib.restrict_preimage from ForLMLExplore/Probability/CondDistrib.lean (item R4, the prerequisite that R19 uses). The source proves the chain rule for a general process along its prefix filtration, through new finPrefix/sigmaPrefix/prefixFiltration/piFinSuccProd APIs. This port specializes the argument to LMLExplore's sigmaHistory, notStoppedSet and LML's history_succ/finSuccProd, so it does not add a parallel API for prefixes of histories. It gets the converse inequality from the existing klDiv_stoppedHistMeasure_le_tsum and data processing through the truncation, so it does not need monotone convergence. It also states the result for two arbitrary pairs (alg, env), (alg', env'), as Layer 2.1 asks, where the source has one algorithm against two environments. The files credit the source. Mathematical references: [KCG16, Lemma 1], [GMS19, Section 2], already cited in DivergenceDecomposition.lean.

Paper: RemyDegenne/Essakine2026Tight
Item: R19

🤖 Prepared with Claude Code