From 4072602e0dbfd7ac3d32fa9b4c8b63b753ac7342 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:16:07 +0100 Subject: [PATCH 1/3] feat: the bipolar rate equals the smallest relative entropy to the null under lower semicontinuity [RR26, Theorem 4.1] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If the smallest relative entropy to the null is lower semicontinuous at `Q` for the topology generated by the integrals of bounded measurable functions, in the sense of neighbourhoods, then `bipolarRate Q S = ⨅ P ∈ S, klDiv Q P` (EValues roadmap, Layer 6.1). The proof is a Sanov-type bound for empirical averages under an i.i.d. law, from the superadditivity of the relative entropy over coordinates, and the weak law of large numbers under the alternative. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/BipolarRate/Semicontinuity.lean | 429 ++++++++++++++++++ 1 file changed, 429 insertions(+) create mode 100644 LMLExplore/EValues/BipolarRate/Semicontinuity.lean diff --git a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean new file mode 100644 index 00000000..dced89ec --- /dev/null +++ b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean @@ -0,0 +1,429 @@ +/- +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 LMLExplore.EValues.BipolarRate +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.ConditionalProbability +public import Mathlib.Probability.Moments.Variance +public import Statlib.Divergence.KullbackLeibler.Basic +public import Statlib.ForMathlib.MeasureTheory.Integral.Pi + +/-! +# The bipolar rate equals the smallest relative entropy under lower semicontinuity + +The bipolar rate `bipolarRate Q S` of a probability measure `Q` against an i.i.d. null `S` is at +most the smallest relative entropy `⨅ P ∈ S, klDiv Q P` from `Q` to the null +(`ProbabilityTheory.bipolarRate_le_iInf_klDiv`). This file proves that they are equal when the +smallest relative entropy to the null, as a function of the law, is lower semicontinuous at `Q` +for the topology generated by the integrals of bounded measurable functions [RR26, Theorem 4.1]. +That topology is finer than the topology of weak convergence, so lower semicontinuity for weak +convergence, which [RR26] assumes on a Polish space, is a special case; no topology on the +sample space is needed here. + +The semicontinuity is stated with neighbourhoods: for every `c` below the smallest relative +entropy from `Q` to `S`, there are finitely many bounded measurable functions `f i` and `ε > 0` +such that every probability measure `R` whose integrals of the `f i` are within `ε` of those of +`Q` is at relative entropy at least `c` from every member of `S`. + +## Main statements + +* `ProbabilityTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on `Fin n → 𝓧` to + an i.i.d. law is at least the sum of the relative entropies of its marginals. +* `ProbabilityTheory.klDiv_cond_le`: the relative entropy from `μ` conditioned on `A` to `μ` is at + most `log (1 / μ A)`. +* `ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`: a Sanov-type bound for the empirical + averages of finitely many bounded functions under an i.i.d. law. +* `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le`: the bipolar rate + equals the smallest relative entropy to the null under the semicontinuity above. + +## Implementation notes + +The lower bound is a Sanov-type argument with blocks of length one. The probability under `P ^ m` +that the empirical averages of the test functions lie in the neighbourhood is at most +`exp (- m c)`: condition `P ^ m` on that event, and use the superadditivity of the relative +entropy over the coordinates and its convexity. The indicator of the event, multiplied by +`exp (m c)`, is then an `m`-sample e-variable, and the weak law of large numbers under `Q ^ m`, +from Chebyshev's inequality, gives its expected logarithm. + +## References + +* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. +-/ + +public section + +open MeasureTheory InformationTheory Filter +open scoped ENNReal NNReal Topology + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-! ### Bounds on the bipolar rate -/ + +/-- The bipolar rate is at most the smallest relative entropy from `Q` to the null, with the +infimum taken in `EReal`: the form of `bipolarRate_le_iInf_klDiv` used in this file. -/ +lemma bipolarRate_le_iInf_coe_klDiv (Q : Measure 𝓧) [IsProbabilityMeasure Q] (S : Set (Measure 𝓧)) + (hS : ∀ P ∈ S, IsProbabilityMeasure P) : + bipolarRate Q S ≤ ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) := + le_iInf₂ fun P hP ↦ have := hS P hP; bipolarRate_le_klDiv Q hP + +/-- A real lower bound on the growth of `n + 1` observations, divided by `n + 1`, that converges +to `L` gives the lower bound `L` on the bipolar rate. -/ +lemma le_bipolarRate_of_tendsto {Q : Measure 𝓧} {S : Set (Measure 𝓧)} {r : ℕ → ℝ} {L : ℝ} + (hr : ∀ n, (r n : EReal) ≤ maxLogGrowth Q S (n + 1)) + (hlim : Tendsto (fun n : ℕ ↦ r n / (n + 1)) atTop (𝓝 L)) : + (L : EReal) ≤ bipolarRate Q S := by + rw [bipolarRate_def] + refine le_of_tendsto' (EReal.tendsto_coe.2 hlim) fun n ↦ ?_ + refine le_trans ?_ (le_iSup _ n) + have h : ((r n / (n + 1) : ℝ) : EReal) = (r n : EReal) / ((n + 1 : ℕ) : EReal) := by + rw [EReal.coe_div] + norm_cast + rw [h] + exact EReal.div_le_div_right_of_nonneg (by positivity) (hr n) + +/-! ### Relative entropy of marginals and of conditional laws -/ + +/-- The relative entropy to a product law is at least the sum of the relative entropies of the +two marginals. -/ +lemma klDiv_fst_add_klDiv_snd_le {𝓨 : Type*} {m𝓨 : MeasurableSpace 𝓨} (R : Measure (𝓧 × 𝓨)) + [IsProbabilityMeasure R] (P : Measure 𝓧) (P' : Measure 𝓨) [IsProbabilityMeasure P] + [IsProbabilityMeasure P'] : + klDiv R.fst P + klDiv R.snd P' ≤ klDiv R (P.prod P') := by + have h := maxUtility_fst_add_maxUtility_snd_le R (S := {P}) (T := {P'}) + (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) + (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) + rwa [Set.image2_singleton, maxUtility_singleton_eq_klDiv, maxUtility_singleton_eq_klDiv, + maxUtility_singleton_eq_klDiv, ← EReal.coe_ennreal_add, + EReal.coe_ennreal_le_coe_ennreal_iff] at h + +/-- The relative entropy from a law on `𝓧 ^ n` to an i.i.d. law is at least the sum of the +relative entropies of its marginals. -/ +lemma sum_klDiv_map_eval_le (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) + (μ : Measure (Fin n → 𝓧)) [IsProbabilityMeasure μ] : + ∑ j, klDiv (μ.map fun x ↦ x j) P ≤ klDiv μ (Measure.pi fun _ ↦ P) := by + induction n with + | zero => simp + | succ n ih => + set e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) ↦ 𝓧) 0 + set R := μ.map e + have hpi : (Measure.pi fun _ : Fin (n + 1) ↦ P).map e = + P.prod (Measure.pi fun _ : Fin n ↦ P) := + (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) ↦ P) 0).map_eq + have hKL : klDiv R (P.prod (Measure.pi fun _ : Fin n ↦ P)) = + klDiv μ (Measure.pi fun _ ↦ P) := by + rw [← hpi] + refine le_antisymm (klDiv_map_le _ _ e.measurable) ?_ + have h := klDiv_map_le R ((Measure.pi fun _ : Fin (n + 1) ↦ P).map e) e.symm.measurable + rwa [e.map_symm_map, e.map_symm_map] at h + have hfst : R.fst = μ.map fun x ↦ x 0 := by + rw [Measure.fst, Measure.map_map measurable_fst e.measurable] + rfl + have hsnd : R.snd = μ.map fun x j ↦ x j.succ := by + rw [Measure.snd, Measure.map_map measurable_snd e.measurable] + rfl + have hmarg (j : Fin n) : R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x j.succ := by + rw [hsnd, Measure.map_map (by fun_prop) (by fun_prop)] + rfl + calc ∑ j, klDiv (μ.map fun x ↦ x j) P + _ = klDiv R.fst P + ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) P := by + rw [Fin.sum_univ_succ, hfst] + simp_rw [hmarg] + _ ≤ klDiv R.fst P + klDiv R.snd (Measure.pi fun _ : Fin n ↦ P) := by + gcongr + exact ih R.snd + _ ≤ klDiv R (P.prod (Measure.pi fun _ : Fin n ↦ P)) := klDiv_fst_add_klDiv_snd_le R P _ + _ = klDiv μ (Measure.pi fun _ ↦ P) := hKL + +/-- The relative entropy from the law `μ` conditioned on `A` to `μ` is at most `log (1 / μ A)`. -/ +lemma klDiv_cond_le {μ : Measure 𝓧} [IsProbabilityMeasure μ] {A : Set 𝓧} (hμA : μ A ≠ 0) : + ((klDiv (μ[|A]) μ : ℝ≥0∞) : EReal) ≤ ENNReal.log (μ A)⁻¹ := by + have := cond_isProbabilityMeasure hμA + rw [← maxUtility_singleton_eq_klDiv] + refine iSup₂_le fun X hX ↦ ?_ + calc ∫ᵉ x, (logUtility ∘ X) x ∂μ[|A] + _ ≤ logUtility (∫⁻ x, X x ∂μ[|A]) := + Utility.eintegral_le_map logUtility hX.measurable.aemeasurable + _ ≤ ENNReal.log (μ A)⁻¹ := by + refine ENNReal.log_monotone ?_ + rw [ProbabilityTheory.cond, lintegral_smul_measure, smul_eq_mul] + calc (μ A)⁻¹ * ∫⁻ x, X x ∂μ.restrict A + _ ≤ (μ A)⁻¹ * 1 := by + gcongr + exact (setLIntegral_le_lintegral A X).trans + ((hX.lintegral_le_measure_univ μ rfl).trans_eq measure_univ) + _ = (μ A)⁻¹ := mul_one _ + +/-! ### A Sanov-type bound and the law of large numbers -/ + +/-- The tuples whose empirical averages of the measurable functions `f i` are within `ε` of the +`a i` form a measurable set. -/ +lemma measurableSet_setOf_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} + (hf : ∀ i, Measurable (f i)) (a : Fin k → ℝ) (ε : ℝ) (m : ℕ) : + MeasurableSet {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} := by + simp only [Set.ofPred_forall] + exact MeasurableSet.iInter fun i ↦ measurableSet_le (continuous_abs.measurable.comp + (((Finset.measurable_sum _ fun j _ ↦ (hf i).comp (measurable_pi_apply j)).div_const _).sub_const + _)) measurable_const + +/-- The integral against the average of the marginals of `μ` is the integral of the empirical +average against `μ`. -/ +lemma integral_sum_smul_map_eval {m : ℕ} (μ : Measure (Fin m → 𝓧)) + [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) : + ∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) = + ∫ x, (∑ j, g (x j)) / m ∂μ := by + have hint (ν : Measure 𝓧) [IsFiniteMeasure ν] : Integrable g ν := + Integrable.of_bound hg.aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC x) + rw [integral_finsetSum_measure fun j _ ↦ (hint _).smul_measure ENNReal.coe_ne_top] + have hj (j : Fin m) : ∫ x, g x ∂(μ.map fun x ↦ x j) = ∫ x, g (x j) ∂μ := + integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable + simp_rw [integral_smul_measure, hj] + have hs : ∫ x, ∑ j, g (x j) ∂μ = ∑ j, ∫ x, g (x j) ∂μ := + integral_finsetSum _ fun j _ ↦ Integrable.of_bound + (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC _) + rw [integral_div, hs] + simp [div_eq_inv_mul, Finset.mul_sum] + +/-- **Sanov-type bound.** If every law `R` whose integrals of the bounded functions `f i` are +within `ε` of `a i` is at relative entropy at least `c ≥ 0` from `P`, then the probability under +`P ^ m` that the empirical averages of the `f i` are within `ε` of the `a i` is at most +`exp (- m c)`. -/ +lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (hf : ∀ i, Measurable (f i)) + {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) {a : Fin k → ℝ} {ε c : ℝ} (hc : 0 ≤ c) + {P : Measure 𝓧} [IsProbabilityMeasure P] + (hU : ∀ R : Measure 𝓧, IsProbabilityMeasure R → (∀ i, |∫ x, f i x ∂R - a i| ≤ ε) → + ENNReal.ofReal c ≤ klDiv R P) {m : ℕ} (hm : m ≠ 0) : + ENNReal.ofReal (Real.exp (m * c)) * + (Measure.pi fun _ : Fin m ↦ P) {x | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} ≤ 1 := by + set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} + set Pm := Measure.pi fun _ : Fin m ↦ P + have hA : MeasurableSet A := measurableSet_setOf_forall_abs_avg_sub_le hf a ε m + rcases eq_or_ne (Pm A) 0 with h0 | h0 + · simp [h0] + set μ := Pm[|A] + have : IsProbabilityMeasure μ := cond_isProbabilityMeasure h0 + have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm + set w : Fin m → ℝ≥0 := fun _ ↦ (m : ℝ≥0)⁻¹ + have hw : ∑ j, w j = 1 := by + simp [w, Finset.card_univ, mul_inv_cancel₀ (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0)] + set R := ∑ j, (w j : ℝ≥0∞) • μ.map fun x ↦ x j + have hR : IsProbabilityMeasure R := ⟨by + simp [R, w, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), + ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m)]⟩ + have hRU (i : Fin k) : |∫ x, f i x ∂R - a i| ≤ ε := by + rw [integral_sum_smul_map_eval μ (hf i) (hfC i)] + have hint : Integrable (fun x : Fin m → 𝓧 ↦ (∑ j, f i (x j)) / m) μ := + ((integrable_finsetSum _ fun j _ ↦ Integrable.of_bound + ((hf i).comp (measurable_pi_apply j)).aestronglyMeasurable (C i) + (Eventually.of_forall fun x ↦ hfC i _))).div_const _ + have heq : ∫ x, (∑ j, f i (x j)) / m ∂μ - a i = ∫ x, ((∑ j, f i (x j)) / m - a i) ∂μ := by + rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul] + rw [heq, ← Real.norm_eq_abs] + refine (norm_integral_le_of_norm_le_const (C := ε) ?_).trans (by simp) + filter_upwards [ae_cond_mem hA] with x hx + simpa [Real.norm_eq_abs] using hx i + have h1 : (m : ℝ≥0∞) * ENNReal.ofReal c ≤ klDiv μ Pm := by + calc (m : ℝ≥0∞) * ENNReal.ofReal c + _ ≤ m * klDiv R P := by gcongr; exact hU R hR hRU + _ ≤ m * ∑ j, (w j : ℝ≥0∞) * klDiv (μ.map fun x ↦ x j) P := by + gcongr + exact klDiv_sum_smul_left_le hw + _ = ∑ j, klDiv (μ.map fun x ↦ x j) P := by + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ ↦ ?_ + rw [← mul_assoc, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), + ENNReal.coe_natCast, ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m), one_mul] + _ ≤ klDiv μ Pm := sum_klDiv_map_eval_le P m μ + rw [← ENNReal.le_inv_iff_mul_le, ← ENNReal.log_le_log_iff, + ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] + calc ((m * c : ℝ) : EReal) + _ = ((ENNReal.ofReal (m * c) : ℝ≥0∞) : EReal) := by + rw [EReal.coe_ennreal_ofReal, max_eq_left (by positivity)] + _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by + rw [ENNReal.ofReal_mul (Nat.cast_nonneg _), ENNReal.ofReal_natCast] + _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1 + _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0 + +/-- **Weak law of large numbers**, by Chebyshev's inequality: the probability that the empirical +average of a function bounded by `C` deviates by more than `ε` from its mean is at most +`C ^ 2 / (m ε ^ 2)`. -/ +lemma measure_pi_lt_abs_avg_sub_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) + (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : + (Measure.pi fun _ : Fin m ↦ Q) {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} ≤ + ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by + set Qm := Measure.pi fun _ : Fin m ↦ Q + set X : (Fin m → 𝓧) → ℝ := fun x ↦ ∑ j, g (x j) with hX_def + have hm' : (0 : ℝ) < m := Nat.cast_pos.2 (Nat.pos_of_ne_zero hm) + have hgL (j : Fin m) : MemLp (fun x : Fin m → 𝓧 ↦ g (x j)) 2 Qm := + MemLp.of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C + (Eventually.of_forall fun x ↦ hgC _) + have hXL : MemLp X 2 Qm := memLp_finsetSum _ fun j _ ↦ hgL j + have hEX : ∫ x, X x ∂Qm = m * ∫ y, g y ∂Q := by + have hj (j : Fin m) : ∫ x, g (x j) ∂Qm = ∫ y, g y ∂Q := by + rw [← integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable] + congr 1 + exact (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq + rw [integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two] + simp [hj] + have hVar : Var[X; Qm] ≤ m * C ^ 2 := by + have h := variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) + fun _ ↦ MemLp.of_bound hg.aestronglyMeasurable C (Eventually.of_forall hgC) + have hX : X = ∑ j : Fin m, fun x : Fin m → 𝓧 ↦ g (x j) := by + ext x + simp [X] + rw [hX, h, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] + gcongr + have hb := variance_le_sq_of_bounded (μ := Q) (a := -C) (b := C) + (Eventually.of_forall fun x ↦ abs_le.1 (hgC x)) hg.aemeasurable + convert hb using 1 + ring + calc Qm {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} + _ ≤ Qm {x | m * ε ≤ |X x - ∫ x, X x ∂Qm|} := by + refine measure_mono fun x hx ↦ ?_ + simp only [Set.mem_ofPred_eq] at hx ⊢ + have h : (∑ j, g (x j)) / m - ∫ y, g y ∂Q = (X x - ∫ x, X x ∂Qm) / m := by + rw [hEX, hX_def] + field_simp + rw [h, abs_div, abs_of_pos hm', lt_div_iff₀ hm'] at hx + linarith + _ ≤ ENNReal.ofReal (Var[X; Qm] / (m * ε) ^ 2) := + meas_ge_le_variance_div_sq hXL (by positivity) + _ ≤ ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by + refine ENNReal.ofReal_le_ofReal ?_ + calc Var[X; Qm] / (m * ε) ^ 2 + _ ≤ m * C ^ 2 / (m * ε) ^ 2 := by gcongr + _ = C ^ 2 / (m * ε ^ 2) := by field_simp + +/-- The e-variable `1/2 + (1/2) e ^ t 1_A`, valid when `e ^ t P (A) ≤ 1` for every member `P` of +the null, gives the lower bound `t Q (A) - log 2` on the growth of `m` observations. -/ +lemma le_maxLogGrowth_of_ofReal_exp_mul_le_one (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) {m : ℕ} + {A : Set (Fin m → 𝓧)} (hA : MeasurableSet A) {t : ℝ} + (hP : ∀ P ∈ S, ENNReal.ofReal (Real.exp t) * (Measure.pi fun _ : Fin m ↦ P) A ≤ 1) : + ((t * (Measure.pi fun _ : Fin m ↦ Q).real A - Real.log 2 : ℝ) : EReal) ≤ + maxLogGrowth Q S m := by + set Qm := Measure.pi fun _ : Fin m ↦ Q + set b := ENNReal.ofReal (Real.exp t) + set X : (Fin m → 𝓧) → ℝ≥0∞ := fun x ↦ 2⁻¹ + 2⁻¹ * A.indicator (fun _ ↦ b) x + have hXm : Measurable X := measurable_const.add (measurable_const.mul + (measurable_const.indicator hA)) + have hX : IsEVar X ((fun P ↦ Measure.pi fun _ : Fin m ↦ P) '' S) := by + refine IsEVar.of_lintegral_le_one ?_ hXm ?_ + · rintro _ ⟨P, hP, rfl⟩ + have := hS P hP + infer_instance + · rintro _ ⟨P, hPS, rfl⟩ + have := hS P hPS + calc ∫⁻ x, X x ∂(Measure.pi fun _ : Fin m ↦ P) + _ = 2⁻¹ + 2⁻¹ * (b * (Measure.pi fun _ : Fin m ↦ P) A) := by + simp only [X] + rw [lintegral_add_right _ ((measurable_const.indicator hA).const_mul _), + lintegral_const, measure_univ, mul_one, + lintegral_const_mul _ (measurable_const.indicator hA), lintegral_indicator_const hA] + _ ≤ 2⁻¹ + 2⁻¹ * 1 := by gcongr; exact hP P hPS + _ = 1 := by rw [mul_one, ENNReal.inv_two_add_inv_two] + set g : (Fin m → 𝓧) → ℝ := fun x ↦ A.indicator (fun _ ↦ t) x - Real.log 2 + have hg (x : Fin m → 𝓧) : ENNReal.ofReal (Real.exp (g x)) ≤ X x := by + by_cases hx : x ∈ A + · simp only [g, X, Set.indicator_of_mem hx] + rw [Real.exp_sub, Real.exp_log two_pos, ENNReal.ofReal_div_of_pos two_pos, + ENNReal.ofReal_ofNat, div_eq_mul_inv, mul_comm] + exact le_add_self + · simp only [g, X, Set.indicator_of_notMem hx, zero_sub, Real.exp_neg, Real.exp_log two_pos, + mul_zero, add_zero] + rw [ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat] + have hgi : Integrable g Qm := ((integrable_const t).indicator hA).sub (integrable_const _) + calc ((t * Qm.real A - Real.log 2 : ℝ) : EReal) + _ = ∫ᵉ x, (g x : EReal) ∂Qm := by + rw [eintegral_eq_integral hgi, integral_sub ((integrable_const t).indicator hA) + (integrable_const _), integral_indicator_const _ hA, integral_const, probReal_univ, + smul_eq_mul, one_smul, mul_comm] + _ ≤ ∫ᵉ x, (logUtility ∘ X) x ∂Qm := eintegral_mono fun x ↦ by + calc (g x : EReal) + _ = ENNReal.log (ENNReal.ofReal (Real.exp (g x))) := by + rw [ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] + _ ≤ (logUtility ∘ X) x := ENNReal.log_monotone (hg x) + _ ≤ maxLogGrowth Q S m := by + rw [maxLogGrowth_def] + exact hX.eintegral_le_maxUtility _ _ + +/-- If the smallest relative entropy to `S` is lower semicontinuous at `Q` for the topology of +integrals of bounded measurable functions, in the sense of neighbourhoods, then the bipolar rate +of `Q` against `S` equals the smallest relative entropy from `Q` to `S` [RR26, Theorem 4.1]. The +test functions need only be bounded, by any constant, and measurable: no topology on `𝓧` is +used, and lower semicontinuity for weak convergence is a special case. -/ +theorem bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le (Q : Measure 𝓧) + [IsProbabilityMeasure Q] (S : Set (Measure 𝓧)) (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (h : ∀ c : EReal, c < ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) → + ∃ (k : ℕ) (f : Fin k → 𝓧 → ℝ) (ε : ℝ), 0 < ε ∧ (∀ i, Measurable (f i)) ∧ + (∀ i, ∃ C, ∀ x, |f i x| ≤ C) ∧ ∀ R : Measure 𝓧, IsProbabilityMeasure R → + (∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) → + c ≤ ⨅ P ∈ S, ((klDiv R P : ℝ≥0∞) : EReal)) : + bipolarRate Q S = ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) := by + refine le_antisymm (bipolarRate_le_iInf_coe_klDiv Q S hS) + (le_of_forall_lt_imp_le_of_dense fun c hc ↦ ?_) + rcases le_or_gt c 0 with hc0 | hc0 + · exact hc0.trans (bipolarRate_nonneg Q S) + obtain ⟨k, f, ε, hε, hfm, hfC, hU⟩ := h c hc + choose C hC using hfC + obtain ⟨c, rfl⟩ : ∃ r : ℝ, (r : EReal) = c := + ⟨c.toReal, EReal.coe_toReal hc.ne_top (ne_bot_of_gt hc0)⟩ + have hc0' : 0 < c := by exact_mod_cast hc0 + -- every law in the neighbourhood is at relative entropy at least `c` from every null law + have hU' (P : Measure 𝓧) (hP : P ∈ S) (R : Measure 𝓧) (hR : IsProbabilityMeasure R) + (hRf : ∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) : ENNReal.ofReal c ≤ klDiv R P := by + have := (hU R hR hRf).trans (iInf₂_le P hP) + rwa [← max_eq_left hc0'.le, ← EReal.coe_ennreal_ofReal, + EReal.coe_ennreal_le_coe_ennreal_iff] at this + set A : ∀ m : ℕ, Set (Fin m → 𝓧) := + fun m ↦ {x | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} with hA_def + set D := ∑ i, C i ^ 2 / ε ^ 2 + -- the law of large numbers under `Q` + have hQA (m : ℕ) (hm : m ≠ 0) : 1 - D / m ≤ (Measure.pi fun _ : Fin m ↦ Q).real (A m) := by + have hcompl : (A m)ᶜ = ⋃ i, {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} := by + ext x + simp [A] + have hle : (Measure.pi fun _ : Fin m ↦ Q) (A m)ᶜ ≤ ENNReal.ofReal (D / m) := by + rw [hcompl] + refine (measure_iUnion_fintype_le _ _).trans ?_ + calc ∑ i, (Measure.pi fun _ : Fin m ↦ Q) + {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} + _ ≤ ∑ i, ENNReal.ofReal (C i ^ 2 / (m * ε ^ 2)) := + Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_avg_sub_le (hfm i) (hC i) Q hε hm + _ = ENNReal.ofReal (D / m) := by + rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦ by positivity] + congr 1 + simp only [D, Finset.sum_div] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + field_simp + have h := ENNReal.toReal_le_of_le_ofReal (by positivity) hle + rw [← measureReal_def, probReal_compl_eq_one_sub + (measurableSet_setOf_forall_abs_avg_sub_le hfm _ ε m)] at h + linarith + refine le_bipolarRate_of_tendsto (r := fun n ↦ (n + 1) * c * (1 - D / (n + 1)) - Real.log 2) + (fun n ↦ ?_) ?_ + · have hsan (P : Measure 𝓧) (hP : P ∈ S) := + have := hS P hP + ofReal_exp_mul_measure_pi_le_one hfm hC hc0'.le (hU' P hP) (m := n + 1) n.succ_ne_zero + refine le_trans ?_ (le_maxLogGrowth_of_ofReal_exp_mul_le_one Q hS + (measurableSet_setOf_forall_abs_avg_sub_le hfm _ ε (n + 1)) hsan) + have h := hQA (n + 1) n.succ_ne_zero + simp only [hA_def] at h + refine EReal.coe_le_coe_iff.2 ?_ + have hnc : 0 ≤ ((n + 1 : ℕ) : ℝ) * c := by positivity + have hn1 : ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1 := by push_cast; ring + rw [hn1] at hnc h ⊢ + nlinarith + · have h0 := tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ) + have h1 := (tendsto_const_nhds (x := c)).sub (h0.const_mul (c * D + Real.log 2)) + rw [mul_zero, sub_zero] at h1 + refine h1.congr fun n ↦ ?_ + field_simp + ring + +end ProbabilityTheory From 85f1b1359598798a0d48bd62d24d4c974ca92160 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:46:35 +0100 Subject: [PATCH 2/3] refactor: move generic KL and empirical-average lemmas to topic files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address review on the bipolar-rate semicontinuity PR: - move `klDiv_fst_add_klDiv_snd_le` and `sum_klDiv_map_eval_le` (now for any product `Measure.pi P`) to `InformationTheory/KullbackLeibler/Pi.lean`, and `klDiv_cond_le` to `InformationTheory/KullbackLeibler/Cond.lean`, in namespace `InformationTheory`; - move the empirical-average lemmas, the Sanov-type bound (crediting Csiszár [Csi84]) and the weak law of large numbers to `Probability/LargeDeviations/EmpiricalAverage.lean`, extracting `isProbabilityMeasure_sum_smul_map_eval`, `abs_integral_sum_smul_map_eval_sub_le` and `one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le`; - move `le_bipolarRate_of_tendsto` to `EValues/BipolarRate.lean`; - delete `bipolarRate_le_iInf_coe_klDiv` and state the main theorem with the `ℝ≥0∞` infimum of `bipolarRate_le_iInf_klDiv`; - replace the `rfl` closes of the marginal-law identities by simp lemmas; - correct the implementation notes on the mixture e-variable. Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate.lean | 17 + .../EValues/BipolarRate/Semicontinuity.lean | 319 ++---------------- .../KullbackLeibler/Cond.lean | 54 +++ .../InformationTheory/KullbackLeibler/Pi.lean | 92 +++++ .../LargeDeviations/EmpiricalAverage.lean | 244 ++++++++++++++ 5 files changed, 433 insertions(+), 293 deletions(-) create mode 100644 LMLExplore/InformationTheory/KullbackLeibler/Cond.lean create mode 100644 LMLExplore/InformationTheory/KullbackLeibler/Pi.lean create mode 100644 LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean diff --git a/LMLExplore/EValues/BipolarRate.lean b/LMLExplore/EValues/BipolarRate.lean index f2ca48fd..ed8234a6 100644 --- a/LMLExplore/EValues/BipolarRate.lean +++ b/LMLExplore/EValues/BipolarRate.lean @@ -47,6 +47,8 @@ else: no domination, convexity or compactness. * `ProbabilityTheory.maxLogGrowth_le_mul_klDiv`, `ProbabilityTheory.bipolarRate_le_iInf_klDiv`: the bipolar rate is at most the smallest relative entropy from `Q₁` to the null [RR26, proof of Theorem 4.1]. +* `ProbabilityTheory.le_bipolarRate_of_tendsto`: a lower bound on the bipolar rate from real lower + bounds on `maxLogGrowth Q₁ S₁ (n + 1)` whose quotients by `n + 1` converge. ## References @@ -224,4 +226,19 @@ theorem bipolarRate_le_iInf_klDiv (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q rw [← EReal.toENNReal_coe (x := klDiv Q₁ P)] exact EReal.toENNReal_le_toENNReal (bipolarRate_le_klDiv Q₁ hP) +/-- A real lower bound on the growth of `n + 1` observations, divided by `n + 1`, that converges +to `L` gives the lower bound `L` on the bipolar rate. -/ +lemma le_bipolarRate_of_tendsto {r : ℕ → ℝ} {L : ℝ} + (hr : ∀ n, (r n : EReal) ≤ maxLogGrowth Q₁ S₁ (n + 1)) + (hlim : Tendsto (fun n : ℕ ↦ r n / (n + 1)) atTop (𝓝 L)) : + (L : EReal) ≤ bipolarRate Q₁ S₁ := by + rw [bipolarRate_def] + refine le_of_tendsto' (EReal.tendsto_coe.2 hlim) fun n ↦ ?_ + refine le_trans ?_ (le_iSup _ n) + have h : ((r n / (n + 1) : ℝ) : EReal) = (r n : EReal) / ((n + 1 : ℕ) : EReal) := by + rw [EReal.coe_div] + norm_cast + rw [h] + exact EReal.div_le_div_right_of_nonneg (by positivity) (hr n) + end ProbabilityTheory diff --git a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean index dced89ec..fc565f90 100644 --- a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean +++ b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean @@ -6,11 +6,7 @@ Authors: LMLExplore contributors module public import LMLExplore.EValues.BipolarRate -public import Mathlib.InformationTheory.KullbackLeibler.Basic -public import Mathlib.Probability.ConditionalProbability -public import Mathlib.Probability.Moments.Variance -public import Statlib.Divergence.KullbackLeibler.Basic -public import Statlib.ForMathlib.MeasureTheory.Integral.Pi +public import LMLExplore.Probability.LargeDeviations.EmpiricalAverage /-! # The bipolar rate equals the smallest relative entropy under lower semicontinuity @@ -31,27 +27,27 @@ such that every probability measure `R` whose integrals of the `f i` are within ## Main statements -* `ProbabilityTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on `Fin n → 𝓧` to - an i.i.d. law is at least the sum of the relative entropies of its marginals. -* `ProbabilityTheory.klDiv_cond_le`: the relative entropy from `μ` conditioned on `A` to `μ` is at - most `log (1 / μ A)`. -* `ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`: a Sanov-type bound for the empirical - averages of finitely many bounded functions under an i.i.d. law. +* `ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`: the lower bound on the growth of + `m` observations given by the e-variable `1/2 + (1/2) exp t 1_A`. * `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le`: the bipolar rate equals the smallest relative entropy to the null under the semicontinuity above. ## Implementation notes The lower bound is a Sanov-type argument with blocks of length one. The probability under `P ^ m` -that the empirical averages of the test functions lie in the neighbourhood is at most -`exp (- m c)`: condition `P ^ m` on that event, and use the superadditivity of the relative -entropy over the coordinates and its convexity. The indicator of the event, multiplied by -`exp (m c)`, is then an `m`-sample e-variable, and the weak law of large numbers under `Q ^ m`, -from Chebyshev's inequality, gives its expected logarithm. +of the event `A` that the empirical averages of the test functions lie in the neighbourhood is at +most `exp (- m c)` (`ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`, Csiszár's conditioning +argument [Csi84]): condition `P ^ m` on that event, and use the superadditivity of the relative +entropy over the coordinates and its convexity. The mixture `1/2 + (1/2) exp (m c) 1_A` is then an +`m`-sample e-variable, whose expected logarithm under `Q ^ m` is at least +`m c Q ^ m (A) - log 2`; the weak law of large numbers under `Q ^ m`, from Chebyshev's inequality, +gives `Q ^ m (A) ≥ 1 - D / m` for a constant `D`, so this is at least `m c - O(1)`. ## References * [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. +* [Csi84] I. Csiszár, *Sanov property, generalized I-projection and a conditional limit theorem*, + Ann. Probab. 12 (1984), 768–793. -/ public section @@ -63,242 +59,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-! ### Bounds on the bipolar rate -/ - -/-- The bipolar rate is at most the smallest relative entropy from `Q` to the null, with the -infimum taken in `EReal`: the form of `bipolarRate_le_iInf_klDiv` used in this file. -/ -lemma bipolarRate_le_iInf_coe_klDiv (Q : Measure 𝓧) [IsProbabilityMeasure Q] (S : Set (Measure 𝓧)) - (hS : ∀ P ∈ S, IsProbabilityMeasure P) : - bipolarRate Q S ≤ ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) := - le_iInf₂ fun P hP ↦ have := hS P hP; bipolarRate_le_klDiv Q hP - -/-- A real lower bound on the growth of `n + 1` observations, divided by `n + 1`, that converges -to `L` gives the lower bound `L` on the bipolar rate. -/ -lemma le_bipolarRate_of_tendsto {Q : Measure 𝓧} {S : Set (Measure 𝓧)} {r : ℕ → ℝ} {L : ℝ} - (hr : ∀ n, (r n : EReal) ≤ maxLogGrowth Q S (n + 1)) - (hlim : Tendsto (fun n : ℕ ↦ r n / (n + 1)) atTop (𝓝 L)) : - (L : EReal) ≤ bipolarRate Q S := by - rw [bipolarRate_def] - refine le_of_tendsto' (EReal.tendsto_coe.2 hlim) fun n ↦ ?_ - refine le_trans ?_ (le_iSup _ n) - have h : ((r n / (n + 1) : ℝ) : EReal) = (r n : EReal) / ((n + 1 : ℕ) : EReal) := by - rw [EReal.coe_div] - norm_cast - rw [h] - exact EReal.div_le_div_right_of_nonneg (by positivity) (hr n) - -/-! ### Relative entropy of marginals and of conditional laws -/ - -/-- The relative entropy to a product law is at least the sum of the relative entropies of the -two marginals. -/ -lemma klDiv_fst_add_klDiv_snd_le {𝓨 : Type*} {m𝓨 : MeasurableSpace 𝓨} (R : Measure (𝓧 × 𝓨)) - [IsProbabilityMeasure R] (P : Measure 𝓧) (P' : Measure 𝓨) [IsProbabilityMeasure P] - [IsProbabilityMeasure P'] : - klDiv R.fst P + klDiv R.snd P' ≤ klDiv R (P.prod P') := by - have h := maxUtility_fst_add_maxUtility_snd_le R (S := {P}) (T := {P'}) - (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) - (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) - rwa [Set.image2_singleton, maxUtility_singleton_eq_klDiv, maxUtility_singleton_eq_klDiv, - maxUtility_singleton_eq_klDiv, ← EReal.coe_ennreal_add, - EReal.coe_ennreal_le_coe_ennreal_iff] at h - -/-- The relative entropy from a law on `𝓧 ^ n` to an i.i.d. law is at least the sum of the -relative entropies of its marginals. -/ -lemma sum_klDiv_map_eval_le (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) - (μ : Measure (Fin n → 𝓧)) [IsProbabilityMeasure μ] : - ∑ j, klDiv (μ.map fun x ↦ x j) P ≤ klDiv μ (Measure.pi fun _ ↦ P) := by - induction n with - | zero => simp - | succ n ih => - set e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) ↦ 𝓧) 0 - set R := μ.map e - have hpi : (Measure.pi fun _ : Fin (n + 1) ↦ P).map e = - P.prod (Measure.pi fun _ : Fin n ↦ P) := - (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) ↦ P) 0).map_eq - have hKL : klDiv R (P.prod (Measure.pi fun _ : Fin n ↦ P)) = - klDiv μ (Measure.pi fun _ ↦ P) := by - rw [← hpi] - refine le_antisymm (klDiv_map_le _ _ e.measurable) ?_ - have h := klDiv_map_le R ((Measure.pi fun _ : Fin (n + 1) ↦ P).map e) e.symm.measurable - rwa [e.map_symm_map, e.map_symm_map] at h - have hfst : R.fst = μ.map fun x ↦ x 0 := by - rw [Measure.fst, Measure.map_map measurable_fst e.measurable] - rfl - have hsnd : R.snd = μ.map fun x j ↦ x j.succ := by - rw [Measure.snd, Measure.map_map measurable_snd e.measurable] - rfl - have hmarg (j : Fin n) : R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x j.succ := by - rw [hsnd, Measure.map_map (by fun_prop) (by fun_prop)] - rfl - calc ∑ j, klDiv (μ.map fun x ↦ x j) P - _ = klDiv R.fst P + ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) P := by - rw [Fin.sum_univ_succ, hfst] - simp_rw [hmarg] - _ ≤ klDiv R.fst P + klDiv R.snd (Measure.pi fun _ : Fin n ↦ P) := by - gcongr - exact ih R.snd - _ ≤ klDiv R (P.prod (Measure.pi fun _ : Fin n ↦ P)) := klDiv_fst_add_klDiv_snd_le R P _ - _ = klDiv μ (Measure.pi fun _ ↦ P) := hKL - -/-- The relative entropy from the law `μ` conditioned on `A` to `μ` is at most `log (1 / μ A)`. -/ -lemma klDiv_cond_le {μ : Measure 𝓧} [IsProbabilityMeasure μ] {A : Set 𝓧} (hμA : μ A ≠ 0) : - ((klDiv (μ[|A]) μ : ℝ≥0∞) : EReal) ≤ ENNReal.log (μ A)⁻¹ := by - have := cond_isProbabilityMeasure hμA - rw [← maxUtility_singleton_eq_klDiv] - refine iSup₂_le fun X hX ↦ ?_ - calc ∫ᵉ x, (logUtility ∘ X) x ∂μ[|A] - _ ≤ logUtility (∫⁻ x, X x ∂μ[|A]) := - Utility.eintegral_le_map logUtility hX.measurable.aemeasurable - _ ≤ ENNReal.log (μ A)⁻¹ := by - refine ENNReal.log_monotone ?_ - rw [ProbabilityTheory.cond, lintegral_smul_measure, smul_eq_mul] - calc (μ A)⁻¹ * ∫⁻ x, X x ∂μ.restrict A - _ ≤ (μ A)⁻¹ * 1 := by - gcongr - exact (setLIntegral_le_lintegral A X).trans - ((hX.lintegral_le_measure_univ μ rfl).trans_eq measure_univ) - _ = (μ A)⁻¹ := mul_one _ - -/-! ### A Sanov-type bound and the law of large numbers -/ - -/-- The tuples whose empirical averages of the measurable functions `f i` are within `ε` of the -`a i` form a measurable set. -/ -lemma measurableSet_setOf_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} - (hf : ∀ i, Measurable (f i)) (a : Fin k → ℝ) (ε : ℝ) (m : ℕ) : - MeasurableSet {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} := by - simp only [Set.ofPred_forall] - exact MeasurableSet.iInter fun i ↦ measurableSet_le (continuous_abs.measurable.comp - (((Finset.measurable_sum _ fun j _ ↦ (hf i).comp (measurable_pi_apply j)).div_const _).sub_const - _)) measurable_const - -/-- The integral against the average of the marginals of `μ` is the integral of the empirical -average against `μ`. -/ -lemma integral_sum_smul_map_eval {m : ℕ} (μ : Measure (Fin m → 𝓧)) - [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) : - ∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) = - ∫ x, (∑ j, g (x j)) / m ∂μ := by - have hint (ν : Measure 𝓧) [IsFiniteMeasure ν] : Integrable g ν := - Integrable.of_bound hg.aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC x) - rw [integral_finsetSum_measure fun j _ ↦ (hint _).smul_measure ENNReal.coe_ne_top] - have hj (j : Fin m) : ∫ x, g x ∂(μ.map fun x ↦ x j) = ∫ x, g (x j) ∂μ := - integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable - simp_rw [integral_smul_measure, hj] - have hs : ∫ x, ∑ j, g (x j) ∂μ = ∑ j, ∫ x, g (x j) ∂μ := - integral_finsetSum _ fun j _ ↦ Integrable.of_bound - (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC _) - rw [integral_div, hs] - simp [div_eq_inv_mul, Finset.mul_sum] - -/-- **Sanov-type bound.** If every law `R` whose integrals of the bounded functions `f i` are -within `ε` of `a i` is at relative entropy at least `c ≥ 0` from `P`, then the probability under -`P ^ m` that the empirical averages of the `f i` are within `ε` of the `a i` is at most -`exp (- m c)`. -/ -lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (hf : ∀ i, Measurable (f i)) - {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) {a : Fin k → ℝ} {ε c : ℝ} (hc : 0 ≤ c) - {P : Measure 𝓧} [IsProbabilityMeasure P] - (hU : ∀ R : Measure 𝓧, IsProbabilityMeasure R → (∀ i, |∫ x, f i x ∂R - a i| ≤ ε) → - ENNReal.ofReal c ≤ klDiv R P) {m : ℕ} (hm : m ≠ 0) : - ENNReal.ofReal (Real.exp (m * c)) * - (Measure.pi fun _ : Fin m ↦ P) {x | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} ≤ 1 := by - set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} - set Pm := Measure.pi fun _ : Fin m ↦ P - have hA : MeasurableSet A := measurableSet_setOf_forall_abs_avg_sub_le hf a ε m - rcases eq_or_ne (Pm A) 0 with h0 | h0 - · simp [h0] - set μ := Pm[|A] - have : IsProbabilityMeasure μ := cond_isProbabilityMeasure h0 - have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm - set w : Fin m → ℝ≥0 := fun _ ↦ (m : ℝ≥0)⁻¹ - have hw : ∑ j, w j = 1 := by - simp [w, Finset.card_univ, mul_inv_cancel₀ (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0)] - set R := ∑ j, (w j : ℝ≥0∞) • μ.map fun x ↦ x j - have hR : IsProbabilityMeasure R := ⟨by - simp [R, w, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), - ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m)]⟩ - have hRU (i : Fin k) : |∫ x, f i x ∂R - a i| ≤ ε := by - rw [integral_sum_smul_map_eval μ (hf i) (hfC i)] - have hint : Integrable (fun x : Fin m → 𝓧 ↦ (∑ j, f i (x j)) / m) μ := - ((integrable_finsetSum _ fun j _ ↦ Integrable.of_bound - ((hf i).comp (measurable_pi_apply j)).aestronglyMeasurable (C i) - (Eventually.of_forall fun x ↦ hfC i _))).div_const _ - have heq : ∫ x, (∑ j, f i (x j)) / m ∂μ - a i = ∫ x, ((∑ j, f i (x j)) / m - a i) ∂μ := by - rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul] - rw [heq, ← Real.norm_eq_abs] - refine (norm_integral_le_of_norm_le_const (C := ε) ?_).trans (by simp) - filter_upwards [ae_cond_mem hA] with x hx - simpa [Real.norm_eq_abs] using hx i - have h1 : (m : ℝ≥0∞) * ENNReal.ofReal c ≤ klDiv μ Pm := by - calc (m : ℝ≥0∞) * ENNReal.ofReal c - _ ≤ m * klDiv R P := by gcongr; exact hU R hR hRU - _ ≤ m * ∑ j, (w j : ℝ≥0∞) * klDiv (μ.map fun x ↦ x j) P := by - gcongr - exact klDiv_sum_smul_left_le hw - _ = ∑ j, klDiv (μ.map fun x ↦ x j) P := by - rw [Finset.mul_sum] - refine Finset.sum_congr rfl fun j _ ↦ ?_ - rw [← mul_assoc, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), - ENNReal.coe_natCast, ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m), one_mul] - _ ≤ klDiv μ Pm := sum_klDiv_map_eval_le P m μ - rw [← ENNReal.le_inv_iff_mul_le, ← ENNReal.log_le_log_iff, - ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] - calc ((m * c : ℝ) : EReal) - _ = ((ENNReal.ofReal (m * c) : ℝ≥0∞) : EReal) := by - rw [EReal.coe_ennreal_ofReal, max_eq_left (by positivity)] - _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by - rw [ENNReal.ofReal_mul (Nat.cast_nonneg _), ENNReal.ofReal_natCast] - _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1 - _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0 - -/-- **Weak law of large numbers**, by Chebyshev's inequality: the probability that the empirical -average of a function bounded by `C` deviates by more than `ε` from its mean is at most -`C ^ 2 / (m ε ^ 2)`. -/ -lemma measure_pi_lt_abs_avg_sub_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) - (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : - (Measure.pi fun _ : Fin m ↦ Q) {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} ≤ - ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by - set Qm := Measure.pi fun _ : Fin m ↦ Q - set X : (Fin m → 𝓧) → ℝ := fun x ↦ ∑ j, g (x j) with hX_def - have hm' : (0 : ℝ) < m := Nat.cast_pos.2 (Nat.pos_of_ne_zero hm) - have hgL (j : Fin m) : MemLp (fun x : Fin m → 𝓧 ↦ g (x j)) 2 Qm := - MemLp.of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C - (Eventually.of_forall fun x ↦ hgC _) - have hXL : MemLp X 2 Qm := memLp_finsetSum _ fun j _ ↦ hgL j - have hEX : ∫ x, X x ∂Qm = m * ∫ y, g y ∂Q := by - have hj (j : Fin m) : ∫ x, g (x j) ∂Qm = ∫ y, g y ∂Q := by - rw [← integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable] - congr 1 - exact (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq - rw [integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two] - simp [hj] - have hVar : Var[X; Qm] ≤ m * C ^ 2 := by - have h := variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) - fun _ ↦ MemLp.of_bound hg.aestronglyMeasurable C (Eventually.of_forall hgC) - have hX : X = ∑ j : Fin m, fun x : Fin m → 𝓧 ↦ g (x j) := by - ext x - simp [X] - rw [hX, h, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] - gcongr - have hb := variance_le_sq_of_bounded (μ := Q) (a := -C) (b := C) - (Eventually.of_forall fun x ↦ abs_le.1 (hgC x)) hg.aemeasurable - convert hb using 1 - ring - calc Qm {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} - _ ≤ Qm {x | m * ε ≤ |X x - ∫ x, X x ∂Qm|} := by - refine measure_mono fun x hx ↦ ?_ - simp only [Set.mem_ofPred_eq] at hx ⊢ - have h : (∑ j, g (x j)) / m - ∫ y, g y ∂Q = (X x - ∫ x, X x ∂Qm) / m := by - rw [hEX, hX_def] - field_simp - rw [h, abs_div, abs_of_pos hm', lt_div_iff₀ hm'] at hx - linarith - _ ≤ ENNReal.ofReal (Var[X; Qm] / (m * ε) ^ 2) := - meas_ge_le_variance_div_sq hXL (by positivity) - _ ≤ ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by - refine ENNReal.ofReal_le_ofReal ?_ - calc Var[X; Qm] / (m * ε) ^ 2 - _ ≤ m * C ^ 2 / (m * ε) ^ 2 := by gcongr - _ = C ^ 2 / (m * ε ^ 2) := by field_simp - /-- The e-variable `1/2 + (1/2) e ^ t 1_A`, valid when `e ^ t P (A) ≤ 1` for every member `P` of the null, gives the lower bound `t Q (A) - log 2` on the growth of `m` observations. -/ lemma le_maxLogGrowth_of_ofReal_exp_mul_le_one (Q : Measure 𝓧) [IsProbabilityMeasure Q] @@ -359,61 +119,34 @@ test functions need only be bounded, by any constant, and measurable: no topolog used, and lower semicontinuity for weak convergence is a special case. -/ theorem bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le (Q : Measure 𝓧) [IsProbabilityMeasure Q] (S : Set (Measure 𝓧)) (hS : ∀ P ∈ S, IsProbabilityMeasure P) - (h : ∀ c : EReal, c < ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) → + (h : ∀ c : ℝ≥0∞, c < ⨅ P ∈ S, klDiv Q P → ∃ (k : ℕ) (f : Fin k → 𝓧 → ℝ) (ε : ℝ), 0 < ε ∧ (∀ i, Measurable (f i)) ∧ (∀ i, ∃ C, ∀ x, |f i x| ≤ C) ∧ ∀ R : Measure 𝓧, IsProbabilityMeasure R → - (∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) → - c ≤ ⨅ P ∈ S, ((klDiv R P : ℝ≥0∞) : EReal)) : - bipolarRate Q S = ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal) := by - refine le_antisymm (bipolarRate_le_iInf_coe_klDiv Q S hS) + (∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) → c ≤ ⨅ P ∈ S, klDiv R P) : + bipolarRate Q S = (⨅ P ∈ S, klDiv Q P : ℝ≥0∞) := by + refine le_antisymm (bipolarRate_le_iInf_klDiv Q hS) (le_of_forall_lt_imp_le_of_dense fun c hc ↦ ?_) rcases le_or_gt c 0 with hc0 | hc0 · exact hc0.trans (bipolarRate_nonneg Q S) - obtain ⟨k, f, ε, hε, hfm, hfC, hU⟩ := h c hc - choose C hC using hfC obtain ⟨c, rfl⟩ : ∃ r : ℝ, (r : EReal) = c := ⟨c.toReal, EReal.coe_toReal hc.ne_top (ne_bot_of_gt hc0)⟩ have hc0' : 0 < c := by exact_mod_cast hc0 - -- every law in the neighbourhood is at relative entropy at least `c` from every null law - have hU' (P : Measure 𝓧) (hP : P ∈ S) (R : Measure 𝓧) (hR : IsProbabilityMeasure R) - (hRf : ∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) : ENNReal.ofReal c ≤ klDiv R P := by - have := (hU R hR hRf).trans (iInf₂_le P hP) - rwa [← max_eq_left hc0'.le, ← EReal.coe_ennreal_ofReal, - EReal.coe_ennreal_le_coe_ennreal_iff] at this - set A : ∀ m : ℕ, Set (Fin m → 𝓧) := - fun m ↦ {x | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} with hA_def + have hcE : ((ENNReal.ofReal c : ℝ≥0∞) : EReal) = c := by + rw [EReal.coe_ennreal_ofReal, max_eq_left hc0'.le] + obtain ⟨k, f, ε, hε, hfm, hfC, hU⟩ := + h (ENNReal.ofReal c) (EReal.coe_ennreal_lt_coe_ennreal_iff.1 (hcE ▸ hc)) + choose C hC using hfC set D := ∑ i, C i ^ 2 / ε ^ 2 - -- the law of large numbers under `Q` - have hQA (m : ℕ) (hm : m ≠ 0) : 1 - D / m ≤ (Measure.pi fun _ : Fin m ↦ Q).real (A m) := by - have hcompl : (A m)ᶜ = ⋃ i, {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} := by - ext x - simp [A] - have hle : (Measure.pi fun _ : Fin m ↦ Q) (A m)ᶜ ≤ ENNReal.ofReal (D / m) := by - rw [hcompl] - refine (measure_iUnion_fintype_le _ _).trans ?_ - calc ∑ i, (Measure.pi fun _ : Fin m ↦ Q) - {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} - _ ≤ ∑ i, ENNReal.ofReal (C i ^ 2 / (m * ε ^ 2)) := - Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_avg_sub_le (hfm i) (hC i) Q hε hm - _ = ENNReal.ofReal (D / m) := by - rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦ by positivity] - congr 1 - simp only [D, Finset.sum_div] - refine Finset.sum_congr rfl fun i _ ↦ ?_ - field_simp - have h := ENNReal.toReal_le_of_le_ofReal (by positivity) hle - rw [← measureReal_def, probReal_compl_eq_one_sub - (measurableSet_setOf_forall_abs_avg_sub_le hfm _ ε m)] at h - linarith refine le_bipolarRate_of_tendsto (r := fun n ↦ (n + 1) * c * (1 - D / (n + 1)) - Real.log 2) (fun n ↦ ?_) ?_ - · have hsan (P : Measure 𝓧) (hP : P ∈ S) := + · -- the e-variable `1/2 + (1/2) exp ((n + 1) c) 1_A`, with the law of large numbers under `Q` + have hsan (P : Measure 𝓧) (hP : P ∈ S) := have := hS P hP - ofReal_exp_mul_measure_pi_le_one hfm hC hc0'.le (hU' P hP) (m := n + 1) n.succ_ne_zero + ofReal_exp_mul_measure_pi_le_one hfm hC hc0'.le + (fun R hR hRf ↦ (hU R hR hRf).trans (iInf₂_le P hP)) (m := n + 1) n.succ_ne_zero refine le_trans ?_ (le_maxLogGrowth_of_ofReal_exp_mul_le_one Q hS (measurableSet_setOf_forall_abs_avg_sub_le hfm _ ε (n + 1)) hsan) - have h := hQA (n + 1) n.succ_ne_zero - simp only [hA_def] at h + have h := one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le hfm hC Q hε n.succ_ne_zero refine EReal.coe_le_coe_iff.2 ?_ have hnc : 0 ≤ ((n + 1 : ℕ) : ℝ) * c := by positivity have hn1 : ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1 := by push_cast; ring diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Cond.lean b/LMLExplore/InformationTheory/KullbackLeibler/Cond.lean new file mode 100644 index 00000000..472436ed --- /dev/null +++ b/LMLExplore/InformationTheory/KullbackLeibler/Cond.lean @@ -0,0 +1,54 @@ +/- +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.ConditionalProbability +public import Statlib.EValues.RIPr + +/-! +# The relative entropy from a conditional law + +The relative entropy from the law `μ[|A]`, the probability measure `μ` conditioned on the event +`A`, to `μ` is at most `log (1 / μ A)`. The proof uses Statlib's variational form of the relative +entropy, the maximal expected logarithm of an e-variable for the singleton null +(`maxUtility_singleton_eq_klDiv`), and Jensen's inequality: an e-variable for `μ` has integral at +most `1 / μ A` under `μ[|A]`. + +## Main statements + +* `InformationTheory.klDiv_cond_le`: `klDiv (μ[|A]) μ ≤ log (1 / μ A)`. +-/ + +public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace InformationTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-- The relative entropy from the law `μ` conditioned on `A` to `μ` is at most `log (1 / μ A)`. -/ +lemma klDiv_cond_le {μ : Measure 𝓧} [IsProbabilityMeasure μ] {A : Set 𝓧} (hμA : μ A ≠ 0) : + ((klDiv (μ[|A]) μ : ℝ≥0∞) : EReal) ≤ ENNReal.log (μ A)⁻¹ := by + have := cond_isProbabilityMeasure hμA + rw [← maxUtility_singleton_eq_klDiv] + refine iSup₂_le fun X hX ↦ ?_ + calc ∫ᵉ x, (logUtility ∘ X) x ∂μ[|A] + _ ≤ logUtility (∫⁻ x, X x ∂μ[|A]) := + Utility.eintegral_le_map logUtility hX.measurable.aemeasurable + _ ≤ ENNReal.log (μ A)⁻¹ := by + refine ENNReal.log_monotone ?_ + rw [ProbabilityTheory.cond, lintegral_smul_measure, smul_eq_mul] + calc (μ A)⁻¹ * ∫⁻ x, X x ∂μ.restrict A + _ ≤ (μ A)⁻¹ * 1 := by + gcongr + exact (setLIntegral_le_lintegral A X).trans + ((hX.lintegral_le_measure_univ μ rfl).trans_eq measure_univ) + _ = (μ A)⁻¹ := mul_one _ + +end InformationTheory diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean b/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean new file mode 100644 index 00000000..73c53c79 --- /dev/null +++ b/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean @@ -0,0 +1,92 @@ +/- +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 Statlib.EValues.Product +public import Statlib.EValues.RIPr +public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing + +/-! +# Superadditivity of the relative entropy over the marginals of a product + +The relative entropy from a law to a product law is at least the sum of the relative entropies of +its marginals to the factors. For two factors, this is the value of Statlib's +`maxUtility_fst_add_maxUtility_snd_le` for singleton nulls, where the maximal expected logarithm +of an e-variable is the relative entropy (`maxUtility_singleton_eq_klDiv`); for finitely many +factors, it follows by induction on the number of coordinates. + +## Main statements + +* `InformationTheory.klDiv_fst_add_klDiv_snd_le`: the relative entropy to a product law is at + least the sum of the relative entropies of the two marginals. +* `InformationTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on `Fin n → 𝓧` to a + product law `Measure.pi P` is at least the sum of the relative entropies of its marginals to the + factors `P j`. +-/ + +public section + +open MeasureTheory ProbabilityTheory + +namespace InformationTheory + +variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} + +/-- The relative entropy to a product law is at least the sum of the relative entropies of the +two marginals. -/ +lemma klDiv_fst_add_klDiv_snd_le (R : Measure (𝓧 × 𝓨)) [IsProbabilityMeasure R] (P : Measure 𝓧) + (P' : Measure 𝓨) [IsProbabilityMeasure P] [IsProbabilityMeasure P'] : + klDiv R.fst P + klDiv R.snd P' ≤ klDiv R (P.prod P') := by + have h := maxUtility_fst_add_maxUtility_snd_le R (S := {P}) (T := {P'}) + (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) + (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance) + rwa [Set.image2_singleton, maxUtility_singleton_eq_klDiv, maxUtility_singleton_eq_klDiv, + maxUtility_singleton_eq_klDiv, ← EReal.coe_ennreal_add, + EReal.coe_ennreal_le_coe_ennreal_iff] at h + +/-- The relative entropy from a law on `Fin n → 𝓧` to a product law `Measure.pi P` is at least the +sum of the relative entropies of its marginals to the factors `P j`. -/ +lemma sum_klDiv_map_eval_le {n : ℕ} (P : Fin n → Measure 𝓧) [∀ j, IsProbabilityMeasure (P j)] + (μ : Measure (Fin n → 𝓧)) [IsProbabilityMeasure μ] : + ∑ j, klDiv (μ.map fun x ↦ x j) (P j) ≤ klDiv μ (Measure.pi P) := by + induction n with + | zero => simp + | succ n ih => + set e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) ↦ 𝓧) 0 + set R := μ.map e + -- `e` splits off the first coordinate and carries `Measure.pi P` to a product law + have hpi : (Measure.pi P).map e = (P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ) := by + rw [(measurePreserving_piFinSuccAbove P 0).map_eq] + simp + have hKL : klDiv R ((P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ)) = + klDiv μ (Measure.pi P) := by + rw [← hpi] + exact klDiv_map_measurableEmbedding _ _ e.measurableEmbedding + have hfst : R.fst = μ.map fun x ↦ x 0 := by + have h : Prod.fst ∘ e = fun x ↦ x 0 := by + ext x + simp [e, MeasurableEquiv.piFinSuccAbove_apply] + rw [Measure.fst, Measure.map_map measurable_fst e.measurable, h] + have hsnd : R.snd = μ.map fun x j ↦ x j.succ := by + have h : Prod.snd ∘ e = fun x j ↦ x j.succ := by + ext x j + simp [e, MeasurableEquiv.piFinSuccAbove_apply, Fin.tail] + rw [Measure.snd, Measure.map_map measurable_snd e.measurable, h] + have hmarg (j : Fin n) : R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x j.succ := by + rw [hsnd, Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] + calc ∑ j, klDiv (μ.map fun x ↦ x j) (P j) + _ = klDiv R.fst (P 0) + ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) (P j.succ) := by + rw [Fin.sum_univ_succ, hfst] + simp_rw [hmarg] + _ ≤ klDiv R.fst (P 0) + klDiv R.snd (Measure.pi fun j : Fin n ↦ P j.succ) := by + gcongr + exact ih _ R.snd + _ ≤ klDiv R ((P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ)) := + klDiv_fst_add_klDiv_snd_le R _ _ + _ = klDiv μ (Measure.pi P) := hKL + +end InformationTheory diff --git a/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean new file mode 100644 index 00000000..02e62e0b --- /dev/null +++ b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean @@ -0,0 +1,244 @@ +/- +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 LMLExplore.InformationTheory.KullbackLeibler.Cond +public import LMLExplore.InformationTheory.KullbackLeibler.Pi +public import Mathlib.Probability.Moments.Variance +public import Statlib.Divergence.KullbackLeibler.Basic +public import Statlib.ForMathlib.MeasureTheory.Integral.Pi + +/-! +# Empirical averages of bounded functions under product laws + +For finitely many bounded measurable functions `f i` on `𝓧` and `m` observations `x : Fin m → 𝓧`, +this file bounds the probability, under an i.i.d. law `P ^ m`, that the empirical averages +`(∑ j, f i (x j)) / m` lie within `ε` of given values `a i`, from both sides. + +* From above, by a Sanov-type bound with blocks of length one: if every law whose integrals of + the `f i` are within `ε` of the `a i` is at relative entropy at least `c` from `P`, the + probability is at most `exp (- m c)`. This is Csiszár's argument for Sanov's upper bound on a + convex set [Csi84]: condition `P ^ m` on the event, whose relative entropy to `P ^ m` is at most + `log (1 / P ^ m (A))` (`InformationTheory.klDiv_cond_le`), and bound it from below by the + superadditivity of the relative entropy over the coordinates + (`InformationTheory.sum_klDiv_map_eval_le`) and its convexity, at the average of the marginals + of the conditioned law, which is in the neighbourhood. +* From below, when the `a i` are the means of the `f i` under `P`, by the weak law of large + numbers from Chebyshev's inequality. + +## Main statements + +* `ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`: the Sanov-type bound. +* `ProbabilityTheory.measure_pi_lt_abs_avg_sub_le`: the weak law of large numbers for a bounded + function, `P ^ m (|avg - mean| > ε) ≤ C ^ 2 / (m ε ^ 2)`. +* `ProbabilityTheory.one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le`: the weak law of large + numbers for finitely many bounded functions at once. + +## References + +* [Csi84] I. Csiszár, *Sanov property, generalized I-projection and a conditional limit theorem*, + Ann. Probab. 12 (1984), 768–793. +-/ + +public section + +open MeasureTheory InformationTheory Filter +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-- The tuples whose empirical averages of the measurable functions `f i` are within `ε` of the +`a i` form a measurable set. -/ +lemma measurableSet_setOf_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} + (hf : ∀ i, Measurable (f i)) (a : Fin k → ℝ) (ε : ℝ) (m : ℕ) : + MeasurableSet {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} := by + simp only [Set.ofPred_forall] + exact MeasurableSet.iInter fun i ↦ measurableSet_le (continuous_abs.measurable.comp + (((Finset.measurable_sum _ fun j _ ↦ (hf i).comp (measurable_pi_apply j)).div_const _).sub_const + _)) measurable_const + +/-- The average of the marginals of a probability measure on `Fin m → 𝓧`, for `m ≠ 0`, is a +probability measure. -/ +lemma isProbabilityMeasure_sum_smul_map_eval {m : ℕ} (hm : m ≠ 0) (μ : Measure (Fin m → 𝓧)) + [IsProbabilityMeasure μ] : + IsProbabilityMeasure (∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) := + ⟨by simp [ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), + ENNReal.mul_inv_cancel (Nat.cast_ne_zero.2 hm) (ENNReal.natCast_ne_top m)]⟩ + +/-- The integral against the average of the marginals of `μ` is the integral of the empirical +average against `μ`. -/ +lemma integral_sum_smul_map_eval {m : ℕ} (μ : Measure (Fin m → 𝓧)) + [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) : + ∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) = + ∫ x, (∑ j, g (x j)) / m ∂μ := by + have hint (ν : Measure 𝓧) [IsFiniteMeasure ν] : Integrable g ν := + Integrable.of_bound hg.aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC x) + rw [integral_finsetSum_measure fun j _ ↦ (hint _).smul_measure ENNReal.coe_ne_top] + have hj (j : Fin m) : ∫ x, g x ∂(μ.map fun x ↦ x j) = ∫ x, g (x j) ∂μ := + integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable + simp_rw [integral_smul_measure, hj] + have hs : ∫ x, ∑ j, g (x j) ∂μ = ∑ j, ∫ x, g (x j) ∂μ := + integral_finsetSum _ fun j _ ↦ Integrable.of_bound + (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC _) + rw [integral_div, hs] + simp [div_eq_inv_mul, Finset.mul_sum] + +/-- If the empirical average of a bounded measurable function `g` is almost surely within `ε` of +`a` under `μ`, then so is the integral of `g` against the average of the marginals of `μ`. -/ +lemma abs_integral_sum_smul_map_eval_sub_le {m : ℕ} (μ : Measure (Fin m → 𝓧)) + [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) + {a ε : ℝ} (hμ : ∀ᵐ x ∂μ, |(∑ j, g (x j)) / m - a| ≤ ε) : + |∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) - a| ≤ ε := by + rw [integral_sum_smul_map_eval μ hg hgC] + have hint : Integrable (fun x : Fin m → 𝓧 ↦ (∑ j, g (x j)) / m) μ := + ((integrable_finsetSum _ fun j _ ↦ Integrable.of_bound + (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C + (Eventually.of_forall fun x ↦ hgC _))).div_const _ + have heq : ∫ x, (∑ j, g (x j)) / m ∂μ - a = ∫ x, ((∑ j, g (x j)) / m - a) ∂μ := by + rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul] + rw [heq, ← Real.norm_eq_abs] + refine (norm_integral_le_of_norm_le_const (C := ε) ?_).trans (by simp) + simpa only [Real.norm_eq_abs] using hμ + +/-- **Sanov-type bound** [Csi84]. If every law `R` whose integrals of the bounded functions `f i` +are within `ε` of `a i` is at relative entropy at least `c ≥ 0` from `P`, then the probability +under `P ^ m` that the empirical averages of the `f i` are within `ε` of the `a i` is at most +`exp (- m c)`. -/ +lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (hf : ∀ i, Measurable (f i)) + {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) {a : Fin k → ℝ} {ε c : ℝ} (hc : 0 ≤ c) + {P : Measure 𝓧} [IsProbabilityMeasure P] + (hU : ∀ R : Measure 𝓧, IsProbabilityMeasure R → (∀ i, |∫ x, f i x ∂R - a i| ≤ ε) → + ENNReal.ofReal c ≤ klDiv R P) {m : ℕ} (hm : m ≠ 0) : + ENNReal.ofReal (Real.exp (m * c)) * + (Measure.pi fun _ : Fin m ↦ P) {x | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} ≤ 1 := by + set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} + set Pm := Measure.pi fun _ : Fin m ↦ P + have hA : MeasurableSet A := measurableSet_setOf_forall_abs_avg_sub_le hf a ε m + rcases eq_or_ne (Pm A) 0 with h0 | h0 + · simp [h0] + -- the law `μ` of `m` observations conditioned on the event, and the average `R` of its marginals + set μ := Pm[|A] + have : IsProbabilityMeasure μ := cond_isProbabilityMeasure h0 + have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm + set w : Fin m → ℝ≥0 := fun _ ↦ (m : ℝ≥0)⁻¹ + have hw : ∑ j, w j = 1 := by + simp [w, Finset.card_univ, mul_inv_cancel₀ (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0)] + set R := ∑ j, (w j : ℝ≥0∞) • μ.map fun x ↦ x j + have hR : IsProbabilityMeasure R := isProbabilityMeasure_sum_smul_map_eval hm μ + have hRU (i : Fin k) : |∫ x, f i x ∂R - a i| ≤ ε := by + refine abs_integral_sum_smul_map_eval_sub_le μ (hf i) (hfC i) ?_ + filter_upwards [ae_cond_mem hA] with x hx + exact hx i + -- `R` is in the neighbourhood, so by convexity and superadditivity over the coordinates the + -- relative entropy from `μ` to `P ^ m` is at least `m c` + have h1 : (m : ℝ≥0∞) * ENNReal.ofReal c ≤ klDiv μ Pm := by + calc (m : ℝ≥0∞) * ENNReal.ofReal c + _ ≤ m * klDiv R P := by gcongr; exact hU R hR hRU + _ ≤ m * ∑ j, (w j : ℝ≥0∞) * klDiv (μ.map fun x ↦ x j) P := by + gcongr + exact klDiv_sum_smul_left_le hw + _ = ∑ j, klDiv (μ.map fun x ↦ x j) P := by + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ ↦ ?_ + rw [← mul_assoc, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), + ENNReal.coe_natCast, ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m), one_mul] + _ ≤ klDiv μ Pm := sum_klDiv_map_eval_le (fun _ ↦ P) μ + -- the relative entropy from `μ` to `P ^ m` is at most `log (1 / P ^ m (A))`: take logarithms + rw [← ENNReal.le_inv_iff_mul_le, ← ENNReal.log_le_log_iff, + ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] + calc ((m * c : ℝ) : EReal) + _ = ((ENNReal.ofReal (m * c) : ℝ≥0∞) : EReal) := by + rw [EReal.coe_ennreal_ofReal, max_eq_left (by positivity)] + _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by + rw [ENNReal.ofReal_mul (Nat.cast_nonneg _), ENNReal.ofReal_natCast] + _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1 + _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0 + +/-- **Weak law of large numbers**, by Chebyshev's inequality: the probability that the empirical +average of a function bounded by `C` deviates by more than `ε` from its mean is at most +`C ^ 2 / (m ε ^ 2)`. -/ +lemma measure_pi_lt_abs_avg_sub_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) + (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : + (Measure.pi fun _ : Fin m ↦ Q) {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} ≤ + ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by + set Qm := Measure.pi fun _ : Fin m ↦ Q + set X : (Fin m → 𝓧) → ℝ := fun x ↦ ∑ j, g (x j) with hX_def + have hm' : (0 : ℝ) < m := Nat.cast_pos.2 (Nat.pos_of_ne_zero hm) + have hgL (j : Fin m) : MemLp (fun x : Fin m → 𝓧 ↦ g (x j)) 2 Qm := + MemLp.of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C + (Eventually.of_forall fun x ↦ hgC _) + have hXL : MemLp X 2 Qm := memLp_finsetSum _ fun j _ ↦ hgL j + have hEX : ∫ x, X x ∂Qm = m * ∫ y, g y ∂Q := by + have hj (j : Fin m) : ∫ x, g (x j) ∂Qm = ∫ y, g y ∂Q := by + rw [← integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable] + congr 1 + exact (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq + rw [integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two] + simp [hj] + have hVar : Var[X; Qm] ≤ m * C ^ 2 := by + have h := variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) + fun _ ↦ MemLp.of_bound hg.aestronglyMeasurable C (Eventually.of_forall hgC) + have hX : X = ∑ j : Fin m, fun x : Fin m → 𝓧 ↦ g (x j) := by + ext x + simp [X] + rw [hX, h, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] + gcongr + have hb := variance_le_sq_of_bounded (μ := Q) (a := -C) (b := C) + (Eventually.of_forall fun x ↦ abs_le.1 (hgC x)) hg.aemeasurable + convert hb using 1 + ring + calc Qm {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} + _ ≤ Qm {x | m * ε ≤ |X x - ∫ x, X x ∂Qm|} := by + refine measure_mono fun x hx ↦ ?_ + simp only [Set.mem_ofPred_eq] at hx ⊢ + have h : (∑ j, g (x j)) / m - ∫ y, g y ∂Q = (X x - ∫ x, X x ∂Qm) / m := by + rw [hEX, hX_def] + field_simp + rw [h, abs_div, abs_of_pos hm', lt_div_iff₀ hm'] at hx + linarith + _ ≤ ENNReal.ofReal (Var[X; Qm] / (m * ε) ^ 2) := + meas_ge_le_variance_div_sq hXL (by positivity) + _ ≤ ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by + refine ENNReal.ofReal_le_ofReal ?_ + calc Var[X; Qm] / (m * ε) ^ 2 + _ ≤ m * C ^ 2 / (m * ε) ^ 2 := by gcongr + _ = C ^ 2 / (m * ε ^ 2) := by field_simp + +/-- **Weak law of large numbers** for finitely many functions `f i` bounded by `C i`: with +probability at least `1 - (∑ i, C i ^ 2 / ε ^ 2) / m` under `Q ^ m`, the empirical averages of all +the `f i` are within `ε` of their means. -/ +lemma one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} + (hf : ∀ i, Measurable (f i)) {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) + (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : + 1 - (∑ i, C i ^ 2 / ε ^ 2) / m ≤ + (Measure.pi fun _ : Fin m ↦ Q).real + {x | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} := by + set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} + have hcompl : Aᶜ = ⋃ i, {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} := by + ext x + simp [A] + have hle : (Measure.pi fun _ : Fin m ↦ Q) Aᶜ ≤ + ENNReal.ofReal ((∑ i, C i ^ 2 / ε ^ 2) / m) := by + rw [hcompl] + refine (measure_iUnion_fintype_le _ _).trans ?_ + calc ∑ i, (Measure.pi fun _ : Fin m ↦ Q) + {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} + _ ≤ ∑ i, ENNReal.ofReal (C i ^ 2 / (m * ε ^ 2)) := + Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_avg_sub_le (hf i) (hfC i) Q hε hm + _ = ENNReal.ofReal ((∑ i, C i ^ 2 / ε ^ 2) / m) := by + rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦ by positivity] + congr 1 + simp only [Finset.sum_div] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + field_simp + have h := ENNReal.toReal_le_of_le_ofReal (by positivity) hle + rw [← measureReal_def, probReal_compl_eq_one_sub + (measurableSet_setOf_forall_abs_avg_sub_le hf _ ε m)] at h + linarith + +end ProbabilityTheory From 880a8e9912a1f4bbdf77d4f8cb6518e26a94f66b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:19:26 +0100 Subject: [PATCH 3/3] refactor: generalize the KL superadditivity and the weak law, address review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `sum_klDiv_map_eval_le` now holds for any finite index type and a different space per coordinate (via the `Fin n` case and `MeasurableEquiv.piCongrLeft`). - The weak law `measure_pi_lt_abs_sum_div_sub_le` and its finite-family version take `MemLp _ 2 Q` and give the bound `Var[g; Q] / (m ε ^ 2)`. - Rename `avg` to `sum_div` in the empirical-average lemma names. - Move `le_maxLogGrowth_of_ofReal_exp_mul_le_one` to `BipolarRate.lean` and fix its docstring to the product laws `P ^ m`, `Q ^ m`. - Reuse `maxLogGrowth_div_le_bipolarRate` in `le_bipolarRate_of_tendsto`. - Factor `integrable_comp_eval_of_abs_le`, replace brittle `rw` chains and the weight algebra with `simp`, and `nlinarith` with `gcongr`. Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate.lean | 60 +++++- .../EValues/BipolarRate/Semicontinuity.lean | 75 ++------ .../InformationTheory/KullbackLeibler/Pi.lean | 82 +++++--- .../LargeDeviations/EmpiricalAverage.lean | 176 ++++++++---------- 4 files changed, 202 insertions(+), 191 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate.lean b/LMLExplore/EValues/BipolarRate.lean index ed8234a6..d0719966 100644 --- a/LMLExplore/EValues/BipolarRate.lean +++ b/LMLExplore/EValues/BipolarRate.lean @@ -49,6 +49,9 @@ else: no domination, convexity or compactness. [RR26, proof of Theorem 4.1]. * `ProbabilityTheory.le_bipolarRate_of_tendsto`: a lower bound on the bipolar rate from real lower bounds on `maxLogGrowth Q₁ S₁ (n + 1)` whose quotients by `n + 1` converge. +* `ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`: the lower bound on the growth of + `m` observations given by the e-variable `1/2 + (1/2) e ^ t 1_A`, valid when + `e ^ t P ^ m (A) ≤ 1` for every member `P` of the null. ## References @@ -232,13 +235,64 @@ lemma le_bipolarRate_of_tendsto {r : ℕ → ℝ} {L : ℝ} (hr : ∀ n, (r n : EReal) ≤ maxLogGrowth Q₁ S₁ (n + 1)) (hlim : Tendsto (fun n : ℕ ↦ r n / (n + 1)) atTop (𝓝 L)) : (L : EReal) ≤ bipolarRate Q₁ S₁ := by - rw [bipolarRate_def] refine le_of_tendsto' (EReal.tendsto_coe.2 hlim) fun n ↦ ?_ - refine le_trans ?_ (le_iSup _ n) have h : ((r n / (n + 1) : ℝ) : EReal) = (r n : EReal) / ((n + 1 : ℕ) : EReal) := by rw [EReal.coe_div] norm_cast rw [h] - exact EReal.div_le_div_right_of_nonneg (by positivity) (hr n) + exact (EReal.div_le_div_right_of_nonneg (by positivity) (hr n)).trans + (maxLogGrowth_div_le_bipolarRate Q₁ S₁ n.succ_ne_zero) + +/-- The e-variable `1/2 + (1/2) e ^ t 1_A` on `m` observations, valid when `e ^ t P ^ m (A) ≤ 1` +for every member `P` of the null, gives the lower bound `t Q ^ m (A) - log 2` on the growth of `m` +observations. -/ +lemma le_maxLogGrowth_of_ofReal_exp_mul_le_one (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) {m : ℕ} + {A : Set (Fin m → 𝓧)} (hA : MeasurableSet A) {t : ℝ} + (hP : ∀ P ∈ S, ENNReal.ofReal (Real.exp t) * (Measure.pi fun _ : Fin m ↦ P) A ≤ 1) : + ((t * (Measure.pi fun _ : Fin m ↦ Q).real A - Real.log 2 : ℝ) : EReal) ≤ + maxLogGrowth Q S m := by + set Qm := Measure.pi fun _ : Fin m ↦ Q + set b := ENNReal.ofReal (Real.exp t) + set X : (Fin m → 𝓧) → ℝ≥0∞ := fun x ↦ 2⁻¹ + 2⁻¹ * A.indicator (fun _ ↦ b) x + have hXm : Measurable X := measurable_const.add (measurable_const.mul + (measurable_const.indicator hA)) + have hX : IsEVar X ((fun P ↦ Measure.pi fun _ : Fin m ↦ P) '' S) := by + refine IsEVar.of_lintegral_le_one ?_ hXm ?_ + · rintro _ ⟨P, hP, rfl⟩ + have := hS P hP + infer_instance + · rintro _ ⟨P, hPS, rfl⟩ + have := hS P hPS + calc ∫⁻ x, X x ∂(Measure.pi fun _ : Fin m ↦ P) + _ = 2⁻¹ + 2⁻¹ * (b * (Measure.pi fun _ : Fin m ↦ P) A) := by + simp [X, lintegral_add_right _ ((measurable_const.indicator hA).const_mul _), + lintegral_const_mul _ (measurable_const.indicator hA), lintegral_indicator_const hA] + _ ≤ 2⁻¹ + 2⁻¹ * 1 := by gcongr; exact hP P hPS + _ = 1 := by rw [mul_one, ENNReal.inv_two_add_inv_two] + set g : (Fin m → 𝓧) → ℝ := fun x ↦ A.indicator (fun _ ↦ t) x - Real.log 2 + have hg (x : Fin m → 𝓧) : ENNReal.ofReal (Real.exp (g x)) ≤ X x := by + by_cases hx : x ∈ A + · simp only [g, X, Set.indicator_of_mem hx] + rw [Real.exp_sub, Real.exp_log two_pos, ENNReal.ofReal_div_of_pos two_pos, + ENNReal.ofReal_ofNat, div_eq_mul_inv, mul_comm] + exact le_add_self + · simp only [g, X, Set.indicator_of_notMem hx, zero_sub, Real.exp_neg, Real.exp_log two_pos, + mul_zero, add_zero] + rw [ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat] + have hgi : Integrable g Qm := ((integrable_const t).indicator hA).sub (integrable_const _) + calc ((t * Qm.real A - Real.log 2 : ℝ) : EReal) + _ = ∫ᵉ x, (g x : EReal) ∂Qm := by + rw [eintegral_eq_integral hgi] + simp [g, integral_sub ((integrable_const t).indicator hA) (integrable_const _), + integral_indicator_const _ hA, mul_comm] + _ ≤ ∫ᵉ x, (logUtility ∘ X) x ∂Qm := eintegral_mono fun x ↦ by + calc (g x : EReal) + _ = ENNReal.log (ENNReal.ofReal (Real.exp (g x))) := by + rw [ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] + _ ≤ (logUtility ∘ X) x := ENNReal.log_monotone (hg x) + _ ≤ maxLogGrowth Q S m := by + rw [maxLogGrowth_def] + exact hX.eintegral_le_maxUtility _ _ end ProbabilityTheory diff --git a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean index fc565f90..a0218f90 100644 --- a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean +++ b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean @@ -27,8 +27,6 @@ such that every probability measure `R` whose integrals of the `f i` are within ## Main statements -* `ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`: the lower bound on the growth of - `m` observations given by the e-variable `1/2 + (1/2) exp t 1_A`. * `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le`: the bipolar rate equals the smallest relative entropy to the null under the semicontinuity above. @@ -39,9 +37,10 @@ of the event `A` that the empirical averages of the test functions lie in the ne most `exp (- m c)` (`ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`, Csiszár's conditioning argument [Csi84]): condition `P ^ m` on that event, and use the superadditivity of the relative entropy over the coordinates and its convexity. The mixture `1/2 + (1/2) exp (m c) 1_A` is then an -`m`-sample e-variable, whose expected logarithm under `Q ^ m` is at least -`m c Q ^ m (A) - log 2`; the weak law of large numbers under `Q ^ m`, from Chebyshev's inequality, -gives `Q ^ m (A) ≥ 1 - D / m` for a constant `D`, so this is at least `m c - O(1)`. +`m`-sample e-variable, whose expected logarithm under `Q ^ m` is at least `m c Q ^ m (A) - log 2` +(`ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`); the weak law of large numbers +under `Q ^ m`, from Chebyshev's inequality, gives `Q ^ m (A) ≥ 1 - D / m` for a constant `D`, so +this is at least `m c - O(1)`. ## References @@ -59,59 +58,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-- The e-variable `1/2 + (1/2) e ^ t 1_A`, valid when `e ^ t P (A) ≤ 1` for every member `P` of -the null, gives the lower bound `t Q (A) - log 2` on the growth of `m` observations. -/ -lemma le_maxLogGrowth_of_ofReal_exp_mul_le_one (Q : Measure 𝓧) [IsProbabilityMeasure Q] - {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) {m : ℕ} - {A : Set (Fin m → 𝓧)} (hA : MeasurableSet A) {t : ℝ} - (hP : ∀ P ∈ S, ENNReal.ofReal (Real.exp t) * (Measure.pi fun _ : Fin m ↦ P) A ≤ 1) : - ((t * (Measure.pi fun _ : Fin m ↦ Q).real A - Real.log 2 : ℝ) : EReal) ≤ - maxLogGrowth Q S m := by - set Qm := Measure.pi fun _ : Fin m ↦ Q - set b := ENNReal.ofReal (Real.exp t) - set X : (Fin m → 𝓧) → ℝ≥0∞ := fun x ↦ 2⁻¹ + 2⁻¹ * A.indicator (fun _ ↦ b) x - have hXm : Measurable X := measurable_const.add (measurable_const.mul - (measurable_const.indicator hA)) - have hX : IsEVar X ((fun P ↦ Measure.pi fun _ : Fin m ↦ P) '' S) := by - refine IsEVar.of_lintegral_le_one ?_ hXm ?_ - · rintro _ ⟨P, hP, rfl⟩ - have := hS P hP - infer_instance - · rintro _ ⟨P, hPS, rfl⟩ - have := hS P hPS - calc ∫⁻ x, X x ∂(Measure.pi fun _ : Fin m ↦ P) - _ = 2⁻¹ + 2⁻¹ * (b * (Measure.pi fun _ : Fin m ↦ P) A) := by - simp only [X] - rw [lintegral_add_right _ ((measurable_const.indicator hA).const_mul _), - lintegral_const, measure_univ, mul_one, - lintegral_const_mul _ (measurable_const.indicator hA), lintegral_indicator_const hA] - _ ≤ 2⁻¹ + 2⁻¹ * 1 := by gcongr; exact hP P hPS - _ = 1 := by rw [mul_one, ENNReal.inv_two_add_inv_two] - set g : (Fin m → 𝓧) → ℝ := fun x ↦ A.indicator (fun _ ↦ t) x - Real.log 2 - have hg (x : Fin m → 𝓧) : ENNReal.ofReal (Real.exp (g x)) ≤ X x := by - by_cases hx : x ∈ A - · simp only [g, X, Set.indicator_of_mem hx] - rw [Real.exp_sub, Real.exp_log two_pos, ENNReal.ofReal_div_of_pos two_pos, - ENNReal.ofReal_ofNat, div_eq_mul_inv, mul_comm] - exact le_add_self - · simp only [g, X, Set.indicator_of_notMem hx, zero_sub, Real.exp_neg, Real.exp_log two_pos, - mul_zero, add_zero] - rw [ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat] - have hgi : Integrable g Qm := ((integrable_const t).indicator hA).sub (integrable_const _) - calc ((t * Qm.real A - Real.log 2 : ℝ) : EReal) - _ = ∫ᵉ x, (g x : EReal) ∂Qm := by - rw [eintegral_eq_integral hgi, integral_sub ((integrable_const t).indicator hA) - (integrable_const _), integral_indicator_const _ hA, integral_const, probReal_univ, - smul_eq_mul, one_smul, mul_comm] - _ ≤ ∫ᵉ x, (logUtility ∘ X) x ∂Qm := eintegral_mono fun x ↦ by - calc (g x : EReal) - _ = ENNReal.log (ENNReal.ofReal (Real.exp (g x))) := by - rw [ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] - _ ≤ (logUtility ∘ X) x := ENNReal.log_monotone (hg x) - _ ≤ maxLogGrowth Q S m := by - rw [maxLogGrowth_def] - exact hX.eintegral_le_maxUtility _ _ - /-- If the smallest relative entropy to `S` is lower semicontinuous at `Q` for the topology of integrals of bounded measurable functions, in the sense of neighbourhoods, then the bipolar rate of `Q` against `S` equals the smallest relative entropy from `Q` to `S` [RR26, Theorem 4.1]. The @@ -136,7 +82,9 @@ theorem bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le (Q : Measure 𝓧) obtain ⟨k, f, ε, hε, hfm, hfC, hU⟩ := h (ENNReal.ofReal c) (EReal.coe_ennreal_lt_coe_ennreal_iff.1 (hcE ▸ hc)) choose C hC using hfC - set D := ∑ i, C i ^ 2 / ε ^ 2 + have hfL (i : Fin k) : MemLp (f i) 2 Q := + .of_bound (hfm i).aestronglyMeasurable (C i) (.of_forall fun x ↦ (hC i x).trans' (by simp)) + set D := ∑ i, Var[f i; Q] / ε ^ 2 refine le_bipolarRate_of_tendsto (r := fun n ↦ (n + 1) * c * (1 - D / (n + 1)) - Real.log 2) (fun n ↦ ?_) ?_ · -- the e-variable `1/2 + (1/2) exp ((n + 1) c) 1_A`, with the law of large numbers under `Q` @@ -145,13 +93,12 @@ theorem bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le (Q : Measure 𝓧) ofReal_exp_mul_measure_pi_le_one hfm hC hc0'.le (fun R hR hRf ↦ (hU R hR hRf).trans (iInf₂_le P hP)) (m := n + 1) n.succ_ne_zero refine le_trans ?_ (le_maxLogGrowth_of_ofReal_exp_mul_le_one Q hS - (measurableSet_setOf_forall_abs_avg_sub_le hfm _ ε (n + 1)) hsan) - have h := one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le hfm hC Q hε n.succ_ne_zero + (measurableSet_setOf_forall_abs_sum_div_sub_le hfm _ ε (n + 1)) hsan) + have h := one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le hfL hε n.succ_ne_zero refine EReal.coe_le_coe_iff.2 ?_ - have hnc : 0 ≤ ((n + 1 : ℕ) : ℝ) * c := by positivity have hn1 : ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1 := by push_cast; ring - rw [hn1] at hnc h ⊢ - nlinarith + rw [hn1] at h ⊢ + gcongr · have h0 := tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ) have h1 := (tendsto_const_nhds (x := c)).sub (h0.const_mul (c * D + Real.log 2)) rw [mul_zero, sub_zero] at h1 diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean b/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean index 73c53c79..c666957f 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean @@ -17,15 +17,15 @@ The relative entropy from a law to a product law is at least the sum of the rela its marginals to the factors. For two factors, this is the value of Statlib's `maxUtility_fst_add_maxUtility_snd_le` for singleton nulls, where the maximal expected logarithm of an e-variable is the relative entropy (`maxUtility_singleton_eq_klDiv`); for finitely many -factors, it follows by induction on the number of coordinates. +factors, it follows by induction on the number of coordinates, after enumerating them. ## Main statements * `InformationTheory.klDiv_fst_add_klDiv_snd_le`: the relative entropy to a product law is at least the sum of the relative entropies of the two marginals. -* `InformationTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on `Fin n → 𝓧` to a - product law `Measure.pi P` is at least the sum of the relative entropies of its marginals to the - factors `P j`. +* `InformationTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on a finite product + `∀ i, 𝓧 i` to a product law `Measure.pi P` is at least the sum of the relative entropies of its + marginals to the factors `P i`. -/ public section @@ -48,45 +48,67 @@ lemma klDiv_fst_add_klDiv_snd_le (R : Measure (𝓧 × 𝓨)) [IsProbabilityMeas maxUtility_singleton_eq_klDiv, ← EReal.coe_ennreal_add, EReal.coe_ennreal_le_coe_ennreal_iff] at h -/-- The relative entropy from a law on `Fin n → 𝓧` to a product law `Measure.pi P` is at least the -sum of the relative entropies of its marginals to the factors `P j`. -/ -lemma sum_klDiv_map_eval_le {n : ℕ} (P : Fin n → Measure 𝓧) [∀ j, IsProbabilityMeasure (P j)] - (μ : Measure (Fin n → 𝓧)) [IsProbabilityMeasure μ] : +/-- The case of `Fin n` of `sum_klDiv_map_eval_le`, by induction on `n`. -/ +private lemma sum_klDiv_map_eval_le_fin {n : ℕ} {𝓧 : Fin n → Type*} [∀ j, MeasurableSpace (𝓧 j)] + (P : ∀ j, Measure (𝓧 j)) [∀ j, IsProbabilityMeasure (P j)] (μ : Measure (∀ j, 𝓧 j)) + [IsProbabilityMeasure μ] : ∑ j, klDiv (μ.map fun x ↦ x j) (P j) ≤ klDiv μ (Measure.pi P) := by induction n with | zero => simp | succ n ih => - set e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) ↦ 𝓧) 0 + set e := MeasurableEquiv.piFinSuccAbove 𝓧 0 set R := μ.map e + set P' := Measure.pi fun j : Fin n ↦ P ((0 : Fin (n + 1)).succAbove j) -- `e` splits off the first coordinate and carries `Measure.pi P` to a product law - have hpi : (Measure.pi P).map e = (P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ) := by - rw [(measurePreserving_piFinSuccAbove P 0).map_eq] - simp - have hKL : klDiv R ((P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ)) = - klDiv μ (Measure.pi P) := by - rw [← hpi] + have hKL : klDiv R ((P 0).prod P') = klDiv μ (Measure.pi P) := by + rw [← (measurePreserving_piFinSuccAbove P 0).map_eq] exact klDiv_map_measurableEmbedding _ _ e.measurableEmbedding have hfst : R.fst = μ.map fun x ↦ x 0 := by - have h : Prod.fst ∘ e = fun x ↦ x 0 := by - ext x - simp [e, MeasurableEquiv.piFinSuccAbove_apply] + -- the first component of `e x` is `x 0` by definition of `piFinSuccAbove` + have h : Prod.fst ∘ e = fun x ↦ x 0 := rfl rw [Measure.fst, Measure.map_map measurable_fst e.measurable, h] - have hsnd : R.snd = μ.map fun x j ↦ x j.succ := by - have h : Prod.snd ∘ e = fun x j ↦ x j.succ := by - ext x j - simp [e, MeasurableEquiv.piFinSuccAbove_apply, Fin.tail] - rw [Measure.snd, Measure.map_map measurable_snd e.measurable, h] - have hmarg (j : Fin n) : R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x j.succ := by - rw [hsnd, Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] + have hmarg (j : Fin n) : + R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x ((0 : Fin (n + 1)).succAbove j) := by + -- the second component of `e x` is `x ∘ succAbove 0` by definition of `piFinSuccAbove` + have h : ((fun x ↦ x j) ∘ Prod.snd) ∘ e = fun x ↦ x ((0 : Fin (n + 1)).succAbove j) := rfl + rw [Measure.snd, Measure.map_map (measurable_pi_apply j) measurable_snd, + Measure.map_map ((measurable_pi_apply j).comp measurable_snd) e.measurable, h] calc ∑ j, klDiv (μ.map fun x ↦ x j) (P j) - _ = klDiv R.fst (P 0) + ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) (P j.succ) := by - rw [Fin.sum_univ_succ, hfst] + _ = klDiv R.fst (P 0) + + ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) (P ((0 : Fin (n + 1)).succAbove j)) := by + rw [Fin.sum_univ_succAbove _ 0, hfst] simp_rw [hmarg] - _ ≤ klDiv R.fst (P 0) + klDiv R.snd (Measure.pi fun j : Fin n ↦ P j.succ) := by + _ ≤ klDiv R.fst (P 0) + klDiv R.snd P' := by gcongr exact ih _ R.snd - _ ≤ klDiv R ((P 0).prod (Measure.pi fun j : Fin n ↦ P j.succ)) := - klDiv_fst_add_klDiv_snd_le R _ _ + _ ≤ klDiv R ((P 0).prod P') := klDiv_fst_add_klDiv_snd_le R _ _ _ = klDiv μ (Measure.pi P) := hKL +/-- The relative entropy from a law on a finite product `∀ i, 𝓧 i` to a product law +`Measure.pi P` is at least the sum of the relative entropies of its marginals to the factors +`P i`. -/ +lemma sum_klDiv_map_eval_le {ι : Type*} [Fintype ι] {𝓧 : ι → Type*} + [∀ i, MeasurableSpace (𝓧 i)] (P : ∀ i, Measure (𝓧 i)) [∀ i, IsProbabilityMeasure (P i)] + (μ : Measure (∀ i, 𝓧 i)) [IsProbabilityMeasure μ] : + ∑ i, klDiv (μ.map fun x ↦ x i) (P i) ≤ klDiv μ (Measure.pi P) := by + -- transport to `Fin n` along an enumeration of `ι` + set e := (Fintype.equivFin ι).symm + set ψ := MeasurableEquiv.piCongrLeft 𝓧 e + set ν := μ.map ψ.symm + have hν : ν.map ψ = μ := by + rw [Measure.map_map ψ.measurable ψ.symm.measurable, ψ.self_comp_symm, Measure.map_id] + have hKL : klDiv ν (Measure.pi fun a ↦ P (e a)) = klDiv μ (Measure.pi P) := by + rw [← (measurePreserving_piCongrLeft P e).map_eq, ← klDiv_map_measurableEmbedding _ _ + ψ.measurableEmbedding, hν] + have hmarg (a : Fin (Fintype.card ι)) : ν.map (fun x ↦ x a) = μ.map fun x ↦ x (e a) := by + -- `ψ.symm x a = x (e a)` by definition of `piCongrLeft` + have h : (fun x ↦ x a) ∘ ψ.symm = fun x ↦ x (e a) := rfl + rw [Measure.map_map (measurable_pi_apply a) ψ.symm.measurable, h] + calc ∑ i, klDiv (μ.map fun x ↦ x i) (P i) + _ = ∑ a, klDiv (ν.map fun x ↦ x a) (P (e a)) := by + rw [← e.sum_comp] + simp_rw [hmarg] + _ ≤ klDiv ν (Measure.pi fun a ↦ P (e a)) := sum_klDiv_map_eval_le_fin _ ν + _ = klDiv μ (Measure.pi P) := hKL + end InformationTheory diff --git a/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean index 02e62e0b..fe276416 100644 --- a/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean +++ b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean @@ -12,30 +12,30 @@ public import Statlib.Divergence.KullbackLeibler.Basic public import Statlib.ForMathlib.MeasureTheory.Integral.Pi /-! -# Empirical averages of bounded functions under product laws +# Empirical averages of functions under product laws -For finitely many bounded measurable functions `f i` on `𝓧` and `m` observations `x : Fin m → 𝓧`, +For finitely many measurable functions `f i` on `𝓧` and `m` observations `x : Fin m → 𝓧`, this file bounds the probability, under an i.i.d. law `P ^ m`, that the empirical averages `(∑ j, f i (x j)) / m` lie within `ε` of given values `a i`, from both sides. -* From above, by a Sanov-type bound with blocks of length one: if every law whose integrals of - the `f i` are within `ε` of the `a i` is at relative entropy at least `c` from `P`, the - probability is at most `exp (- m c)`. This is Csiszár's argument for Sanov's upper bound on a - convex set [Csi84]: condition `P ^ m` on the event, whose relative entropy to `P ^ m` is at most - `log (1 / P ^ m (A))` (`InformationTheory.klDiv_cond_le`), and bound it from below by the - superadditivity of the relative entropy over the coordinates +* From above, for bounded `f i`, by a Sanov-type bound with blocks of length one: if every law + whose integrals of the `f i` are within `ε` of the `a i` is at relative entropy at least `c` + from `P`, the probability is at most `exp (- m c)`. This is Csiszár's argument for Sanov's + upper bound on a convex set [Csi84]: condition `P ^ m` on the event, whose relative entropy to + `P ^ m` is at most `log (1 / P ^ m (A))` (`InformationTheory.klDiv_cond_le`), and bound it from + below by the superadditivity of the relative entropy over the coordinates (`InformationTheory.sum_klDiv_map_eval_le`) and its convexity, at the average of the marginals of the conditioned law, which is in the neighbourhood. -* From below, when the `a i` are the means of the `f i` under `P`, by the weak law of large - numbers from Chebyshev's inequality. +* From below, for square-integrable `f i` whose means under `P` are the `a i`, by the weak law of + large numbers from Chebyshev's inequality. ## Main statements * `ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`: the Sanov-type bound. -* `ProbabilityTheory.measure_pi_lt_abs_avg_sub_le`: the weak law of large numbers for a bounded - function, `P ^ m (|avg - mean| > ε) ≤ C ^ 2 / (m ε ^ 2)`. -* `ProbabilityTheory.one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le`: the weak law of large - numbers for finitely many bounded functions at once. +* `ProbabilityTheory.measure_pi_lt_abs_sum_div_sub_le`: the weak law of large numbers for a + square-integrable function `g`, `P ^ m (|(∑ j, g (x j)) / m - mean| > ε) ≤ Var[g] / (m ε ^ 2)`. +* `ProbabilityTheory.one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le`: the weak law of + large numbers for finitely many square-integrable functions at once. ## References @@ -54,7 +54,7 @@ variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} /-- The tuples whose empirical averages of the measurable functions `f i` are within `ε` of the `a i` form a measurable set. -/ -lemma measurableSet_setOf_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} +lemma measurableSet_setOf_forall_abs_sum_div_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} (hf : ∀ i, Measurable (f i)) (a : Fin k → ℝ) (ε : ℝ) (m : ℕ) : MeasurableSet {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} := by simp only [Set.ofPred_forall] @@ -62,13 +62,19 @@ lemma measurableSet_setOf_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 (((Finset.measurable_sum _ fun j _ ↦ (hf i).comp (measurable_pi_apply j)).div_const _).sub_const _)) measurable_const +/-- A measurable function `g` bounded by `C` in absolute value, evaluated at one coordinate, is +integrable against every finite measure on `ι → 𝓧`. -/ +lemma integrable_comp_eval_of_abs_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} + (hgC : ∀ x, |g x| ≤ C) {ι : Type*} (μ : Measure (ι → 𝓧)) [IsFiniteMeasure μ] (j : ι) : + Integrable (fun x ↦ g (x j)) μ := + .of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (.of_forall fun _ ↦ hgC _) + /-- The average of the marginals of a probability measure on `Fin m → 𝓧`, for `m ≠ 0`, is a probability measure. -/ lemma isProbabilityMeasure_sum_smul_map_eval {m : ℕ} (hm : m ≠ 0) (μ : Measure (Fin m → 𝓧)) [IsProbabilityMeasure μ] : IsProbabilityMeasure (∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) := - ⟨by simp [ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), - ENNReal.mul_inv_cancel (Nat.cast_ne_zero.2 hm) (ENNReal.natCast_ne_top m)]⟩ + ⟨by simp [ENNReal.coe_inv, hm, ENNReal.mul_inv_cancel]⟩ /-- The integral against the average of the marginals of `μ` is the integral of the empirical average against `μ`. -/ @@ -76,16 +82,13 @@ lemma integral_sum_smul_map_eval {m : ℕ} (μ : Measure (Fin m → 𝓧)) [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) : ∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) = ∫ x, (∑ j, g (x j)) / m ∂μ := by - have hint (ν : Measure 𝓧) [IsFiniteMeasure ν] : Integrable g ν := - Integrable.of_bound hg.aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC x) - rw [integral_finsetSum_measure fun j _ ↦ (hint _).smul_measure ENNReal.coe_ne_top] + have hgj := integrable_comp_eval_of_abs_le hg hgC μ + rw [integral_finsetSum_measure fun j _ ↦ ((integrable_map_measure hg.aestronglyMeasurable + (measurable_pi_apply j).aemeasurable).2 (hgj j)).smul_measure ENNReal.coe_ne_top] have hj (j : Fin m) : ∫ x, g x ∂(μ.map fun x ↦ x j) = ∫ x, g (x j) ∂μ := integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable simp_rw [integral_smul_measure, hj] - have hs : ∫ x, ∑ j, g (x j) ∂μ = ∑ j, ∫ x, g (x j) ∂μ := - integral_finsetSum _ fun j _ ↦ Integrable.of_bound - (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (Eventually.of_forall fun x ↦ hgC _) - rw [integral_div, hs] + rw [integral_div, integral_finsetSum _ fun j _ ↦ hgj j] simp [div_eq_inv_mul, Finset.mul_sum] /-- If the empirical average of a bounded measurable function `g` is almost surely within `ε` of @@ -96,9 +99,7 @@ lemma abs_integral_sum_smul_map_eval_sub_le {m : ℕ} (μ : Measure (Fin m → |∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) - a| ≤ ε := by rw [integral_sum_smul_map_eval μ hg hgC] have hint : Integrable (fun x : Fin m → 𝓧 ↦ (∑ j, g (x j)) / m) μ := - ((integrable_finsetSum _ fun j _ ↦ Integrable.of_bound - (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C - (Eventually.of_forall fun x ↦ hgC _))).div_const _ + (integrable_finsetSum _ fun j _ ↦ integrable_comp_eval_of_abs_le hg hgC μ j).div_const _ have heq : ∫ x, (∑ j, g (x j)) / m ∂μ - a = ∫ x, ((∑ j, g (x j)) / m - a) ∂μ := by rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul] rw [heq, ← Real.norm_eq_abs] @@ -118,16 +119,15 @@ lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (h (Measure.pi fun _ : Fin m ↦ P) {x | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} ≤ 1 := by set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} set Pm := Measure.pi fun _ : Fin m ↦ P - have hA : MeasurableSet A := measurableSet_setOf_forall_abs_avg_sub_le hf a ε m + have hA : MeasurableSet A := measurableSet_setOf_forall_abs_sum_div_sub_le hf a ε m rcases eq_or_ne (Pm A) 0 with h0 | h0 · simp [h0] -- the law `μ` of `m` observations conditioned on the event, and the average `R` of its marginals set μ := Pm[|A] have : IsProbabilityMeasure μ := cond_isProbabilityMeasure h0 - have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm set w : Fin m → ℝ≥0 := fun _ ↦ (m : ℝ≥0)⁻¹ have hw : ∑ j, w j = 1 := by - simp [w, Finset.card_univ, mul_inv_cancel₀ (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0)] + simp [w, hm] set R := ∑ j, (w j : ℝ≥0∞) • μ.map fun x ↦ x j have hR : IsProbabilityMeasure R := isProbabilityMeasure_sum_smul_map_eval hm μ have hRU (i : Fin k) : |∫ x, f i x ∂R - a i| ≤ ε := by @@ -143,102 +143,90 @@ lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (h gcongr exact klDiv_sum_smul_left_le hw _ = ∑ j, klDiv (μ.map fun x ↦ x j) P := by - rw [Finset.mul_sum] - refine Finset.sum_congr rfl fun j _ ↦ ?_ - rw [← mul_assoc, ENNReal.coe_inv (Nat.cast_ne_zero.2 hm : (m : ℝ≥0) ≠ 0), - ENNReal.coe_natCast, ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m), one_mul] + simp [w, Finset.mul_sum, ← mul_assoc, ENNReal.coe_inv, hm, ENNReal.mul_inv_cancel] _ ≤ klDiv μ Pm := sum_klDiv_map_eval_le (fun _ ↦ P) μ -- the relative entropy from `μ` to `P ^ m` is at most `log (1 / P ^ m (A))`: take logarithms - rw [← ENNReal.le_inv_iff_mul_le, ← ENNReal.log_le_log_iff, - ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] - calc ((m * c : ℝ) : EReal) - _ = ((ENNReal.ofReal (m * c) : ℝ≥0∞) : EReal) := by - rw [EReal.coe_ennreal_ofReal, max_eq_left (by positivity)] - _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by - rw [ENNReal.ofReal_mul (Nat.cast_nonneg _), ENNReal.ofReal_natCast] - _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1 - _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0 + have h2 : ((m * c : ℝ) : EReal) ≤ ENNReal.log (Pm A)⁻¹ := by + calc ((m * c : ℝ) : EReal) + _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by + simp [← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, EReal.coe_ennreal_ofReal, + max_eq_left (mul_nonneg (Nat.cast_nonneg m) hc)] + _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1 + _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0 + -- take exponentials + refine ENNReal.le_inv_iff_mul_le.1 (ENNReal.log_le_log_iff.1 ?_) + simpa [ENNReal.log_ofReal_of_pos (Real.exp_pos _)] using h2 /-- **Weak law of large numbers**, by Chebyshev's inequality: the probability that the empirical -average of a function bounded by `C` deviates by more than `ε` from its mean is at most -`C ^ 2 / (m ε ^ 2)`. -/ -lemma measure_pi_lt_abs_avg_sub_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) - (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : +average of a square-integrable function `g` deviates by more than `ε` from its mean is at most +`Var[g; Q] / (m ε ^ 2)`. -/ +lemma measure_pi_lt_abs_sum_div_sub_le {g : 𝓧 → ℝ} {Q : Measure 𝓧} [IsProbabilityMeasure Q] + (hg : MemLp g 2 Q) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : (Measure.pi fun _ : Fin m ↦ Q) {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} ≤ - ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by + ENNReal.ofReal (Var[g; Q] / (m * ε ^ 2)) := by set Qm := Measure.pi fun _ : Fin m ↦ Q - set X : (Fin m → 𝓧) → ℝ := fun x ↦ ∑ j, g (x j) with hX_def + set X : (Fin m → 𝓧) → ℝ := ∑ j : Fin m, fun x ↦ g (x j) with hX_def have hm' : (0 : ℝ) < m := Nat.cast_pos.2 (Nat.pos_of_ne_zero hm) have hgL (j : Fin m) : MemLp (fun x : Fin m → 𝓧 ↦ g (x j)) 2 Qm := - MemLp.of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C - (Eventually.of_forall fun x ↦ hgC _) - have hXL : MemLp X 2 Qm := memLp_finsetSum _ fun j _ ↦ hgL j + hg.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m ↦ Q) j) + have hXL : MemLp X 2 Qm := memLp_finsetSum' _ fun j _ ↦ hgL j have hEX : ∫ x, X x ∂Qm = m * ∫ y, g y ∂Q := by have hj (j : Fin m) : ∫ x, g (x j) ∂Qm = ∫ y, g y ∂Q := by - rw [← integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable] - congr 1 - exact (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq - rw [integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two] - simp [hj] - have hVar : Var[X; Qm] ≤ m * C ^ 2 := by - have h := variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) - fun _ ↦ MemLp.of_bound hg.aestronglyMeasurable C (Eventually.of_forall hgC) - have hX : X = ∑ j : Fin m, fun x : Fin m → 𝓧 ↦ g (x j) := by - ext x - simp [X] - rw [hX, h, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] - gcongr - have hb := variance_le_sq_of_bounded (μ := Q) (a := -C) (b := C) - (Eventually.of_forall fun x ↦ abs_le.1 (hgC x)) hg.aemeasurable - convert hb using 1 - ring + have h := (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq + rw [← integral_map (measurable_pi_apply j).aemeasurable (h ▸ hg.aestronglyMeasurable), h] + simp [X, integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two, hj] + have hVar : Var[X; Qm] = m * Var[g; Q] := by + rw [hX_def, variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) fun _ ↦ hg] + simp calc Qm {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} _ ≤ Qm {x | m * ε ≤ |X x - ∫ x, X x ∂Qm|} := by refine measure_mono fun x hx ↦ ?_ simp only [Set.mem_ofPred_eq] at hx ⊢ have h : (∑ j, g (x j)) / m - ∫ y, g y ∂Q = (X x - ∫ x, X x ∂Qm) / m := by - rw [hEX, hX_def] + rw [hEX, hX_def, Finset.sum_apply] field_simp rw [h, abs_div, abs_of_pos hm', lt_div_iff₀ hm'] at hx linarith _ ≤ ENNReal.ofReal (Var[X; Qm] / (m * ε) ^ 2) := meas_ge_le_variance_div_sq hXL (by positivity) - _ ≤ ENNReal.ofReal (C ^ 2 / (m * ε ^ 2)) := by - refine ENNReal.ofReal_le_ofReal ?_ - calc Var[X; Qm] / (m * ε) ^ 2 - _ ≤ m * C ^ 2 / (m * ε) ^ 2 := by gcongr - _ = C ^ 2 / (m * ε ^ 2) := by field_simp - -/-- **Weak law of large numbers** for finitely many functions `f i` bounded by `C i`: with -probability at least `1 - (∑ i, C i ^ 2 / ε ^ 2) / m` under `Q ^ m`, the empirical averages of all -the `f i` are within `ε` of their means. -/ -lemma one_sub_div_le_measureReal_pi_forall_abs_avg_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} - (hf : ∀ i, Measurable (f i)) {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) - (Q : Measure 𝓧) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) : - 1 - (∑ i, C i ^ 2 / ε ^ 2) / m ≤ + _ = ENNReal.ofReal (Var[g; Q] / (m * ε ^ 2)) := by + rw [hVar] + congr 1 + field_simp + +/-- **Weak law of large numbers** for finitely many square-integrable functions `f i`: with +probability at least `1 - (∑ i, Var[f i; Q] / ε ^ 2) / m` under `Q ^ m`, the empirical averages of +all the `f i` are within `ε` of their means. -/ +lemma one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ} + {Q : Measure 𝓧} [IsProbabilityMeasure Q] (hf : ∀ i, MemLp (f i) 2 Q) {ε : ℝ} (hε : 0 < ε) + {m : ℕ} (hm : m ≠ 0) : + 1 - (∑ i, Var[f i; Q] / ε ^ 2) / m ≤ (Measure.pi fun _ : Fin m ↦ Q).real {x | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} := by + set Qm := Measure.pi fun _ : Fin m ↦ Q set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} have hcompl : Aᶜ = ⋃ i, {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} := by ext x simp [A] - have hle : (Measure.pi fun _ : Fin m ↦ Q) Aᶜ ≤ - ENNReal.ofReal ((∑ i, C i ^ 2 / ε ^ 2) / m) := by + have hle : Qm Aᶜ ≤ ENNReal.ofReal ((∑ i, Var[f i; Q] / ε ^ 2) / m) := by rw [hcompl] refine (measure_iUnion_fintype_le _ _).trans ?_ - calc ∑ i, (Measure.pi fun _ : Fin m ↦ Q) - {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} - _ ≤ ∑ i, ENNReal.ofReal (C i ^ 2 / (m * ε ^ 2)) := - Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_avg_sub_le (hf i) (hfC i) Q hε hm - _ = ENNReal.ofReal ((∑ i, C i ^ 2 / ε ^ 2) / m) := by - rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦ by positivity] + calc ∑ i, Qm {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} + _ ≤ ∑ i, ENNReal.ofReal (Var[f i; Q] / (m * ε ^ 2)) := + Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_sum_div_sub_le (hf i) hε hm + _ = ENNReal.ofReal ((∑ i, Var[f i; Q] / ε ^ 2) / m) := by + rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦ + div_nonneg (variance_nonneg _ _) (by positivity)] congr 1 simp only [Finset.sum_div] refine Finset.sum_congr rfl fun i _ ↦ ?_ field_simp - have h := ENNReal.toReal_le_of_le_ofReal (by positivity) hle - rw [← measureReal_def, probReal_compl_eq_one_sub - (measurableSet_setOf_forall_abs_avg_sub_le hf _ ε m)] at h + have h := ENNReal.toReal_le_of_le_ofReal + (div_nonneg (Finset.sum_nonneg fun i _ ↦ div_nonneg (variance_nonneg _ _) (by positivity)) + (Nat.cast_nonneg _)) hle + rw [← measureReal_def] at h + have hu : 1 ≤ Qm.real A + Qm.real Aᶜ := by + simpa using measureReal_union_le (μ := Qm) A Aᶜ linarith end ProbabilityTheory