From 5fbd6acc66ce04bad15e7a8c44668f0b54841d04 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 12:17:12 +0100 Subject: [PATCH 1/5] =?UTF-8?q?feat:=20transport=20of=20means=20and=20vari?= =?UTF-8?q?ances=20under=20a=20KL=20constraint=20[MDJKLV21,=20Lemmas=2010?= =?UTF-8?q?=E2=80=9312]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Code --- .../KullbackLeibler/Bernstein.lean | 245 ++++++++++++++++++ LMLExplore/Probability/Moments/Variance.lean | 103 ++++++++ 2 files changed, 348 insertions(+) create mode 100644 LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean new file mode 100644 index 00000000..a1855fce --- /dev/null +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -0,0 +1,245 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.Moments.Variance +import Mathlib.Analysis.Convex.Integral +import LMLExplore.Analysis.SpecialFunctions.Exp +import LMLExplore.Probability.Moments.Bernstein +import LMLExplore.Probability.Moments.Variance +import TauCeti.InformationTheory.KullbackLeibler.Variational + +/-! +# Transport of means and variances under a Kullback–Leibler constraint + +If `KL(μ ‖ ν) ≤ a`, the mean of a function under `μ` is close to its mean under `ν`, at a +Bernstein-type distance governed by the variance under `ν`: for `f` with values in an interval of +length `b`, +`|∫ f ∂μ - ∫ f ∂ν| ≤ √(2 Var_ν(f) a) + b a / 3`. +This is the form in which a confidence region `{p | KL(p̂ ‖ p) ≤ a}` around an empirical law `p̂` +controls the means of value functions, in the analysis of optimistic exploration algorithms. It +also transports variances: `Var_ν(f) ≤ 2 Var_μ(f) + (8 / 3) b² a` and +`Var_μ(f) ≤ 2 Var_ν(f) + (5 / 6) b² a`. + +The proof combines the Donsker–Varadhan inequality +`∫ g ∂μ - log ∫ exp g ∂ν ≤ KL(μ ‖ ν)` (Tau Ceti's +`TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv`), applied to `g = t (f - ∫ f ∂ν)`, with +Bennett's bound on the moment-generating function of the centred function +(`MeasureTheory.MemLp.mgf_le_exp_mul_exp_sub_one_sub_of_ae_le`). Its sub-gamma form +`exp x - 1 - x ≤ x² / (2 (1 - x / 3))` then inverts in closed form, as in the high-probability form +of Bernstein's inequality [BLM13, Theorem 2.10]. + +## Main statements + +* `LMLExplore.integral_sub_integral_le_of_klDiv_le`: the one-sided transport, for `f` bounded + above by its `ν`-mean plus `b`. +* `LMLExplore.abs_integral_sub_integral_le_of_klDiv_le`: the two-sided transport for `f` with + values in `[c, d]` [TM18], [MDJKLV21, Lemma 10]. +* `LMLExplore.variance_le_two_mul_variance_add_of_klDiv_le` and + `LMLExplore.variance_le_two_mul_variance_add_of_klDiv_le'`: the transport of variances + [MDJKLV21, Lemma 11]. + +The sources state the two-sided transport with `2 b a / 3` in place of `b a / 3`, and the +transport of variances with `4 b² a`; the constants here are sharper. + +## References + +* [BLM13] S. Boucheron, G. Lugosi and P. Massart, *Concentration Inequalities*, Oxford + University Press, 2013. +* [TM18] M. S. Talebi and O.-A. Maillard, *Variance-aware regret bounds for undiscounted + reinforcement learning in MDPs*, ALT 2018. +* [MDJKLV21] P. Ménard, O. D. Domingues, A. Jonsson, E. Kaufmann, E. Leurent and M. Valko, + *Fast active learning for pure exploration in reinforcement learning*, ICML 2021. +-/ + +public section + +open MeasureTheory ProbabilityTheory InformationTheory Real + +open scoped ENNReal + +namespace LMLExplore + +variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} [IsProbabilityMeasure μ] + [IsProbabilityMeasure ν] {f : α → ℝ} {a b c d : ℝ} + +/-- The Donsker–Varadhan inequality at `g = t (f - ∫ f ∂ν)`, with Bennett's bound on the +moment-generating function: for every `t ≥ 0`, +`t (∫ f ∂μ - ∫ f ∂ν) - Var_ν(f) ψ_b(t) ≤ a`, with `ψ_b(t) = (exp (t b) - 1 - t b) / b²`. -/ +private lemma mul_sub_le_of_klDiv_le (hfν : MemLp f 2 ν) (hfμ : Integrable f μ) (hb : 0 < b) + (hfb : ∀ᵐ x ∂ν, f x - ν[f] ≤ b) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) {t : ℝ} + (ht : 0 ≤ t) : + t * (∫ x, f x ∂μ - ∫ x, f x ∂ν) - Var[f; ν] * ((exp (t * b) - 1 - t * b) / b ^ 2) ≤ a := by + set Y := fun x ↦ f x - ν[f] + have hY : MemLp Y 2 ν := hfν.sub (memLp_const _) + have hmean : ν[Y] = 0 := by + simp [Y, integral_sub (hfν.integrable one_le_two) (integrable_const _)] + have hexp : Integrable (fun x ↦ exp (t * Y x)) ν := + integrable_exp_mul_of_le t b ht hY.aestronglyMeasurable.aemeasurable hfb + have hmgf := hY.mgf_le_exp_mul_exp_sub_one_sub_of_ae_le hmean.le hb hfb ht + rw [← variance_eq_integral hfν.aestronglyMeasurable.aemeasurable] at hmgf + have hDV := TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv (μ := μ) (ν := ν) + (f := fun x ↦ t * Y x) ((hfμ.sub (integrable_const _)).const_mul t) hexp + have hDV' : ∫ x, t * Y x ∂μ - log (mgf Y ν t) ≤ a := + (ENNReal.ofReal_le_ofReal_iff ha).1 (hDV.trans h) + have hint : ∫ x, t * Y x ∂μ = t * (∫ x, f x ∂μ - ∫ x, f x ∂ν) := by + simp [Y, integral_const_mul, integral_sub hfμ (integrable_const _)] + have hlog := (log_le_log (mgf_pos hexp) hmgf).trans_eq (log_exp _) + linarith + +/-- `integral_sub_integral_le_of_klDiv_le` for `b > 0`. -/ +private lemma integral_sub_integral_le_of_klDiv_le_of_pos (hfν : MemLp f 2 ν) + (hfμ : Integrable f μ) (hb : 0 < b) (hfb : ∀ᵐ x ∂ν, f x - ν[f] ≤ b) (ha : 0 ≤ a) + (h : klDiv μ ν ≤ ENNReal.ofReal a) : + ∫ x, f x ∂μ - ∫ x, f x ∂ν ≤ √(2 * Var[f; ν] * a) + b * a / 3 := by + set D := ∫ x, f x ∂μ - ∫ x, f x ∂ν + set v := Var[f; ν] + have key {t : ℝ} (ht : 0 ≤ t) := mul_sub_le_of_klDiv_le hfν hfμ hb hfb ha h ht + rcases ha.eq_or_lt with rfl | ha' + · -- `KL(μ ‖ ν) = 0` forces `μ = ν` + have hμν : μ = ν := klDiv_eq_zero_iff.1 (le_antisymm (by simpa using h) zero_le) + simp [D, hμν] + rcases (variance_nonneg f ν).eq_or_lt with hv | hv + · -- zero variance: `t D ≤ a` for every `t ≥ 0`, so `D ≤ 0` + by_contra! hD + have hD0 : 0 < D := lt_of_le_of_lt (by positivity) hD + have := key (t := (a + 1) / D) (by positivity) + rw [← hv, div_mul_cancel₀ _ hD0.ne'] at this + linarith + -- Chernoff's choice `t = r / (v + b r / 3)` with `r = √(2 v a)`, at which the sub-gamma bound + -- `ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` makes `t (r + b a / 3) - v ψ_b(t)` at least `a` + set r := √(2 * v * a) + have hr : r ^ 2 = 2 * v * a := sq_sqrt (by positivity) + have hr0 : 0 < r := sqrt_pos.2 (by positivity) + obtain ⟨s, hs⟩ : ∃ s, s = v + b * r / 3 := ⟨_, rfl⟩ + have hs0 : 0 < s := by rw [hs]; positivity + obtain ⟨t, rfl⟩ : ∃ t, t = r / s := ⟨_, rfl⟩ + have ht : 0 < r / s := by positivity + have htb : r / s * b < 3 := by + rw [div_mul_eq_mul_div, div_lt_iff₀ hs0] + nlinarith + have hψ : (exp (r / s * b) - 1 - r / s * b) / b ^ 2 ≤ + (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by + calc (exp (r / s * b) - 1 - r / s * b) / b ^ 2 + ≤ (r / s * b) ^ 2 / (2 * (1 - r / s * b / 3)) / b ^ 2 := by + gcongr + exact exp_sub_one_sub_id_le_sq_div (by positivity) htb + _ = (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by field_simp + have h1 : 1 - r / s * b / 3 = v / s := by + field_simp + linear_combination 3 * hs + have hval : r / s * (r + b * a / 3) - v * ((r / s) ^ 2 / (2 * (1 - r / s * b / 3))) = a := by + have hv' : v ≠ 0 := hv.ne' + rw [h1] + field_simp + linear_combination 3 * hr - 6 * a * hs + have hkey := key ht.le + have : r / s * D ≤ r / s * (r + b * a / 3) := by nlinarith [mul_le_mul_of_nonneg_left hψ hv.le] + exact le_of_mul_le_mul_left this ht + +/-- **Transport of the mean under a Kullback–Leibler constraint**, one-sided form: if +`KL(μ ‖ ν) ≤ a` and `f ≤ ∫ f ∂ν + b` holds `ν`-almost everywhere, then +`∫ f ∂μ - ∫ f ∂ν ≤ √(2 Var_ν(f) a) + b a / 3`. -/ +theorem integral_sub_integral_le_of_klDiv_le (hfν : MemLp f 2 ν) (hfμ : Integrable f μ) + (hfb : ∀ᵐ x ∂ν, f x - ν[f] ≤ b) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : + ∫ x, f x ∂μ - ∫ x, f x ∂ν ≤ √(2 * Var[f; ν] * a) + b * a / 3 := by + -- the bound `b` is nonnegative, as `f - ∫ f ∂ν` has mean zero + have hb : 0 ≤ b := by + have hint := integral_mono_ae (hfν.integrable one_le_two |>.sub (integrable_const _)) + (integrable_const b) hfb + simpa [integral_sub (hfν.integrable one_le_two) (integrable_const _)] using hint + -- the case `b = 0` is the limit of the bounds for `b + 3 ε / (a + 1)`, `ε > 0` + refine le_of_forall_pos_le_add fun ε hε ↦ ?_ + have hε' : 0 < 3 * ε / (a + 1) := by positivity + have := integral_sub_integral_le_of_klDiv_le_of_pos hfν hfμ (b := b + 3 * ε / (a + 1)) + (by positivity) (hfb.mono fun x hx ↦ by linarith) ha h + have hle : 3 * ε / (a + 1) * a / 3 ≤ ε := by + rw [div_mul_eq_mul_div, div_div, div_le_iff₀ (by positivity)] + nlinarith + linarith [show (b + 3 * ε / (a + 1)) * a / 3 = b * a / 3 + 3 * ε / (a + 1) * a / 3 by ring] + +/-- **Transport of the mean under a Kullback–Leibler constraint** [TM18], [MDJKLV21, Lemma 10]: +if `KL(μ ‖ ν) ≤ a` and `f` has values in `[c, d]` `ν`-almost everywhere, then +`|∫ f ∂μ - ∫ f ∂ν| ≤ √(2 Var_ν(f) a) + (d - c) a / 3`. -/ +theorem abs_integral_sub_integral_le_of_klDiv_le (hfm : AEStronglyMeasurable f ν) + (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : + |∫ x, f x ∂μ - ∫ x, f x ∂ν| ≤ √(2 * Var[f; ν] * a) + (d - c) * a / 3 := by + have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + have hfν : MemLp f 2 ν := memLp_of_bounded hf hfm 2 + have hfμ : Integrable f μ := + .of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable (hμν.ae_le hf) + have hm : ν[f] ∈ Set.Icc c d := + (convex_Icc c d).integral_mem isClosed_Icc hf (hfν.integrable one_le_two) + have hup := integral_sub_integral_le_of_klDiv_le hfν hfμ (b := d - c) + (hf.mono fun x hx ↦ by linarith [hx.2, hm.1]) ha h + have hdown := integral_sub_integral_le_of_klDiv_le (f := fun x ↦ -f x) hfν.neg hfμ.neg + (b := d - c) (hf.mono fun x hx ↦ by rw [integral_neg]; linarith [hx.1, hm.2]) ha h + rw [variance_fun_neg, integral_neg, integral_neg] at hdown + rw [abs_sub_le_iff] + exact ⟨hup, by linarith⟩ + +/-- The transport of the mean for a function with values in `[0, B]`, with the variance bounded +by `B` times the mean: `|∫ g ∂μ - ∫ g ∂ν| ≤ √(2 B (∫ g ∂ν) a) + B a / 3`. -/ +private lemma abs_integral_sub_integral_le_of_klDiv_le_of_nonneg {g : α → ℝ} {B : ℝ} + (hgm : AEStronglyMeasurable g ν) (hg : ∀ᵐ x ∂ν, g x ∈ Set.Icc 0 B) (ha : 0 ≤ a) + (h : klDiv μ ν ≤ ENNReal.ofReal a) : + |∫ x, g x ∂μ - ∫ x, g x ∂ν| ≤ √(2 * (B * ∫ x, g x ∂ν) * a) + B * a / 3 := by + have hvar := variance_le_mul_integral_sub hgm.aemeasurable hg + simp only [sub_zero] at hvar + refine (abs_integral_sub_integral_le_of_klDiv_le hgm hg ha h).trans ?_ + simp only [sub_zero] + gcongr + +/-- **Transport of the variance under a Kullback–Leibler constraint** [MDJKLV21, Lemma 11]: if +`KL(μ ‖ ν) ≤ a` and `f` has values in `[c, d]` `ν`-almost everywhere, then +`Var_ν(f) ≤ 2 Var_μ(f) + (8 / 3) (d - c)² a`. -/ +theorem variance_le_two_mul_variance_add_of_klDiv_le (hfm : AEStronglyMeasurable f ν) + (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : + Var[f; ν] ≤ 2 * Var[f; μ] + 8 / 3 * (d - c) ^ 2 * a := by + have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + have hfμ : ∀ᵐ x ∂μ, f x ∈ Set.Icc c d := hμν.ae_le hf + have hm : μ[f] ∈ Set.Icc c d := (convex_Icc c d).integral_mem isClosed_Icc hfμ + (.of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable hfμ) + -- the square `g = (f - ∫ f ∂μ) ^ 2` has values in `[0, (d - c) ^ 2]` + have hg : ∀ᵐ x ∂ν, (f x - μ[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := hf.mono fun x hx ↦ + ⟨sq_nonneg _, by nlinarith [hx.1, hx.2, hm.1, hm.2]⟩ + have hT := abs_integral_sub_integral_le_of_klDiv_le_of_nonneg (μ := μ) + (by fun_prop) hg ha h + rw [← variance_eq_integral (hfm.mono_ac hμν).aemeasurable] at hT + set x := ∫ y, (f y - μ[f]) ^ 2 ∂ν + have hx : Var[f; ν] ≤ x := variance_le_integral_sub_sq hfm _ + have hx0 : 0 ≤ x := integral_nonneg_of_ae (hg.mono fun _ hy ↦ hy.1) + -- `√(2 (d - c)² x a) ≤ x / 2 + (d - c)² a` + have hsq : √(2 * ((d - c) ^ 2 * x) * a) ≤ x / 2 + (d - c) ^ 2 * a := by + rw [sqrt_le_left (by positivity)] + nlinarith [sq_nonneg (x / 2 - (d - c) ^ 2 * a)] + linarith [(abs_le.1 hT).1] + +/-- **Transport of the variance under a Kullback–Leibler constraint**, the other direction +[MDJKLV21, Lemma 11]: if `KL(μ ‖ ν) ≤ a` and `f` has values in `[c, d]` `ν`-almost everywhere, +then `Var_μ(f) ≤ 2 Var_ν(f) + (5 / 6) (d - c)² a`. -/ +theorem variance_le_two_mul_variance_add_of_klDiv_le' (hfm : AEStronglyMeasurable f ν) + (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : + Var[f; μ] ≤ 2 * Var[f; ν] + 5 / 6 * (d - c) ^ 2 * a := by + have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + have hm : ν[f] ∈ Set.Icc c d := (convex_Icc c d).integral_mem isClosed_Icc hf + (.of_mem_Icc c d hfm.aemeasurable hf) + -- the square `g = (f - ∫ f ∂ν) ^ 2` has values in `[0, (d - c) ^ 2]` + have hg : ∀ᵐ x ∂ν, (f x - ν[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := hf.mono fun x hx ↦ + ⟨sq_nonneg _, by nlinarith [hx.1, hx.2, hm.1, hm.2]⟩ + have hT := abs_integral_sub_integral_le_of_klDiv_le_of_nonneg (μ := μ) + (by fun_prop) hg ha h + rw [← variance_eq_integral hfm.aemeasurable] at hT + have hx : Var[f; μ] ≤ ∫ y, (f y - ν[f]) ^ 2 ∂μ := variance_le_integral_sub_sq (hfm.mono_ac hμν) _ + have hv := variance_nonneg f ν + -- `√(2 (d - c)² Var_ν(f) a) ≤ Var_ν(f) + (d - c)² a / 2` + have hsq : √(2 * ((d - c) ^ 2 * Var[f; ν]) * a) ≤ Var[f; ν] + (d - c) ^ 2 * a / 2 := by + rw [sqrt_le_left (by positivity)] + nlinarith [sq_nonneg (Var[f; ν] - (d - c) ^ 2 * a / 2)] + linarith [(abs_le.1 hT).2] + +end LMLExplore diff --git a/LMLExplore/Probability/Moments/Variance.lean b/LMLExplore/Probability/Moments/Variance.lean index 5d68b87e..0a7343f1 100644 --- a/LMLExplore/Probability/Moments/Variance.lean +++ b/LMLExplore/Probability/Moments/Variance.lean @@ -8,6 +8,7 @@ module public import Mathlib.Probability.Kernel.MeasurableIntegral public import Mathlib.Probability.Moments.Variance import Mathlib.Algebra.QuadraticDiscriminant +import Mathlib.Analysis.Convex.Integral /-! # Variances under a kernel, and of bounded random variables @@ -28,6 +29,10 @@ function, such as the optimal value of a Markov decision process, with the varia computable one, and transfers a Bernstein-type bound on the deviation `∫ Y dμ - ∫ Y dν` of the nearby function `Y` to `X`. +The variance is also the least centred second moment, `Var[X; μ] ≤ ∫ (X - c) ^ 2 ∂μ`, which +transports variances: between two functions within `D` of each other, and between two laws on a +finite space at a cost proportional to their `ℓ¹` distance [MDJKLV21, Lemma 12]. + ## Main statements * `Measurable.variance_kernel`: `b ↦ Var[X; η b]` is measurable. @@ -40,6 +45,18 @@ nearby function `Y` to `X`. * `ProbabilityTheory.abs_integral_sub_integral_le_of_abs_sub_le`: a Bernstein-type bound `|∫ Y dμ - ∫ Y dν| ≤ a √Var[Y; μ] + b` transfers to every `X` uniformly within `d` of `Y`, at the cost of `(2 + a) d`. +* `ProbabilityTheory.variance_le_integral_sub_sq`: `Var[X; μ] ≤ ∫ (X - c) ^ 2 ∂μ`. +* `ProbabilityTheory.variance_le_mul_integral_sub`: `X ∈ [c, d]` gives + `Var[X; μ] ≤ (d - c) (𝔼 X - c)`. +* `ProbabilityTheory.variance_le_two_mul_variance_add_mul_integral_abs_sub`: if `|X - Y| ≤ D`, then + `Var[X; μ] ≤ 2 Var[Y; μ] + 2 D 𝔼 |X - Y|`. +* `ProbabilityTheory.variance_le_variance_add_mul_sum_abs_sub`: on a finite space, for `f` with + values in `[c, d]`, `Var[f; ν] ≤ Var[f; μ] + (d - c) ^ 2 / 2 * ∑ x, |μ {x} - ν {x}|`. + +## References + +* [MDJKLV21] P. Ménard, O. D. Domingues, A. Jonsson, E. Kaufmann, E. Leurent and M. Valko, + *Fast active learning for pure exploration in reinforcement learning*, ICML 2021. -/ public section @@ -143,4 +160,90 @@ theorem abs_integral_sub_integral_le_of_abs_sub_le {ν : Measure β} [IsProbabil |∫ x, Y x ∂μ - ∫ x, Y x ∂ν| := (abs_add_le _ _).trans (by gcongr; exact abs_sub _ _) _ ≤ a * √Var[X; μ] + (2 + a) * d + b := by linarith +/-- The variance is the least centred second moment: `Var[X; μ] ≤ ∫ (X - c) ^ 2 ∂μ` for every +`c`. -/ +theorem variance_le_integral_sub_sq (hX : AEStronglyMeasurable X μ) (c : ℝ) : + Var[X; μ] ≤ ∫ b, (X b - c) ^ 2 ∂μ := by + have h := variance_le_expectation_sq (μ := μ) (X := fun b ↦ X b - c) + (hX.sub aestronglyMeasurable_const) + rwa [variance_sub_const hX c] at h + +/-- A real random variable with values in `[c, d]` almost surely has variance at most +`(d - c) (𝔼 X - c)`; for `X ∈ [0, B]`, `Var[X; μ] ≤ B 𝔼 X`. This weakens the Bhatia–Davis +inequality `ProbabilityTheory.variance_le_sub_mul_sub`. -/ +theorem variance_le_mul_integral_sub {c d : ℝ} (hX : AEMeasurable X μ) + (h : ∀ᵐ b ∂μ, X b ∈ Set.Icc c d) : Var[X; μ] ≤ (d - c) * (μ[X] - c) := by + have hm : μ[X] ∈ Set.Icc c d := + (convex_Icc c d).integral_mem isClosed_Icc h (.of_mem_Icc c d hX h) + refine (variance_le_sub_mul_sub h hX).trans ?_ + nlinarith [hm.1, hm.2] + +/-- **Transport of the variance between two functions** [MDJKLV21, Lemma 12]: if `|X - Y| ≤ D` +almost surely, then `Var[X; μ] ≤ 2 Var[Y; μ] + 2 D 𝔼 |X - Y|`. The source states it for +functions with values in `[0, D]`. -/ +theorem variance_le_two_mul_variance_add_mul_integral_abs_sub (hX : AEStronglyMeasurable X μ) + (hY : MemLp Y 2 μ) {D : ℝ} (hD : ∀ᵐ b ∂μ, |X b - Y b| ≤ D) : + Var[X; μ] ≤ 2 * Var[Y; μ] + 2 * D * ∫ b, |X b - Y b| ∂μ := by + have hYc : Integrable (fun b ↦ (Y b - μ[Y]) ^ 2) μ := (hY.sub (memLp_const _)).integrable_sq + have habs : Integrable (fun b ↦ |X b - Y b|) μ := + .of_bound (hX.sub hY.aestronglyMeasurable).norm D + (hD.mono fun b hb ↦ by rwa [Real.norm_eq_abs, abs_abs]) + calc Var[X; μ] ≤ ∫ b, (X b - μ[Y]) ^ 2 ∂μ := variance_le_integral_sub_sq hX _ + _ ≤ ∫ b, (2 * D * |X b - Y b| + 2 * (Y b - μ[Y]) ^ 2) ∂μ := by + refine integral_mono_of_nonneg (.of_forall fun _ ↦ sq_nonneg _) + ((habs.const_mul _).add (hYc.const_mul _)) ?_ + filter_upwards [hD] with b hb + have hsq : (X b - Y b) ^ 2 ≤ D * |X b - Y b| := by + rw [← sq_abs] + nlinarith [abs_nonneg (X b - Y b)] + nlinarith [sq_nonneg (X b - Y b - (Y b - μ[Y]))] + _ = 2 * Var[Y; μ] + 2 * D * ∫ b, |X b - Y b| ∂μ := by + rw [integral_add (habs.const_mul _) (hYc.const_mul _), integral_const_mul, + integral_const_mul, variance_eq_integral hY.aestronglyMeasurable.aemeasurable] + ring + +/-- **Transport of the variance between two laws on a finite space** [MDJKLV21, Lemma 12]: for +probability measures `μ` and `ν` on a finite type and `f` with values in `[c, d]`, +`Var[f; ν] ≤ Var[f; μ] + (d - c) ^ 2 / 2 * ∑ x, |μ {x} - ν {x}|`. This sharpens the factor `3` of +the source to `1 / 2`. -/ +theorem variance_le_variance_add_mul_sum_abs_sub {ι : Type*} [Fintype ι] [MeasurableSpace ι] + [MeasurableSingletonClass ι] {μ ν : Measure ι} [IsProbabilityMeasure μ] + [IsProbabilityMeasure ν] {f : ι → ℝ} {c d : ℝ} (hf : ∀ x, f x ∈ Set.Icc c d) : + Var[f; ν] ≤ Var[f; μ] + (d - c) ^ 2 / 2 * ∑ x, |μ.real {x} - ν.real {x}| := by + have hfm : Measurable f := measurable_of_finite f + set m := μ[f] + have hm : m ∈ Set.Icc c d := + (convex_Icc c d).integral_mem isClosed_Icc (.of_forall hf) .of_finite + -- the centred square `(f - m) ^ 2` has values in `[0, (d - c) ^ 2]` + have hg x : (f x - m) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := by + refine ⟨sq_nonneg _, ?_⟩ + have := (hf x).1; have := (hf x).2 + nlinarith [hm.1, hm.2] + have hsum (ρ : Measure ι) [IsProbabilityMeasure ρ] : + ∫ x, (f x - m) ^ 2 ∂ρ = ∑ x, ρ.real {x} * (f x - m) ^ 2 := by + simp [integral_fintype Integrable.of_finite] + have hμ : Var[f; μ] = ∑ x, μ.real {x} * (f x - m) ^ 2 := by + rw [variance_eq_integral hfm.aemeasurable, hsum] + -- subtracting the constant `(d - c) ^ 2 / 2` does not change the difference of the sums + have hshift : ∑ x, ν.real {x} * (f x - m) ^ 2 - ∑ x, μ.real {x} * (f x - m) ^ 2 + = ∑ x, (ν.real {x} - μ.real {x}) * ((f x - m) ^ 2 - (d - c) ^ 2 / 2) := by + have h1 : ∑ x, ν.real {x} = ∑ x, μ.real {x} := by simp + simp only [sub_mul, mul_sub, Finset.sum_sub_distrib, ← Finset.sum_mul, h1] + ring + have hterm x : (ν.real {x} - μ.real {x}) * ((f x - m) ^ 2 - (d - c) ^ 2 / 2) + ≤ (d - c) ^ 2 / 2 * |μ.real {x} - ν.real {x}| := by + rw [abs_sub_comm] + refine (le_abs_self _).trans ?_ + rw [abs_mul, mul_comm] + gcongr + rw [abs_le] + constructor <;> linarith [(hg x).1, (hg x).2] + calc Var[f; ν] ≤ ∑ x, ν.real {x} * (f x - m) ^ 2 := by + rw [← hsum]; exact variance_le_integral_sub_sq hfm.aestronglyMeasurable m + _ = Var[f; μ] + ∑ x, (ν.real {x} - μ.real {x}) * ((f x - m) ^ 2 - (d - c) ^ 2 / 2) := by + rw [← hshift, hμ]; ring + _ ≤ Var[f; μ] + (d - c) ^ 2 / 2 * ∑ x, |μ.real {x} - ν.real {x}| := by + rw [Finset.mul_sum] + exact add_le_add_right (Finset.sum_le_sum fun x _ ↦ hterm x) _ + end ProbabilityTheory From 546ea0c1509ac601490ccfcad0aab4e52082ef75 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 07:41:54 +0100 Subject: [PATCH 2/5] refactor: factor out the Chernoff inversion and the repeated interval facts - `Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub`: the closed-form inversion of the sub-gamma bound, shared by the KL transport and the high-probability Bernstein inequality. - `MeasureTheory.integral_mem_Icc_of_ae_mem_Icc`, `sq_sub_mem_Icc_of_mem_Icc` and `LMLExplore.absolutelyContinuous_of_klDiv_le_ofReal`, each used where the fact was inlined. - Credit the paper project Essakine2026Tight in both module docstrings. Co-Authored-By: Claude Code --- LMLExplore/Algebra/Order/Ring/Abs.lean | 30 ++++++++ LMLExplore/Analysis/Convex/Integral.lean | 15 +++- LMLExplore/Analysis/SpecialFunctions/Exp.lean | 40 +++++++++- .../KullbackLeibler/Bernstein.lean | 74 ++++++++----------- LMLExplore/Probability/Moments/Bernstein.lean | 38 ++-------- LMLExplore/Probability/Moments/Variance.lean | 20 ++--- 6 files changed, 128 insertions(+), 89 deletions(-) create mode 100644 LMLExplore/Algebra/Order/Ring/Abs.lean diff --git a/LMLExplore/Algebra/Order/Ring/Abs.lean b/LMLExplore/Algebra/Order/Ring/Abs.lean new file mode 100644 index 00000000..ac1b37ac --- /dev/null +++ b/LMLExplore/Algebra/Order/Ring/Abs.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Algebra.Order.Ring.Abs +public import Mathlib.Order.Interval.Set.Defs + +/-! +# The square of a difference of two points of an interval + +Two points `x` and `y` of `[c, d]` in a linearly ordered ring are within `d - c` of each other, so +`(x - y) ^ 2` lies in `[0, (d - c) ^ 2]`. This bounds the centred squares `(f - m) ^ 2` of a +function `f` with values in `[c, d]` around a mean `m ∈ [c, d]`, in the transport of variances. + +## Main statements + +* `sq_sub_mem_Icc_of_mem_Icc`: `(x - y) ^ 2 ∈ [0, (d - c) ^ 2]` for `x, y ∈ [c, d]`. +-/ + +public section + +variable {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {x y c d : R} + +/-- For `x, y ∈ [c, d]`, the square `(x - y) ^ 2` lies in `[0, (d - c) ^ 2]`. -/ +theorem sq_sub_mem_Icc_of_mem_Icc (hx : x ∈ Set.Icc c d) (hy : y ∈ Set.Icc c d) : + (x - y) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := + ⟨sq_nonneg _, sq_le_sq' (by rw [neg_sub]; exact sub_le_sub hx.1 hy.2) (sub_le_sub hx.2 hy.1)⟩ diff --git a/LMLExplore/Analysis/Convex/Integral.lean b/LMLExplore/Analysis/Convex/Integral.lean index ee467c95..8f88bf9a 100644 --- a/LMLExplore/Analysis/Convex/Integral.lean +++ b/LMLExplore/Analysis/Convex/Integral.lean @@ -9,12 +9,14 @@ public import Mathlib.Analysis.Convex.Integral public import Mathlib.Analysis.Convex.SpecificFunctions.Pow /-! -# The mean of a measure concentrated on an interval, and Jensen's inequality for the square root +# The mean of a function with values in an interval, and Jensen's inequality for the square root ## Main statements +* `MeasureTheory.integral_mem_Icc_of_ae_mem_Icc`: the mean of a function with values in `[l, u]` + almost everywhere under a probability measure lies in `[l, u]`, by `Convex.integral_mem`. * `MeasureTheory.integral_id_mem_Icc_of_ae_mem_Icc`: the mean of a probability measure on `ℝ` - concentrated on `[l, u]` lies in `[l, u]`, by `Convex.integral_mem`. + concentrated on `[l, u]` lies in `[l, u]`. * `MeasureTheory.integral_sqrt_le_sqrt_measureReal_mul_integral`: Jensen's inequality for the square root, `∫ √g ∂μ ≤ √(μ(univ) ∫ g ∂μ)` for a finite measure `μ` and an integrable `g ≥ 0`, by `ConcaveOn.le_map_average`. @@ -24,10 +26,17 @@ public section namespace MeasureTheory +/-- The mean of a real function with values in `[l, u]` almost everywhere under a probability +measure lies in `[l, u]`. -/ +theorem integral_mem_Icc_of_ae_mem_Icc {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} + [IsProbabilityMeasure μ] {f : α → ℝ} {l u : ℝ} (hf : AEMeasurable f μ) + (h : ∀ᵐ x ∂μ, f x ∈ Set.Icc l u) : ∫ x, f x ∂μ ∈ Set.Icc l u := + (convex_Icc l u).integral_mem isClosed_Icc h (Integrable.of_mem_Icc l u hf h) + /-- The mean of a probability measure on `ℝ` concentrated on `[l, u]` lies in `[l, u]`. -/ theorem integral_id_mem_Icc_of_ae_mem_Icc {μ : Measure ℝ} [IsProbabilityMeasure μ] {l u : ℝ} (h : ∀ᵐ x ∂μ, x ∈ Set.Icc l u) : ∫ x, id x ∂μ ∈ Set.Icc l u := - (convex_Icc l u).integral_mem isClosed_Icc h (Integrable.of_mem_Icc l u aemeasurable_id h) + integral_mem_Icc_of_ae_mem_Icc aemeasurable_id h /-- **Jensen's inequality for the square root**: for a finite measure `μ` and an integrable function `g ≥ 0`, `∫ √g ∂μ ≤ √(μ(univ) ∫ g ∂μ)`. For a probability measure, this is diff --git a/LMLExplore/Analysis/SpecialFunctions/Exp.lean b/LMLExplore/Analysis/SpecialFunctions/Exp.lean index 03a504b2..1bf489e3 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Exp.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Exp.lean @@ -50,7 +50,7 @@ increases with the argument: `x ↦ (exp x - 1 - x) / x ^ 2` is monotone on `[0, [BLM13, proof of Theorem 2.9], the one-step bound behind the inequalities of Bennett, Bernstein and Freedman. Comparing the series with a geometric one gives `exp x - 1 - x ≤ x ^ 2 / (2 (1 - x / 3))` for `0 ≤ x < 3`, which turns -these into Bernstein's form. +these into Bernstein's form, and inverts in closed form at Chernoff's choice of parameter. By the convexity of the exponential, a sum of exponentials is at least its number of terms times the exponential of the mean of the exponents. This spreads a bound on a sum of divergences @@ -82,6 +82,8 @@ lower bound for linear bandits on the unit ball [LS, Theorem 24.2]. * `Real.exp_mul_le_one_add_mul_add_mul_sq`: Bennett's bound `exp (l x) ≤ 1 + l x + (exp (l b) - 1 - l b) / b ^ 2 * x ^ 2` for `b > 0`, `l ≥ 0`, `x ≤ b`. * `Real.exp_sub_one_sub_id_le_sq_div`: `exp x - 1 - x ≤ x ^ 2 / (2 (1 - x / 3))` for `0 ≤ x < 3`. +* `Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub`: the closed-form inversion of this + sub-gamma bound, `L ≤ t (√(2 v L) + b L / 3) - v (exp (t b) - 1 - t b) / b ^ 2` for some `t > 0`. * `Real.card_mul_exp_sum_div_card_le_sum_exp`: `#s exp ((∑ i ∈ s, x i) / #s) ≤ ∑ i ∈ s, exp (x i)`. ## References @@ -319,6 +321,42 @@ theorem exp_sub_one_sub_id_le_sq_div {x : ℝ} (hx : 0 ≤ x) (hx3 : x < 3) : have : 1 - x / 3 ≠ 0 := by linarith field_simp +/-- **Inversion of the sub-gamma bound**, Chernoff's choice of parameter in Bernstein's +inequality [BLM13, Theorem 2.10]: for `b, v, L > 0`, some `t > 0` has +`L ≤ t (√(2 v L) + b L / 3) - v ψ_b(t)`, with `ψ_b(t) = (exp (t b) - 1 - t b) / b ^ 2`. It is +`t = r / (v + b r / 3)` with `r = √(2 v L)`, at which the bound +`ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` of `exp_sub_one_sub_id_le_sq_div` makes the right-hand +side at least `L`. -/ +theorem exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub {b v L : ℝ} (hb : 0 < b) + (hv : 0 < v) (hL : 0 < L) : + ∃ t, 0 < t ∧ + L ≤ t * (√(2 * v * L) + b * L / 3) - v * ((exp (t * b) - 1 - t * b) / b ^ 2) := by + set r := √(2 * v * L) + have hr : r ^ 2 = 2 * v * L := sq_sqrt (by positivity) + have hr0 : 0 < r := sqrt_pos.2 (by positivity) + obtain ⟨s, hs⟩ : ∃ s, s = v + b * r / 3 := ⟨_, rfl⟩ + have hs0 : 0 < s := by rw [hs]; positivity + refine ⟨r / s, by positivity, ?_⟩ + have htb : r / s * b < 3 := by + rw [div_mul_eq_mul_div, div_lt_iff₀ hs0] + nlinarith + have hψ : (exp (r / s * b) - 1 - r / s * b) / b ^ 2 ≤ + (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by + calc (exp (r / s * b) - 1 - r / s * b) / b ^ 2 + ≤ (r / s * b) ^ 2 / (2 * (1 - r / s * b / 3)) / b ^ 2 := by + gcongr + exact exp_sub_one_sub_id_le_sq_div (by positivity) htb + _ = (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by field_simp + have h1 : 1 - r / s * b / 3 = v / s := by + field_simp + linear_combination 3 * hs + have hval : r / s * (r + b * L / 3) - v * ((r / s) ^ 2 / (2 * (1 - r / s * b / 3))) = L := by + have hv' : v ≠ 0 := hv.ne' + rw [h1] + field_simp + linear_combination 3 * hr - 6 * L * hs + linarith [mul_le_mul_of_nonneg_left hψ hv.le] + /-- **Bennett's bound on the exponential.** For `b > 0`, `l ≥ 0` and `x ≤ b`, `exp (l x) ≤ 1 + l x + ψ x ^ 2` with `ψ = (exp (l b) - 1 - l b) / b ^ 2`. -/ theorem exp_mul_le_one_add_mul_add_mul_sq {b l x : ℝ} (hb : 0 < b) (hl : 0 ≤ l) (hx : x ≤ b) : diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean index a1855fce..8da898b0 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -7,7 +7,8 @@ module public import Mathlib.InformationTheory.KullbackLeibler.Basic public import Mathlib.Probability.Moments.Variance -import Mathlib.Analysis.Convex.Integral +import LMLExplore.Algebra.Order.Ring.Abs +import LMLExplore.Analysis.Convex.Integral import LMLExplore.Analysis.SpecialFunctions.Exp import LMLExplore.Probability.Moments.Bernstein import LMLExplore.Probability.Moments.Variance @@ -31,10 +32,18 @@ The proof combines the Donsker–Varadhan inequality Bennett's bound on the moment-generating function of the centred function (`MeasureTheory.MemLp.mgf_le_exp_mul_exp_sub_one_sub_of_ae_le`). Its sub-gamma form `exp x - 1 - x ≤ x² / (2 (1 - x / 3))` then inverts in closed form, as in the high-probability form -of Bernstein's inequality [BLM13, Theorem 2.10]. +of Bernstein's inequality [BLM13, Theorem 2.10] +(`Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub`). + +The statements, their order and the decomposition into [MDJKLV21, Lemmas 10 and 11] are adapted +from the paper project Essakine2026Tight (`github.com/RemyDegenne/Essakine2026Tight`, file +`Essakine2026Tight/ForLMLExplore/InformationTheory/KLBernstein.lean`, by Rémy Degenne, +Apache 2.0), with a new proof of the transport of the mean and sharper constants. ## Main statements +* `LMLExplore.absolutelyContinuous_of_klDiv_le_ofReal`: a finite bound on `KL(μ ‖ ν)` gives + `μ ≪ ν`. * `LMLExplore.integral_sub_integral_le_of_klDiv_le`: the one-sided transport, for `f` bounded above by its `ν`-mean plus `b`. * `LMLExplore.abs_integral_sub_integral_le_of_klDiv_le`: the two-sided transport for `f` with @@ -67,6 +76,11 @@ namespace LMLExplore variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {f : α → ℝ} {a b c d : ℝ} +/-- A finite bound `KL(μ ‖ ν) ≤ a` gives `μ ≪ ν`. -/ +theorem absolutelyContinuous_of_klDiv_le_ofReal {μ ν : Measure α} + (h : klDiv μ ν ≤ ENNReal.ofReal a) : μ ≪ ν := + (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + /-- The Donsker–Varadhan inequality at `g = t (f - ∫ f ∂ν)`, with Bennett's bound on the moment-generating function: for every `t ≥ 0`, `t (∫ f ∂μ - ∫ f ∂ν) - Var_ν(f) ψ_b(t) ≤ a`, with `ψ_b(t) = (exp (t b) - 1 - t b) / b²`. -/ @@ -110,36 +124,10 @@ private lemma integral_sub_integral_le_of_klDiv_le_of_pos (hfν : MemLp f 2 ν) have := key (t := (a + 1) / D) (by positivity) rw [← hv, div_mul_cancel₀ _ hD0.ne'] at this linarith - -- Chernoff's choice `t = r / (v + b r / 3)` with `r = √(2 v a)`, at which the sub-gamma bound - -- `ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` makes `t (r + b a / 3) - v ψ_b(t)` at least `a` - set r := √(2 * v * a) - have hr : r ^ 2 = 2 * v * a := sq_sqrt (by positivity) - have hr0 : 0 < r := sqrt_pos.2 (by positivity) - obtain ⟨s, hs⟩ : ∃ s, s = v + b * r / 3 := ⟨_, rfl⟩ - have hs0 : 0 < s := by rw [hs]; positivity - obtain ⟨t, rfl⟩ : ∃ t, t = r / s := ⟨_, rfl⟩ - have ht : 0 < r / s := by positivity - have htb : r / s * b < 3 := by - rw [div_mul_eq_mul_div, div_lt_iff₀ hs0] - nlinarith - have hψ : (exp (r / s * b) - 1 - r / s * b) / b ^ 2 ≤ - (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by - calc (exp (r / s * b) - 1 - r / s * b) / b ^ 2 - ≤ (r / s * b) ^ 2 / (2 * (1 - r / s * b / 3)) / b ^ 2 := by - gcongr - exact exp_sub_one_sub_id_le_sq_div (by positivity) htb - _ = (r / s) ^ 2 / (2 * (1 - r / s * b / 3)) := by field_simp - have h1 : 1 - r / s * b / 3 = v / s := by - field_simp - linear_combination 3 * hs - have hval : r / s * (r + b * a / 3) - v * ((r / s) ^ 2 / (2 * (1 - r / s * b / 3))) = a := by - have hv' : v ≠ 0 := hv.ne' - rw [h1] - field_simp - linear_combination 3 * hr - 6 * a * hs + -- Chernoff's choice of `t`, at which `t (√(2 v a) + b a / 3) - v ψ_b(t)` is at least `a` + obtain ⟨t, ht, hta⟩ := exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub hb hv ha' have hkey := key ht.le - have : r / s * D ≤ r / s * (r + b * a / 3) := by nlinarith [mul_le_mul_of_nonneg_left hψ hv.le] - exact le_of_mul_le_mul_left this ht + exact le_of_mul_le_mul_left (by linarith) ht /-- **Transport of the mean under a Kullback–Leibler constraint**, one-sided form: if `KL(μ ‖ ν) ≤ a` and `f ≤ ∫ f ∂ν + b` holds `ν`-almost everywhere, then @@ -168,12 +156,11 @@ if `KL(μ ‖ ν) ≤ a` and `f` has values in `[c, d]` `ν`-almost everywhere, theorem abs_integral_sub_integral_le_of_klDiv_le (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : |∫ x, f x ∂μ - ∫ x, f x ∂ν| ≤ √(2 * Var[f; ν] * a) + (d - c) * a / 3 := by - have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h have hfν : MemLp f 2 ν := memLp_of_bounded hf hfm 2 have hfμ : Integrable f μ := .of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable (hμν.ae_le hf) - have hm : ν[f] ∈ Set.Icc c d := - (convex_Icc c d).integral_mem isClosed_Icc hf (hfν.integrable one_le_two) + have hm : ν[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hfm.aemeasurable hf have hup := integral_sub_integral_le_of_klDiv_le hfν hfμ (b := d - c) (hf.mono fun x hx ↦ by linarith [hx.2, hm.1]) ha h have hdown := integral_sub_integral_le_of_klDiv_le (f := fun x ↦ -f x) hfν.neg hfμ.neg @@ -200,13 +187,13 @@ private lemma abs_integral_sub_integral_le_of_klDiv_le_of_nonneg {g : α → ℝ theorem variance_le_two_mul_variance_add_of_klDiv_le (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; ν] ≤ 2 * Var[f; μ] + 8 / 3 * (d - c) ^ 2 * a := by - have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 + have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h have hfμ : ∀ᵐ x ∂μ, f x ∈ Set.Icc c d := hμν.ae_le hf - have hm : μ[f] ∈ Set.Icc c d := (convex_Icc c d).integral_mem isClosed_Icc hfμ - (.of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable hfμ) + have hm : μ[f] ∈ Set.Icc c d := + integral_mem_Icc_of_ae_mem_Icc (hfm.mono_ac hμν).aemeasurable hfμ -- the square `g = (f - ∫ f ∂μ) ^ 2` has values in `[0, (d - c) ^ 2]` - have hg : ∀ᵐ x ∂ν, (f x - μ[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := hf.mono fun x hx ↦ - ⟨sq_nonneg _, by nlinarith [hx.1, hx.2, hm.1, hm.2]⟩ + have hg : ∀ᵐ x ∂ν, (f x - μ[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := + hf.mono fun _ hx ↦ sq_sub_mem_Icc_of_mem_Icc hx hm have hT := abs_integral_sub_integral_le_of_klDiv_le_of_nonneg (μ := μ) (by fun_prop) hg ha h rw [← variance_eq_integral (hfm.mono_ac hμν).aemeasurable] at hT @@ -225,12 +212,11 @@ then `Var_μ(f) ≤ 2 Var_ν(f) + (5 / 6) (d - c)² a`. -/ theorem variance_le_two_mul_variance_add_of_klDiv_le' (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; μ] ≤ 2 * Var[f; ν] + 5 / 6 * (d - c) ^ 2 * a := by - have hμν : μ ≪ ν := (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 - have hm : ν[f] ∈ Set.Icc c d := (convex_Icc c d).integral_mem isClosed_Icc hf - (.of_mem_Icc c d hfm.aemeasurable hf) + have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h + have hm : ν[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hfm.aemeasurable hf -- the square `g = (f - ∫ f ∂ν) ^ 2` has values in `[0, (d - c) ^ 2]` - have hg : ∀ᵐ x ∂ν, (f x - ν[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := hf.mono fun x hx ↦ - ⟨sq_nonneg _, by nlinarith [hx.1, hx.2, hm.1, hm.2]⟩ + have hg : ∀ᵐ x ∂ν, (f x - ν[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := + hf.mono fun _ hx ↦ sq_sub_mem_Icc_of_mem_Icc hx hm have hT := abs_integral_sub_integral_le_of_klDiv_le_of_nonneg (μ := μ) (by fun_prop) hg ha h rw [← variance_eq_integral hfm.aemeasurable] at hT diff --git a/LMLExplore/Probability/Moments/Bernstein.lean b/LMLExplore/Probability/Moments/Bernstein.lean index 3126ccd4..b55a8e74 100644 --- a/LMLExplore/Probability/Moments/Bernstein.lean +++ b/LMLExplore/Probability/Moments/Bernstein.lean @@ -30,7 +30,8 @@ inequality. Since `ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` for `t b < 3` (`Real.exp_sub_one_sub_id_le_sq_div`), `S` is also sub-gamma with variance factor `v` and scale -`b / 3`. Chernoff's bound at an explicit `t` then inverts in closed form: for every `L`, +`b / 3`. Chernoff's bound at an explicit `t` then inverts in closed form +(`Real.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub`): for every `L`, `P(√(2 v L) + b L / 3 ≤ S) ≤ exp (-L)`, so that with probability at least `1 - δ`, `S < √(2 v log (1 / δ)) + b log (1 / δ) / 3`. This is the form of Bernstein's inequality in which confidence bounds are stated [BLM13, Theorem 2.10]. It is also the high-probability form of @@ -231,37 +232,12 @@ theorem measureReal_sqrt_add_le_sum_le_of_ae_le (h_indep : iIndepFun X μ) {b v linarith rw [hnull] positivity - -- Chernoff's bound at `t = r / (v + b r / 3)` with `r = √(2 v L)`, where the sub-gamma bound - -- `ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` makes the exponent exactly `-L`. - set r := √(2 * v * L) - have hr : r ^ 2 = 2 * v * L := sq_sqrt (by positivity) - have hr0 : 0 ≤ r := sqrt_nonneg _ - have hD : 0 < v + b * r / 3 := by positivity - set t := r / (v + b * r / 3) - have ht : 0 ≤ t := by positivity - have htb : t * b < 3 := by - rw [div_mul_eq_mul_div, div_lt_iff₀ hD] - nlinarith - have h1 : 1 - t * b / 3 = v / (v + b * r / 3) := by - simp only [t] - field_simp - ring - have hmgf : mgf (fun ω ↦ ∑ i ∈ s, X i ω) μ t ≤ exp (v * t ^ 2 / (2 * (1 - t * b / 3))) := by - refine (h_indep.mgf_sum_le_exp_mul_exp_sub_one_sub_of_ae_le hX hmean hb hXb hv ht).trans - (exp_le_exp.2 ?_) - calc v * ((exp (t * b) - 1 - t * b) / b ^ 2) - ≤ v * ((t * b) ^ 2 / (2 * (1 - t * b / 3)) / b ^ 2) := by - gcongr - exact exp_sub_one_sub_id_le_sq_div (by positivity) htb - _ = v * t ^ 2 / (2 * (1 - t * b / 3)) := by - field_simp + -- Chernoff's bound at the parameter `t` at which the exponent is at most `-L`. + obtain ⟨t, ht, htL⟩ := exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub hb hv0 hL refine (measureReal_sum_ge_le_exp_of_mgf_le - (fun i hi ↦ (hX i hi).aestronglyMeasurable.aemeasurable) hXb ht hmgf).trans_eq ?_ - rw [h1] - congr 1 - simp only [t] - field_simp - linear_combination (-3 : ℝ) * hr + (fun i hi ↦ (hX i hi).aestronglyMeasurable.aemeasurable) hXb ht.le + (h_indep.mgf_sum_le_exp_mul_exp_sub_one_sub_of_ae_le hX hmean hb hXb hv ht.le)).trans + (exp_le_exp.2 (by linarith)) /-- **Bernstein's inequality at confidence level `δ`** [BLM13, Theorem 2.10]. Under the hypotheses of `measureReal_sqrt_add_le_sum_le_of_ae_le`, for `δ > 0`, with probability at least diff --git a/LMLExplore/Probability/Moments/Variance.lean b/LMLExplore/Probability/Moments/Variance.lean index 0a7343f1..c8364bdb 100644 --- a/LMLExplore/Probability/Moments/Variance.lean +++ b/LMLExplore/Probability/Moments/Variance.lean @@ -8,7 +8,8 @@ module public import Mathlib.Probability.Kernel.MeasurableIntegral public import Mathlib.Probability.Moments.Variance import Mathlib.Algebra.QuadraticDiscriminant -import Mathlib.Analysis.Convex.Integral +import LMLExplore.Algebra.Order.Ring.Abs +import LMLExplore.Analysis.Convex.Integral /-! # Variances under a kernel, and of bounded random variables @@ -31,7 +32,11 @@ nearby function `Y` to `X`. The variance is also the least centred second moment, `Var[X; μ] ≤ ∫ (X - c) ^ 2 ∂μ`, which transports variances: between two functions within `D` of each other, and between two laws on a -finite space at a cost proportional to their `ℓ¹` distance [MDJKLV21, Lemma 12]. +finite space at a cost proportional to their `ℓ¹` distance [MDJKLV21, Lemma 12]. These variance +transports, and `variance_le_integral_sub_sq` and `variance_le_mul_integral_sub`, are adapted from +the paper project Essakine2026Tight (`github.com/RemyDegenne/Essakine2026Tight`, file +`Essakine2026Tight/ForLMLExplore/Probability/Moments/VarianceTransport.lean`, by Rémy Degenne, +Apache 2.0). ## Main statements @@ -173,8 +178,7 @@ theorem variance_le_integral_sub_sq (hX : AEStronglyMeasurable X μ) (c : ℝ) : inequality `ProbabilityTheory.variance_le_sub_mul_sub`. -/ theorem variance_le_mul_integral_sub {c d : ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ b ∂μ, X b ∈ Set.Icc c d) : Var[X; μ] ≤ (d - c) * (μ[X] - c) := by - have hm : μ[X] ∈ Set.Icc c d := - (convex_Icc c d).integral_mem isClosed_Icc h (.of_mem_Icc c d hX h) + have hm : μ[X] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hX h refine (variance_le_sub_mul_sub h hX).trans ?_ nlinarith [hm.1, hm.2] @@ -212,13 +216,9 @@ theorem variance_le_variance_add_mul_sum_abs_sub {ι : Type*} [Fintype ι] [Meas Var[f; ν] ≤ Var[f; μ] + (d - c) ^ 2 / 2 * ∑ x, |μ.real {x} - ν.real {x}| := by have hfm : Measurable f := measurable_of_finite f set m := μ[f] - have hm : m ∈ Set.Icc c d := - (convex_Icc c d).integral_mem isClosed_Icc (.of_forall hf) .of_finite + have hm : m ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hfm.aemeasurable (.of_forall hf) -- the centred square `(f - m) ^ 2` has values in `[0, (d - c) ^ 2]` - have hg x : (f x - m) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := by - refine ⟨sq_nonneg _, ?_⟩ - have := (hf x).1; have := (hf x).2 - nlinarith [hm.1, hm.2] + have hg x : (f x - m) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := sq_sub_mem_Icc_of_mem_Icc (hf x) hm have hsum (ρ : Measure ι) [IsProbabilityMeasure ρ] : ∫ x, (f x - m) ^ 2 ∂ρ = ∑ x, ρ.real {x} * (f x - m) ^ 2 := by simp [integral_fintype Integrable.of_finite] From 3a38a9ef4236dbc4134515859d4b9c4a1498866b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 08:06:07 +0100 Subject: [PATCH 3/5] refactor: weaken absolutelyContinuous_of_klDiv_ne_top to a finiteness hypothesis Co-Authored-By: Claude Code --- .../KullbackLeibler/Bernstein.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean index 8da898b0..216cd4a5 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -42,8 +42,7 @@ Apache 2.0), with a new proof of the transport of the mean and sharper constants ## Main statements -* `LMLExplore.absolutelyContinuous_of_klDiv_le_ofReal`: a finite bound on `KL(μ ‖ ν)` gives - `μ ≪ ν`. +* `LMLExplore.absolutelyContinuous_of_klDiv_ne_top`: a finite `KL(μ ‖ ν)` gives `μ ≪ ν`. * `LMLExplore.integral_sub_integral_le_of_klDiv_le`: the one-sided transport, for `f` bounded above by its `ν`-mean plus `b`. * `LMLExplore.abs_integral_sub_integral_le_of_klDiv_le`: the two-sided transport for `f` with @@ -76,10 +75,9 @@ namespace LMLExplore variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {f : α → ℝ} {a b c d : ℝ} -/-- A finite bound `KL(μ ‖ ν) ≤ a` gives `μ ≪ ν`. -/ -theorem absolutelyContinuous_of_klDiv_le_ofReal {μ ν : Measure α} - (h : klDiv μ ν ≤ ENNReal.ofReal a) : μ ≪ ν := - (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 +/-- A finite Kullback–Leibler divergence `KL(μ ‖ ν) ≠ ∞` gives `μ ≪ ν`. -/ +theorem absolutelyContinuous_of_klDiv_ne_top {μ ν : Measure α} (h : klDiv μ ν ≠ ∞) : μ ≪ ν := + (klDiv_ne_top_iff.1 h).1 /-- The Donsker–Varadhan inequality at `g = t (f - ∫ f ∂ν)`, with Bennett's bound on the moment-generating function: for every `t ≥ 0`, @@ -156,7 +154,8 @@ if `KL(μ ‖ ν) ≤ a` and `f` has values in `[c, d]` `ν`-almost everywhere, theorem abs_integral_sub_integral_le_of_klDiv_le (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : |∫ x, f x ∂μ - ∫ x, f x ∂ν| ≤ √(2 * Var[f; ν] * a) + (d - c) * a / 3 := by - have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h + have hμν : μ ≪ ν := + absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) have hfν : MemLp f 2 ν := memLp_of_bounded hf hfm 2 have hfμ : Integrable f μ := .of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable (hμν.ae_le hf) @@ -187,7 +186,8 @@ private lemma abs_integral_sub_integral_le_of_klDiv_le_of_nonneg {g : α → ℝ theorem variance_le_two_mul_variance_add_of_klDiv_le (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; ν] ≤ 2 * Var[f; μ] + 8 / 3 * (d - c) ^ 2 * a := by - have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h + have hμν : μ ≪ ν := + absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) have hfμ : ∀ᵐ x ∂μ, f x ∈ Set.Icc c d := hμν.ae_le hf have hm : μ[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc (hfm.mono_ac hμν).aemeasurable hfμ @@ -212,7 +212,8 @@ then `Var_μ(f) ≤ 2 Var_ν(f) + (5 / 6) (d - c)² a`. -/ theorem variance_le_two_mul_variance_add_of_klDiv_le' (hfm : AEStronglyMeasurable f ν) (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; μ] ≤ 2 * Var[f; ν] + 5 / 6 * (d - c) ^ 2 * a := by - have hμν : μ ≪ ν := absolutelyContinuous_of_klDiv_le_ofReal h + have hμν : μ ≪ ν := + absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) have hm : ν[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hfm.aemeasurable hf -- the square `g = (f - ∫ f ∂ν) ^ 2` has values in `[0, (d - c) ^ 2]` have hg : ∀ᵐ x ∂ν, (f x - ν[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) := From ddebeaace42086351055bee7455c37849728741d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 09:14:03 +0100 Subject: [PATCH 4/5] chore: name LMLExplore contributors in the headers of the new files Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- LMLExplore/Algebra/Order/Ring/Abs.lean | 4 ++-- LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/LMLExplore/Algebra/Order/Ring/Abs.lean b/LMLExplore/Algebra/Order/Ring/Abs.lean index ac1b37ac..28ae4f0a 100644 --- a/LMLExplore/Algebra/Order/Ring/Abs.lean +++ b/LMLExplore/Algebra/Order/Ring/Abs.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 LMLExplore contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne +Authors: LMLExplore contributors -/ module diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean index 216cd4a5..7de65526 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 LMLExplore contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne +Authors: LMLExplore contributors -/ module From 3311c92befc3b1b2e3dbf091078c27cc588343bc Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 23:05:44 +0100 Subject: [PATCH 5/5] refactor: inline the klDiv_ne_top_iff wrapper in the KL transport Remove the public `LMLExplore.absolutelyContinuous_of_klDiv_ne_top`; its three uses now call Mathlib's `klDiv_ne_top_iff` directly. Co-Authored-By: Claude Code --- .../InformationTheory/KullbackLeibler/Bernstein.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean index 7de65526..1a809290 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -42,7 +42,6 @@ Apache 2.0), with a new proof of the transport of the mean and sharper constants ## Main statements -* `LMLExplore.absolutelyContinuous_of_klDiv_ne_top`: a finite `KL(μ ‖ ν)` gives `μ ≪ ν`. * `LMLExplore.integral_sub_integral_le_of_klDiv_le`: the one-sided transport, for `f` bounded above by its `ν`-mean plus `b`. * `LMLExplore.abs_integral_sub_integral_le_of_klDiv_le`: the two-sided transport for `f` with @@ -75,10 +74,6 @@ namespace LMLExplore variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {f : α → ℝ} {a b c d : ℝ} -/-- A finite Kullback–Leibler divergence `KL(μ ‖ ν) ≠ ∞` gives `μ ≪ ν`. -/ -theorem absolutelyContinuous_of_klDiv_ne_top {μ ν : Measure α} (h : klDiv μ ν ≠ ∞) : μ ≪ ν := - (klDiv_ne_top_iff.1 h).1 - /-- The Donsker–Varadhan inequality at `g = t (f - ∫ f ∂ν)`, with Bennett's bound on the moment-generating function: for every `t ≥ 0`, `t (∫ f ∂μ - ∫ f ∂ν) - Var_ν(f) ψ_b(t) ≤ a`, with `ψ_b(t) = (exp (t b) - 1 - t b) / b²`. -/ @@ -155,7 +150,7 @@ theorem abs_integral_sub_integral_le_of_klDiv_le (hfm : AEStronglyMeasurable f (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : |∫ x, f x ∂μ - ∫ x, f x ∂ν| ≤ √(2 * Var[f; ν] * a) + (d - c) * a / 3 := by have hμν : μ ≪ ν := - absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) + (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 have hfν : MemLp f 2 ν := memLp_of_bounded hf hfm 2 have hfμ : Integrable f μ := .of_mem_Icc c d (hfm.mono_ac hμν).aemeasurable (hμν.ae_le hf) @@ -187,7 +182,7 @@ theorem variance_le_two_mul_variance_add_of_klDiv_le (hfm : AEStronglyMeasurable (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; ν] ≤ 2 * Var[f; μ] + 8 / 3 * (d - c) ^ 2 * a := by have hμν : μ ≪ ν := - absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) + (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 have hfμ : ∀ᵐ x ∂μ, f x ∈ Set.Icc c d := hμν.ae_le hf have hm : μ[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc (hfm.mono_ac hμν).aemeasurable hfμ @@ -213,7 +208,7 @@ theorem variance_le_two_mul_variance_add_of_klDiv_le' (hfm : AEStronglyMeasurabl (hf : ∀ᵐ x ∂ν, f x ∈ Set.Icc c d) (ha : 0 ≤ a) (h : klDiv μ ν ≤ ENNReal.ofReal a) : Var[f; μ] ≤ 2 * Var[f; ν] + 5 / 6 * (d - c) ^ 2 * a := by have hμν : μ ≪ ν := - absolutelyContinuous_of_klDiv_ne_top (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h) + (klDiv_ne_top_iff.1 (ne_top_of_le_ne_top ENNReal.ofReal_ne_top h)).1 have hm : ν[f] ∈ Set.Icc c d := integral_mem_Icc_of_ae_mem_Icc hfm.aemeasurable hf -- the square `g = (f - ∫ f ∂ν) ^ 2` has values in `[0, (d - c) ^ 2]` have hg : ∀ᵐ x ∂ν, (f x - ν[f]) ^ 2 ∈ Set.Icc 0 ((d - c) ^ 2) :=