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

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 not ported; its uses are inlined as Mathlib's Convex.integral_mem.
• 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 25 declarations.
• The local environment lint passed.

Paper: RemyDegenne/Essakine2026Tight
Item: R23

🤖 Prepared with Claude Code