[RemyDegenne]

This PR adds to LMLExplore/Probability/HasCondDistrib.lean the integrals and conditional expectations against a given conditional distribution HasCondDistrib Y X κ P, together with two constructions of conditional distributions. Episodic Markov arguments need these, on spaces where Mathlib's condDistrib (standard Borel) does not apply:

• hasCondDistrib_iff_forall_lintegral_eq: κ is the conditional distribution of Y given X iff ∫⁻ g(X, Y) dP = ∫⁻ ∫⁻ g(X, y) dκ(X) dP for every measurable g ≥ 0. The forward direction is the existing lintegral_comp_prodMk_eq_lintegral_lintegral;
• HasCondDistrib.integral_comp_prodMk_eq_integral_integral: the Bochner form, for g integrable for P.map X ⊗ₘ κ, valued in any real normed space;
• HasCondDistrib.condExp_prod_ae_eq_integral: P[g(X, Y) | σ(X)] =ᵐ ∫ g(X, y) dκ(X) for integrable g valued in a Banach space. Unlike Mathlib's condExp_prod_ae_eq_integral_condDistrib' and LML's HasCondDistrib.condExp_comp_ae_eq, it needs no standard Borel assumption, and it allows functions of (X, Y) (not only of Y);
• hasCondDistrib_compProd_of_forall_sectR: if Y has conditional distribution η (a, ·) given X under every κ a, then under μ ⊗ₘ κ it has conditional distribution η given (fst, X ∘ snd). It is proved through the new characterization;
• HasCondDistrib.of_comp_hasLaw: the converse of LML's HasCondDistrib.comp_hasLaw. A conditional distribution of Y ∘ f given X ∘ f under P is one of Y given X under the law of f.

Target: ReinforcementLearning, Layer 7.7 "Episodes as rounds" (statesEnv M H μ and episodeEnv M H μ, not yet on main), and through it Layer 14.2 "Visits and stream models". This PR supplies prerequisites of both; it adds none of their statements. The path from each lemma:

• 7.7 defines statesEnv (and episodeEnv) as the stationaryEnv of the kernel from H-step policies to the law of the state sequence (and rewards) of an episode, and proves that forgetting the rewards maps one episode law to the other and that a stochastic Markov policy has the episode law of a random H-step policy. These are statements about the joint law of the H steps of an episode, built step by step: the next state has conditional distribution P_h(s, a) given the steps so far. hasCondDistrib_compProd_of_forall_sectR glues these per-step conditional distributions over the composition-product μ ⊗ₘ κ that forms the episode law; HasCondDistrib.of_comp_hasLaw transports the conditional distribution of the trajectory of M.augmented (a run of M.env) to the episode law, the law of the state-sequence map; hasCondDistrib_iff_forall_lintegral_eq is how both the gluing and the comparison of episode laws are proved. In the source paper project this is hasCondDistrib_shiftRounds_stepLaw (MarkovDecisionProcess/Episodic/StepLaw.lean, the paper's item R6).
• 14.2 proves the stream representation in statesEnv: the next state of each visit of (h, s, a) is a draw of law P_h(s, a) given the past. Its proofs compute integrals and conditional expectations of functions of (visit, next state) against these conditional distributions, on the finite but not otherwise structured spaces of statesEnv, where Mathlib's condDistrib would need a standard Borel assumption: HasCondDistrib.integral_comp_prodMk_eq_integral_integral and HasCondDistrib.condExp_prod_ae_eq_integral. In the source these are integral_mul_obs_succ_stepLaw (R6) and Visits.lean, VisitConcentration.lean (item R11).

Layer 7.6 "Episodic values" is already on main; an earlier version of this description named it as the target by mistake.

Generality, relative to the source: the Bochner identity and the conditional expectation take integrability for the joint law instead of strong measurability, a bound, or real values. The characterization takes an s-finite measure instead of a finite one. The gluing takes an s-finite kernel κ instead of a Markov one. The transport needs only almost-everywhere measurability. The source's HasCondDistrib.restrict_preimage (also in the item) is not included: PR #288 has already added it to this file on main. The additions sit at the end of the existing sections and in two new sections at the end of the file. The proofs use Mathlib's HasLaw.integral_comp and HasLaw.integrable_comp for the joint law, and one new lemma, MeasureTheory.Integrable.integral_measure_compProd in LMLExplore/Probability/Kernel/Composition/IntegralCompProd.lean: the measure form Integrable g (μ ⊗ₘ κ) → Integrable (fun a ↦ ∫ b, g (a, b) ∂κ a) μ of Mathlib's kernel-level Integrable.integral_compProd, used by both integral lemmas. No public declaration is removed or renamed.

Source: adapted from the paper project RemyDegenne/Essakine2026Tight at commit afce796e30222b744d6cef85899b2e81f06e3fc7 (Apache 2.0), files Essakine2026Tight/ForLMLExplore/Probability/HasCondDistribIntegral.lean, HasCondDistribCondExp.lean and CondDistrib.lean. The module docstring credits it.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R4

🤖 Prepared with Claude Code

[lmlexplore-automation]

⚠️ This PR no longer merges into main. Rebase it onto current main (or merge main into it) and push — nothing downstream can make progress until then, since a green build and an approving review on this head still cannot merge.

Do check what the conflict actually is before resolving it mechanically. If main has since landed its own version of something this PR adds, part of it may be superseded, and the right answer is to drop that part — or close the PR — rather than to reconcile the text. That is an authoring decision.

[RemyDegenne]

✅ scope — now passing on 5db0008.

[RemyDegenne]

Agreed: Layer 7.6 is already on main, so it was the wrong target. Commit 5db0008 leaves the code unchanged in scope, and the PR description now names ReinforcementLearning Layer 7.7 "Episodes as rounds" (statesEnv M H μ / episodeEnv M H μ, not on main: grep -rn 'statesEnv\|episodeEnv' LMLExplore finds nothing), and through it Layer 14.2 "Visits and stream models". The path from each lemma:

• 7.7 is about the joint law of the H steps of an episode: statesEnv is the stationaryEnv of the kernel from H-step policies to the law of the episode's state sequence, plus the comparisons "forgetting rewards maps episodeEnv episode laws to statesEnv ones" and "a stochastic Markov policy has the episode law of the random H-step policy". That law is built step by step, where the next state has conditional distribution P_h(s, a) given the earlier steps. hasCondDistrib_compProd_of_forall_sectR glues the per-step conditional distributions over the composition-product μ ⊗ₘ κ that forms the episode law. HasCondDistrib.of_comp_hasLaw transports the conditional distribution of the M.augmented trajectory to the episode law, which is the law of the state-sequence map. hasCondDistrib_iff_forall_lintegral_eq proves both of these and the comparison of episode laws. (Source: hasCondDistrib_shiftRounds_stepLaw, paper item R6.)
• 14.2: the stream representation in statesEnv (the next state of each visit of (h, s, a) has law P_h(s, a) given the past) takes integrals and conditional expectations of functions of (visit, next state) against these conditional distributions, with no standard Borel structure available: HasCondDistrib.integral_comp_prodMk_eq_integral_integral and HasCondDistrib.condExp_prod_ae_eq_integral. (Source: integral_mul_obs_succ_stepLaw (R6), Visits.lean / VisitConcentration.lean (R11).)

The Roadmap: ReinforcementLearning line is unchanged.

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

The proofs are short and robust, but the same integrability step is proved twice in a row by unfolding Measure.compProd into the kernel compProd and closing with simpa, instead of through one shared measure-level lemma.

• LMLExplore/Probability/HasCondDistrib.lean:137 — hg' (integrability of x ↦ ∫ y, g (x, y) ∂κ x under P.map X) is proved by rw [Measure.compProd] at hg; simpa using hg.integral_compProd. This unfolds the measure compProd into the kernel κ ⊗ₖ η form and depends on simp removing the prodMkLeft/const wrappers. The same two lines are repeated verbatim at line 249 in condExp_prod_ae_eq_integral. Fix: Add a reusable lemma MeasureTheory.Integrable.integral_measure_compProd [SFinite μ] [IsSFiniteKernel κ] (hf : Integrable f (μ ⊗ₘ κ)) : Integrable (fun x ↦ ∫ y, f (x, y) ∂κ x) μ in LMLExplore/Probability/Kernel/Composition/IntegralCompProd.lean. Prove it once, e.g. like Mathlib's Measure.integrable_compProd_iff via simp_rw [Measure.compProd, ...], and use it at both sites.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 36s · 73.6k in (68.8k cache read, 4.8k cache write) / 2.2k out tokens · reviewing this diff · rubric}

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	All six new statements are faithful to the mathematics: the characterization, the Bochner identity, the conditional expectation given σ(X), the gluing, the transport, and integrability of the inner integral. None is vacuous and no hypothesis carries the claim's content.
✅	reuse	approved	claude/claude-opus-5-5	Both earlier findings are fixed: the proofs now use Mathlib's HasLaw.integral_comp and HasLaw.integrable_comp through h.integral_comp and h.integrable_comp. None of the new declarations (lintegral characterization, Bochner identity, condExp without standard Borel, gluing, transport, measure-form Integrable.integral_measure_compProd) has a counterpart in Mathlib (HasCondDistrib.lean, CondDistrib.lean, Kernel/Composition/IntegralCompProd.lean) or LMLExplore.
✅	scope	approved	claude/claude-opus-5-5	The PR is one topic: an API for integrals, conditional expectations, gluing and transport against a given HasCondDistrib. It now names targets that are on the roadmap and not yet on main, ReinforcementLearning Layer 7.7 (episode laws of statesEnv/episodeEnv, built step by step on finite non-standard-Borel spaces) and Layer 14.2 (stream models in statesEnv), and gives a concrete path to each, which resolves the prior finding.
✅	attribution	approved	claude/claude-opus-5-5	The module docstring credits RemyDegenne/Essakine2026Tight (Apache 2.0, with the three source files) for every adapted declaration, which matches the PR description. The new helper Integrable.integral_measure_compProd is a routine wrapper whose docstring names Mathlib's Integrable.integral_compProd, and the file does not credit the roadmap.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds public, reusable lemmas about HasCondDistrib and one general measure-level integrability lemma in its canonical file, with no new definitions, exposed bodies or compatibility layer. The new infrastructure lemma does not duplicate Mathlib, and none of the statements is a normal-form @[simp] or @[grind] candidate.
✅	generality	approved	claude/claude-opus-5-5	Each new declaration's assumptions are no stronger than the Mathlib lemmas it is built on need: s-finite measure and kernel, integrability for the joint law, measurable X with a finite measure for the conditional expectation, and a.e.-measurability for the transport. No special case is proved separately from its general form, and nothing is generalized beyond what the target needs.
✅	placement	approved	claude/claude-opus-5-5	The five new HasCondDistrib lemmas are general and belong in LMLExplore/Probability/HasCondDistrib.lean, and Integrable.integral_measure_compProd sits in the IntegralCompProd file that mirrors its Mathlib source. The one new import (IntegralCompProd into HasCondDistrib) is used at lines 142 and 245.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard terminology, consistent with the adjacent lintegral_comp_prodMk_eq_lintegral_lintegral, hasCondDistrib_snd_compProd_comap, comp_hasLaw, and Mathlib's condExp_prod_ae_eq_integral_condDistrib' and Integrable.integral_compProd; _iff is a genuine Iff, namespaces support dot notation, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The updated module docstrings and every new public lemma are documented accurately, with hypotheses and conclusions matching the statements, sources credited, and no roadmap or process narrative in the files. The claimed relation to LML's condExp_comp_ae_eq could not be checked because LML's source is not in the checkout.
✅	proof-quality	approved	claude/claude-opus-5-5	The repeated unfolding of Measure.compProd is now one reusable lemma, Integrable.integral_measure_compProd, used by both integral lemmas. The remaining proofs are short, robust and free of undocumented definitional equality.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 5db0008. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.64.}