[RemyDegenne]

This PR adds the transport of means and variances under a Kullback–Leibler constraint, the tools "the KL-to-Bernstein transport" and "the variance transfers [MDJKLV21, Lemmas 10–12]" of RF-Express: if KL(μ ‖ ν) ≤ a and f has values in [c, d], then |∫ f ∂μ - ∫ f ∂ν| ≤ √(2 Var_ν(f) a) + (d - c) a / 3, Var_ν(f) ≤ 2 Var_μ(f) + (8/3)(d - c)² a and Var_μ(f) ≤ 2 Var_ν(f) + (5/6)(d - c)² a. It also adds the two variance transports of [MDJKLV21, Lemma 12] that use no KL constraint.

Roadmap: ReinforcementLearning

The target is ReinforcementLearning Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]), whose list of tools includes "the KL-to-Bernstein transport: if KL(p,q) ≤ α and f ∈ [0,b], then |pf − qf| ≤ √(2Var_q(f)α) + (2/3)bα" and "the variance transfers [MDJKLV21, Lemmas 10–12]". The case c = 0, d = b of abs_integral_sub_integral_le_of_klDiv_le gives the roadmap's bound with b α / 3 in place of 2 b α / 3. After this PR, Layer 19.2 still needs counts versus pseudo-counts, Lemma 9 (∑_t u_{t+1}/max(1, U_t) ≤ 4 log(U_{T+1} + 1)), the inversion of Lemma 13 (open in #287), and then the algorithm with its PAC and sample-complexity theorem.

The constants are sharper than in the sources, and I checked them by hand. [MDJKLV21, Lemma 10] (after [TM18]) bounds the positive root of 2α(V + D/3) − D² ≥ 0 by √(2Vα) + 2α/3. Here, Chernoff's choice t = r / (v + b r / 3), with r = √(2 v a), in the sub-gamma bound exp x − 1 − x ≤ x² / (2(1 − x/3)) gives √(2 v a) + b a / 3 directly. This is the inversion from the high-probability Bernstein inequality [BLM13, Theorem 2.10] that LMLExplore already has in Probability/Moments/Bernstein.lean. The variance transports follow from it with (8/3) and (5/6) in place of 4 [MDJKLV21, Lemma 11], and the finite-space transport has the factor 1/2 in place of 3 [MDJKLV21, Lemma 12], because the constant (d − c)²/2 can be subtracted under ∑ (ν{x} − μ{x}) = 0. The one-sided transport only needs f ≤ ∫ f ∂ν + b ν-a.e., MemLp f 2 ν and Integrable f μ. The bound b ≥ 0 follows from these, and b = 0 is handled as a limit. The two-sided statements take f in any interval [c, d], not just [0, b].

New declarations:

• LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean (new file, namespace LMLExplore):

  • integral_sub_integral_le_of_klDiv_le (one-sided)
  • abs_integral_sub_integral_le_of_klDiv_le [TM18], [MDJKLV21, Lemma 10]
  • variance_le_two_mul_variance_add_of_klDiv_le and variance_le_two_mul_variance_add_of_klDiv_le' [MDJKLV21, Lemma 11]
  • three private proof steps: the Donsker–Varadhan inequality with Bennett's bound at every t ≥ 0, the case b > 0, and the specialisation to g ∈ [0, B] with Var_ν(g) ≤ B ∫ g ∂ν

• LMLExplore/Probability/Moments/Variance.lean (namespace ProbabilityTheory):

  • variance_le_integral_sub_sq: Var[X] ≤ ∫ (X − c)²
  • variance_le_mul_integral_sub: X ∈ [c, d] gives Var[X] ≤ (d − c)(𝔼X − c), a weakening of Mathlib's Bhatia–Davis variance_le_sub_mul_sub
  • variance_le_two_mul_variance_add_mul_integral_abs_sub: |X − Y| ≤ D gives Var[X] ≤ 2Var[Y] + 2D𝔼|X − Y|
  • variance_le_variance_add_mul_sum_abs_sub: on a finite space, Var_ν(f) ≤ Var_μ(f) + (d − c)²/2 ∑|μ{x} − ν{x}|

• LMLExplore/Analysis/SpecialFunctions/Exp.lean: Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub, the closed-form inversion of the sub-gamma bound at Chernoff's t = r / (v + b r / 3). It is shared with measureReal_sqrt_add_le_sum_le_of_ae_le in Probability/Moments/Bernstein.lean, whose proof now uses it in place of its own copy of the inversion.

• LMLExplore/Analysis/Convex/Integral.lean: MeasureTheory.integral_mem_Icc_of_ae_mem_Icc, the mean of a function with values in [l, u] a.e. lies in [l, u]. The existing integral_id_mem_Icc_of_ae_mem_Icc is now its special case.

• LMLExplore/Algebra/Order/Ring/Abs.lean (new file): sq_sub_mem_Icc_of_mem_Icc, x, y ∈ [c, d] gives (x - y) ^ 2 ∈ [0, (d - c) ^ 2].

The proofs reuse:

• Tau Ceti's TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv
• LMLExplore's MeasureTheory.MemLp.mgf_le_exp_mul_exp_sub_one_sub_of_ae_le and Real.exp_sub_one_sub_id_le_sq_div
• Mathlib's variance_le_expectation_sq, variance_le_sub_mul_sub, Convex.integral_mem and klDiv_eq_zero_iff

No declaration is removed or renamed.

Source: this PR ports item R23 of the paper project RemyDegenne/Essakine2026Tight, at commit 520dd39a55fa4e9a62a4a2d51f48163926176a5d (Apache-2.0). The source files are Essakine2026Tight/ForLMLExplore/InformationTheory/KLBernstein.lean and Essakine2026Tight/ForLMLExplore/Probability/Moments/VarianceTransport.lean. Changes from the source:

• The main proof is new. It inverts the sub-gamma bound in closed form and does not use the source's Poisson Cramér transform (Real.poissonCramer, Real.expSubOneSub, item R26, which is not a ReinforcementLearning target), nor the AM–GM helpers of Analysis/Real/Sqrt.lean.
• The constants are sharper, as described above.
• The statements are generalised from [0, b] to [c, d], and the one-sided transport to functions bounded above.
• The source's integral_mem_Icc_of_ae_mem_Icc (item R8) is added, under the same name, in Analysis/Convex/Integral.lean.
• The general variance facts go into the existing Probability/Moments/Variance.lean rather than a new file.

Local checks (not CI):

• lake build --iofail is green.
• The local changed-module axiom check found 0 violations in 87 declarations across 6 modules.
• The local environment lint passed.

Paper: RemyDegenne/Essakine2026Tight
Item: R23

🤖 Generated with Claude Code

[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.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	All new statements check out by hand with the stated constants: the one- and two-sided KL mean transports, the 8/3 and 5/6 variance transports, both Lemma 12 transports, the sub-gamma inversion and the interval helpers. The hypotheses are not vacuous, and the new variance lemmas sit in the IsProbabilityMeasure section that variance_le_expectation_sq requires.
✅	reuse	approved	claude/claude-opus-5-5	Both the KL transport and measureReal_sqrt_add_le_sum_le_of_ae_le now use the shared Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub, and the redundant absolutelyContinuous_of_klDiv_ne_top is gone in favour of klDiv_ne_top_iff. No Mathlib or LMLExplore declaration already provides integral_mem_Icc_of_ae_mem_Icc, variance_le_integral_sub_sq, variance_le_mul_integral_sub, sq_sub_mem_Icc_of_mem_Icc or the KL and variance transports; they reuse variance_le_expectation_sq, variance_le_sub_mul_sub, Convex.integral_mem and TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv.
✅	scope	approved	claude/claude-opus-5-5	The new material proves two tools that ReinforcementLearning Layer 19.2 (RF-Express) lists by name: the KL-to-Bernstein transport and the variance transfers of [MDJKLV21, Lemmas 10–12] (roadmap README lines 1664–1666). The edits to the Bernstein and convex-integral files only move into shared lemmas proofs the new work also uses, so the PR is one topic.
✅	attribution	approved	claude/claude-opus-5-5	Both ported Essakine2026Tight files are credited in the module docstrings of InformationTheory/KullbackLeibler/Bernstein.lean and Probability/Moments/Variance.lean, and [MDJKLV21], [TM18] and [BLM13] are cited at the declarations that follow them. The remaining helpers are routine and need no separate credit.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is the roadmap's KL-transport theorems, one closed-form sub-gamma inversion that Bernstein.lean now also uses, and general interval and variance lemmas in their canonical homes that do not duplicate Mathlib. The private helpers are specific to the Donsker–Varadhan argument, and the PR adds no definitions or compatibility layers.
✅	generality	approved	claude/claude-opus-5-5	The general one-sided KL transport comes first, and the two-sided and variance transports, the shared Chernoff inversion and the interval-mean lemma are all derived from general forms without duplication. The over-assuming public lemma from the prior round is gone, and no remaining hypothesis is unused or stronger than Mathlib convention.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration lives in its topical home (KL transports in InformationTheory/KullbackLeibler/, general variance facts in Probability/Moments/Variance.lean, the sub-gamma inversion in Exp.lean shared with Bernstein.lean, the interval lemmas in Analysis/Convex/Integral.lean and the Mathlib-mirroring Algebra/Order/Ring/Abs.lean). Every new import is used and none is overly broad.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, consistent with neighbouring declarations such as Mathlib's variance_le_sub_mul_sub, and none overstates its statement. Namespaces are appropriate and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Every new file has a module docstring and every new public declaration has an accurate docstring; constants, hypotheses and comparisons with the sources match the statements. The refactored docstrings in Convex/Integral.lean, Exp.lean, Moments/Bernstein.lean and Variance.lean are still correct.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, commented where the structure is non-obvious, free of change/show and defeq reliance, and Chernoff's inversion is now a shared lemma rather than duplicated; the prior hμν finding is withdrawn because the description no longer claims the missing lemma and each repeated line is a single term combining two Mathlib lemmas, whose wrapper the reuse review asked to delete.

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

_{Reviewing this diff at head 3311c92. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $4.05.}

[prevostad]

🟡 reuse — request_changes claude/claude-opus-5-5

The new transport and variance results are new and reuse Mathlib and LMLExplore API, including a shared Chernoff inversion for Bernstein. One public declaration is still a thin wrapper around Mathlib's klDiv_ne_top_iff.

• LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean:79 — absolutelyContinuous_of_klDiv_ne_top is a public wrapper whose whole proof is (klDiv_ne_top_iff.1 h).1. It is used at the three hμν sites (lines 158, 190, 216), and the module docstring (line 45) lists it as a main statement. Fix: Delete it and its docstring entry. At each site write (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1.

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 · 20s · 113k in (75.4k cache read, 37.6k cache write) / 1.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

Fixed in 3311c92. I deleted LMLExplore.absolutelyContinuous_of_klDiv_ne_top and removed its entry from the module docstring. The three hμν sites (abs_integral_sub_integral_le_of_klDiv_le and both variance transports) now use (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1, as suggested. The earlier generality finding, which turned the ≤ ofReal a form into the ≠ ∞ form, no longer applies because the declaration is gone. This head also merges current main (8280ba8), which fixes the merge conflict.

[prevostad]

AI review — changes requested

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.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
♻️	correctness	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
🟡	reuse	changes requested	claude/claude-opus-5-5	The new transport and variance results are new and reuse Mathlib and LMLExplore API, including a shared Chernoff inversion for Bernstein. One public declaration is still a thin wrapper around Mathlib's klDiv_ne_top_iff.
♻️	scope	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	attribution	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	api-design	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	generality	stale (re-run pending)	claude/claude-opus-5-5	The statements are at the natural level: the transports take any interval [c, d] (one-sided: f bounded above), the special cases are derived from shared general lemmas, and no hypothesis is unused or stronger than Mathlib convention.
♻️	placement	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	naming	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	documentation	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—
♻️	proof-quality	stale (re-run pending) (approved in @RemyDegenne's review of 2ed0443)	—

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

_{Reviewing this diff at head b6b7e54. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.84.}

[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.