diff --git a/LMLExplore/Algebra/Order/Ring/Abs.lean b/LMLExplore/Algebra/Order/Ring/Abs.lean new file mode 100644 index 00000000..28ae4f0a --- /dev/null +++ b/LMLExplore/Algebra/Order/Ring/Abs.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +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 9456f6b0..45373755 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 ec5e4520..1fd7a26b 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Exp.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Exp.lean @@ -52,7 +52,8 @@ increases with the argument: `x ↦ (exp x - 1 - x) / x ^ 2` is monotone on `[0, `exp (l x) ≤ 1 + l x + ψ x ^ 2` with `ψ = (exp (l b) - 1 - l b) / b ^ 2` [BLM13, proof of Theorem 2.9], the one-step bound behind the inequalities of Bennett, Bernstein and Freedman. Tau Ceti's `Real.exp_le_one_add_add_sq_div_of_le`, which gives -`exp x - 1 - x ≤ x ^ 2 / (2 (1 - x / 3))` for `0 ≤ x < 3`, turns these into Bernstein's form. +`exp x - 1 - x ≤ x ^ 2 / (2 (1 - x / 3))` for `0 ≤ x < 3`, turns these into Bernstein's form, +which 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 @@ -83,6 +84,8 @@ lower bound for linear bandits on the unit ball [LS, Theorem 24.2]. `[0, ∞)`. * `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.exists_pos_le_mul_sqrt_add_sub_mul_exp_sub_one_sub`: the closed-form inversion of the + 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.exp_neg_le_one_sub_add_sq`: `exp (-x) ≤ 1 - x + x ^ 2` for `x ≥ -1`. * `Real.card_mul_exp_sum_div_card_le_sum_exp`: `#s exp ((∑ i ∈ s, x i) / #s) ≤ ∑ i ∈ s, exp (x i)`. @@ -301,6 +304,42 @@ theorem monotoneOn_exp_sub_one_sub_id_div_sq : · refine hasSum_le (fun j ↦ ?_) (hseries u hu') (hseries v (hu'.trans_le huv)) gcongr +/-- **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 Tau Ceti's `exp_le_one_add_add_sq_div_of_le` 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 + linarith [exp_le_one_add_add_sq_div_of_le le_rfl (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 new file mode 100644 index 00000000..1a809290 --- /dev/null +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernstein.lean @@ -0,0 +1,227 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.Moments.Variance +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 +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] +(`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.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 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 + 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 +`∫ 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 := 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 + (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 := + 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 _ 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 + 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 := 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 _ 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 + 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/Bernstein.lean b/LMLExplore/Probability/Moments/Bernstein.lean index 4bcc39ce..0b58b758 100644 --- a/LMLExplore/Probability/Moments/Bernstein.lean +++ b/LMLExplore/Probability/Moments/Bernstein.lean @@ -32,7 +32,8 @@ inequality. Since `ψ_b(t) ≤ t ^ 2 / (2 (1 - t b / 3))` for `t b < 3` (Tau Ceti's `Real.exp_le_one_add_add_sq_div_of_le`), `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 @@ -228,37 +229,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 - linarith [exp_le_one_add_add_sq_div_of_le le_rfl (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 dca6ee35..03db15fe 100644 --- a/LMLExplore/Probability/Moments/Variance.lean +++ b/LMLExplore/Probability/Moments/Variance.lean @@ -8,6 +8,8 @@ module public import Mathlib.Probability.Kernel.MeasurableIntegral public import Mathlib.Probability.Moments.Variance import Mathlib.Algebra.QuadraticDiscriminant +import LMLExplore.Algebra.Order.Ring.Abs +import LMLExplore.Analysis.Convex.Integral /-! # Variances under a kernel, and of bounded random variables @@ -28,6 +30,14 @@ 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]. 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 * `Measurable.variance_kernel`: `b ↦ Var[X; η b]` is measurable. @@ -40,6 +50,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 +165,85 @@ 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 := integral_mem_Icc_of_ae_mem_Icc 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 := 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) := 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] + 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