From e8e5a137c8888aee6b938fb0473bc5a62e0adb14 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 13:22:27 +0100 Subject: [PATCH 1/5] feat: likelihood ratios of sequential predictors and time-uniform KL concentration by the Laplace mixture [JKMDLV20, Proposition 1] Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- LMLExplore/Data/Nat/Choose/Bounds.lean | 78 ++++ .../InformationTheory/LaplaceMixture.lean | 367 ++++++++++++++++++ .../Martingale/LikelihoodRatio.lean | 277 +++++++++++++ .../SequentialLearning/FiniteActions.lean | 30 +- 4 files changed, 751 insertions(+), 1 deletion(-) create mode 100644 LMLExplore/Data/Nat/Choose/Bounds.lean create mode 100644 LMLExplore/InformationTheory/LaplaceMixture.lean create mode 100644 LMLExplore/Probability/Martingale/LikelihoodRatio.lean diff --git a/LMLExplore/Data/Nat/Choose/Bounds.lean b/LMLExplore/Data/Nat/Choose/Bounds.lean new file mode 100644 index 00000000..708182f6 --- /dev/null +++ b/LMLExplore/Data/Nat/Choose/Bounds.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Analysis.Complex.Exponential +public import Mathlib.Data.Nat.Choose.Bounds +public import Mathlib.Data.Nat.Choose.Multinomial + +/-! +# Bounds on binomial and multinomial coefficients + +Two classical upper bounds on the number of words with prescribed letter counts. + +* `Nat.choose_le_exp_one_mul_div_pow`: `n.choose k ≤ (e n / k) ^ k`, from Mathlib's + `Nat.choose_le_pow_div` and `k ^ k / k! ≤ e ^ k`. +* `Nat.multinomial_mul_prod_pow_le_one`: for a probability vector `p` on `s`, the term + `multinomial s f * ∏ i ∈ s, p i ^ f i` of the multinomial expansion of `(∑ i ∈ s, p i) ^ n` is at + most `1`. It is the probability of the counts `f` in `n` independent draws from `p`. With + `p i = f i / n`, it bounds the maximum likelihood `∏ i ∈ s, (f i / n) ^ f i` of a word with counts + `f` by `∏ i ∈ s, (f i)! / n!`. + +Both bounds control the likelihood ratios of universal (mixture) predictors against the maximum +likelihood, as in the analysis of Laplace's rule of succession. +-/ + +public section + +open Finset Real +open scoped Nat + +namespace Nat + +/-- **Binomial coefficients are at most `(e n / k) ^ k`.** -/ +theorem choose_le_exp_one_mul_div_pow (n k : ℕ) : + (n.choose k : ℝ) ≤ (exp 1 * n / k) ^ k := by + rcases Nat.eq_zero_or_pos k with rfl | hk + · simp + have hkR : (0 : ℝ) < k := by exact_mod_cast hk + -- `k ^ k / k! ≤ e ^ k` + have hfact : (k : ℝ) ^ k / k ! ≤ exp 1 ^ k := by + rw [← exp_nat_mul, mul_one] + exact pow_div_factorial_le_exp _ hkR.le k + calc (n.choose k : ℝ) ≤ (n : ℝ) ^ k / k ! := choose_le_pow_div k n + _ = ((n : ℝ) / k) ^ k * ((k : ℝ) ^ k / k !) := by + rw [div_pow] + field_simp + _ ≤ ((n : ℝ) / k) ^ k * exp 1 ^ k := by gcongr + _ = (exp 1 * n / k) ^ k := by rw [← mul_pow, mul_comm, mul_div_assoc] + +/-- **A multinomial probability is at most one**: for `p` nonnegative on `s` with +`∑ i ∈ s, p i = 1`, `multinomial s f * ∏ i ∈ s, p i ^ f i ≤ 1`. This term of the multinomial +expansion of `(∑ i ∈ s, p i) ^ (∑ i ∈ s, f i)` is the probability of the counts `f` under +independent draws from `p`. -/ +theorem multinomial_mul_prod_pow_le_one {R ι : Type*} [CommSemiring R] [PartialOrder R] + [IsOrderedRing R] (s : Finset ι) (f : ι → ℕ) {p : ι → R} (hp0 : ∀ i ∈ s, 0 ≤ p i) + (hp1 : ∑ i ∈ s, p i = 1) : + (multinomial s f : R) * ∏ i ∈ s, p i ^ f i ≤ 1 := by + classical + -- the counts `f`, set to `0` outside `s`, are a term of the multinomial expansion + set g : ι → ℕ := fun i ↦ if i ∈ s then f i else 0 with hg + have hgf : ∀ i ∈ s, g i = f i := fun i hi ↦ by simp [hg, hi] + have hg_mem : g ∈ piAntidiag s (∑ i ∈ s, f i) := by + rw [mem_piAntidiag] + refine ⟨sum_congr rfl hgf, fun i hi ↦ ?_⟩ + by_contra his + simp [hg, his] at hi + have hexp := sum_pow_eq_sum_piAntidiag s p (∑ i ∈ s, f i) + rw [hp1, one_pow] at hexp + rw [multinomial_congr (fun i hi ↦ (hgf i hi).symm), + prod_congr rfl fun i hi ↦ by rw [← hgf i hi], hexp] + exact single_le_sum (f := fun k ↦ (multinomial s k : R) * ∏ i ∈ s, p i ^ k i) + (fun k _ ↦ mul_nonneg (Nat.cast_nonneg _) (prod_nonneg fun i hi ↦ pow_nonneg (hp0 i hi) _)) + hg_mem + +end Nat diff --git a/LMLExplore/InformationTheory/LaplaceMixture.lean b/LMLExplore/InformationTheory/LaplaceMixture.lean new file mode 100644 index 00000000..7bfcbda3 --- /dev/null +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -0,0 +1,367 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.Independence.InfinitePi +public import LMLExplore.Data.Nat.Choose.Bounds +public import LMLExplore.Probability.Martingale.LikelihoodRatio +public import LMLExplore.Probability.Martingale.Ville +public import LMLExplore.SequentialLearning.FiniteActions +public import TauCeti.MeasureTheory.Measure.Decomposition.Lebesgue +public import TauCeti.Probability.Process.EmpiricalMeasure + +/-! +# Time-uniform concentration of empirical distributions by the Laplace mixture + +Let `ξ 0, ξ 1, …` be independent with law `ν` on a finite type `α` with `m` elements, let +`N_n(a) = #{k < n | ξ k = a}` be the counts (LML's `pullCount`) and `p̂_n` the empirical +distribution of `ξ 0, …, ξ (n - 1)` (Tau Ceti's `empiricalFiniteMeasure`). For every `δ > 0`, +`P(∃ n ≥ 1, log (1/δ) + (m - 1) log (e (1 + n / (m - 1))) ≤ n KL(p̂_n ‖ ν)) ≤ δ` +[JKMDLV20, Proposition 1]. + +The proof uses *Laplace's rule of succession*, the sequential predictor +`q_t(a) = (N_t(a) + 1) / (t + m)` (`LMLExplore.laplacePredictor`). Its likelihood ratio +`L_n = ∏_{t < n} q_t(ξ t) / ν{ξ t}` against `ν` is a nonnegative supermartingale with `L_0 = 1` +(`LMLExplore.supermartingale_predictorLikelihoodRatio`), so that Ville's inequality bounds by `δ` +the probability that it ever reaches `1 / δ`. The likelihood of the rule of succession is +`∏_{t < n} q_t(ξ t) = ∏ₐ N_n(a)! / (m (m + 1) ⋯ (m + n - 1))` +(`LMLExplore.prod_range_laplacePredictor`), the mixture of the likelihoods `∏_{t < n} p(ξ t)` over +the uniform law of the probability vector `p`. It is within the factor +`binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` of the maximum likelihood +`∏ₐ (N_n(a) / n)^{N_n(a)} = exp (n KL(p̂_n ‖ ν)) ∏_{t < n} ν{ξ t}`, by the multinomial bound +`Nat.multinomial_mul_prod_pow_le_one` +(`LMLExplore.exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor`). + +## Main statements + +* `LMLExplore.exp_mul_toReal_klDiv_empiricalFiniteMeasure`: for a finite family `x` of points + charged by `ν`, `exp (card κ KL(p̂ ‖ ν)) = ∏ᵢ p̂{x i} / ν{x i}`. +* `LMLExplore.exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor`: + `exp (n KL(p̂_n ‖ ν)) ≤ (e (1 + n / (m - 1)))^{m - 1} L_n`. +* `LMLExplore.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le`: the time-uniform bound, + for observations adapted to a filtration, each independent of the past. +* `ProbabilityTheory.iIndepFun.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le`: the + time-uniform bound for independent observations. + +## Implementation notes + +[JKMDLV20, Proposition 1] states the event with a strict inequality; the event here, with `≤`, +contains it. For `m = 1` the second term of the threshold vanishes. + +The time-uniform bound is adapted from `InformationTheory/KLTimeUniform.lean` of the formalization +RemyDegenne/Essakine2026Tight (commit 38bbd16f, directory `ForLMLExplore/`), which bounds the same +mixture with Stirling's formula and obtains the threshold +`log (1/δ) + (m - 1) log (n + 1) + 1 + log n / 2`. + +## References + +* [JKMDLV20] A. Jonsson, E. Kaufmann, P. Ménard, O. D. Domingues, E. Leurent and M. Valko, + *Planning in Markov decision processes with gap-dependent sample complexity*, NeurIPS 2020, + Proposition 1. +* [EV26] Y. Essakine and C. Vernade, *Tight sample complexity bounds for entropic best policy + identification*, 2026, Lemma 5. +-/ + +public section + +open MeasureTheory ProbabilityTheory Finset Real Learning TauCeti.Probability InformationTheory +open scoped ENNReal Nat + +namespace LMLExplore + +variable {α Ω : Type*} [Fintype α] [DecidableEq α] {mΩ : MeasurableSpace Ω} {ξ : ℕ → Ω → α} + +/-! ### Laplace's rule of succession -/ + +/-- **Laplace's rule of succession**: after the observations `ξ 0, …, ξ (t - 1)`, predict `a` with +probability `(N_t(a) + 1) / (t + m)`, where `N_t(a)` is the number of occurrences of `a` and `m` +the cardinality of `α`. -/ +noncomputable def laplacePredictor (ξ : ℕ → Ω → α) (t : ℕ) (ω : Ω) (a : α) : ℝ := + (pullCount ξ a t ω + 1) / (t + Fintype.card α) + +lemma laplacePredictor_def (t : ℕ) (ω : Ω) (a : α) : + laplacePredictor ξ t ω a = (pullCount ξ a t ω + 1) / (t + Fintype.card α) := + (rfl) + +lemma laplacePredictor_nonneg (t : ℕ) (ω : Ω) (a : α) : 0 ≤ laplacePredictor ξ t ω a := by + rw [laplacePredictor_def] + positivity + +/-- The rule of succession predicts a probability vector. -/ +lemma sum_laplacePredictor (t : ℕ) (ω : Ω) : ∑ a, laplacePredictor ξ t ω a = 1 := by + have : Nonempty α := ⟨ξ 0 ω⟩ + have hm : (0 : ℝ) < t + Fintype.card α := by positivity + simp_rw [laplacePredictor_def, ← sum_div, sum_add_distrib, sum_natCast_pullCount, sum_const, + card_univ, nsmul_eq_mul, mul_one, div_self hm.ne'] + +/-- If `ξ s` is `ℱ (s + 1)`-measurable for every `s`, the rule of succession at time `t` is +`ℱ t`-measurable. -/ +lemma measurable_laplacePredictor [MeasurableSpace α] [MeasurableSingletonClass α] + {ℱ : Filtration ℕ mΩ} (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) (t : ℕ) (a : α) : + Measurable[ℱ t] (fun ω ↦ laplacePredictor ξ t ω a) := by + simp_rw [laplacePredictor_def, pullCount_eq_sum, Nat.cast_sum, Nat.cast_ite, Nat.cast_one, + Nat.cast_zero] + refine ((Finset.measurable_sum _ fun s hs ↦ Measurable.ite ?_ measurable_const + measurable_const).add_const 1).div_const _ + exact (hξ s).mono (ℱ.mono (mem_range.1 hs)) le_rfl (measurableSet_singleton a) + +/-- **The likelihood of the rule of succession**: `∏_{t < n} q_t(ξ t) = ∏ₐ N_n(a)! / m^{(n)}`, +where `m^{(n)} = m (m + 1) ⋯ (m + n - 1)` is the ascending factorial. -/ +lemma prod_range_laplacePredictor (n : ℕ) (ω : Ω) : + ∏ t ∈ range n, laplacePredictor ξ t ω (ξ t ω) = + (∏ a, ((pullCount ξ a n ω)! : ℝ)) / (Fintype.card α).ascFactorial n := by + simp_rw [laplacePredictor_def, prod_div_distrib, Nat.ascFactorial_eq_prod_range] + congr 1 + · exact_mod_cast prod_range_pullCount_action_add_one n ω + · push_cast + exact prod_congr rfl fun t _ ↦ add_comm _ _ + +/-! ### The divergence of an empirical distribution -/ + +section Empirical + +variable [MeasurableSpace α] [MeasurableSingletonClass α] + +omit [Fintype α] in +/-- The mass of a point under the empirical distribution of `ξ 0, …, ξ (n - 1)` is its frequency +`N_n(a) / n`. -/ +lemma measureReal_empiricalFiniteMeasure_singleton_eq_pullCount (n : ℕ) (ω : Ω) (a : α) : + (empiricalFiniteMeasure (fun k : Fin n ↦ ξ k ω) : Measure α).real {a} = + pullCount ξ a n ω / n := by + have h_sum : ∑ k : Fin n, ({a} : Set α).indicator (1 : α → ℝ≥0∞) (ξ k ω) = pullCount ξ a n ω := by + rw [pullCount_eq_sum, Nat.cast_sum, + ← Fin.sum_univ_eq_sum_range (fun s ↦ ((if ξ s ω = a then 1 else 0 : ℕ) : ℝ≥0∞))] + refine sum_congr rfl fun k _ ↦ ?_ + simp [Set.indicator_apply] + rw [measureReal_def, empiricalFiniteMeasure_apply (measurableSet_singleton a), h_sum, + ENNReal.toReal_mul, ENNReal.toReal_inv, Fintype.card_fin, ENNReal.toReal_natCast, + ENNReal.toReal_natCast, inv_mul_eq_div] + +omit [Fintype α] [DecidableEq α] in +/-- **The divergence of an empirical distribution**: for a nonempty finite family `x` of points +charged by a probability measure `ν`, with empirical distribution `p̂`, +`exp (card κ KL(p̂ ‖ ν)) = ∏ᵢ p̂{x i} / ν{x i}`. -/ +theorem exp_mul_toReal_klDiv_empiricalFiniteMeasure {κ : Type*} [Fintype κ] [Nonempty κ] + {ν : Measure α} [IsProbabilityMeasure ν] {x : κ → α} (hx : ∀ i, ν {x i} ≠ 0) : + exp (Fintype.card κ * (klDiv (empiricalFiniteMeasure x : Measure α) ν).toReal) = + ∏ i, (empiricalFiniteMeasure x : Measure α).real {x i} / ν.real {x i} := by + set p : Measure α := (empiricalFiniteMeasure x : Measure α) + have hκ : (0 : ℝ) < Fintype.card κ := by exact_mod_cast Fintype.card_pos + -- the empirical distribution only charges the points `x i` + have hac : p ≪ ν := Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ by + rw [empiricalFiniteMeasure_apply hs, sum_eq_zero fun i _ ↦ Set.indicator_of_notMem + (fun hi ↦ hx i (measure_mono_null (Set.singleton_subset_iff.2 hi) hνs)) _, mul_zero] + have hp_pos : ∀ i, 0 < p.real {x i} := fun i ↦ by + refine ENNReal.toReal_pos ?_ (measure_ne_top _ _) + rw [empiricalFiniteMeasure_apply (measurableSet_singleton _)] + refine mul_ne_zero (by simp) (ne_of_gt ?_) + refine lt_of_lt_of_le ?_ (single_le_sum (fun j _ ↦ zero_le) (mem_univ i)) + simp + have hν_pos : ∀ i, 0 < ν.real {x i} := fun i ↦ + ENNReal.toReal_pos (hx i) (measure_ne_top _ _) + have h_llr : ∀ i, llr p ν (x i) = log (p.real {x i} / ν.real {x i}) := fun i ↦ by + simp only [llr_def, Measure.rnDeriv_eq_measure_singleton_div (hx i) (measure_ne_top _ _), + ENNReal.toReal_div, measureReal_def] + rw [toReal_klDiv_of_measure_eq hac (by simp only [p, measure_univ]), + integral_empiricalFiniteMeasure_of_measurableSingletonClass, smul_eq_mul, ← mul_assoc, + mul_inv_cancel₀ hκ.ne', one_mul, exp_sum] + exact prod_congr rfl fun i _ ↦ by + rw [h_llr, exp_log (div_pos (hp_pos i) (hν_pos i))] + +end Empirical + +/-! ### The likelihood ratio of the rule of succession -/ + +section Ratio + +variable [MeasurableSpace α] [MeasurableSingletonClass α] {ν : Measure α} + +/-- **The rule of succession is within `(e (1 + n / (m - 1)))^{m - 1}` of the maximum +likelihood**: if `n ≥ 1` and `ν` charges `ξ 0, …, ξ (n - 1)`, the empirical distribution `p̂_n` of +these observations satisfies `exp (n KL(p̂_n ‖ ν)) ≤ (e (1 + n / (m - 1)))^{m - 1} L_n`, where +`L_n` is the likelihood ratio of the rule of succession against `ν` and `m` the cardinality of +`α`. -/ +theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor + [IsProbabilityMeasure ν] {n : ℕ} (hn : n ≠ 0) {ω : Ω} (hξ : ∀ k < n, ν {ξ k ω} ≠ 0) : + exp (n * (klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) ν).toReal) ≤ + (exp 1 * (1 + n / (Fintype.card α - 1 : ℕ))) ^ (Fintype.card α - 1) * + predictorLikelihoodRatio ν (laplacePredictor ξ) ξ n ω := by + have : Nonempty (Fin n) := ⟨⟨0, Nat.pos_of_ne_zero hn⟩⟩ + have : Nonempty α := ⟨ξ 0 ω⟩ + set m := Fintype.card α with hm_def + have hm : 1 ≤ m := Fintype.card_pos + set N : α → ℕ := fun a ↦ pullCount ξ a n ω with hN + have hnR : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn + have hN_sum : ∑ a, N a = n := sum_pullCount + -- `P = ∏_{t < n} ν{ξ t} > 0` + set P := ∏ t ∈ range n, ν.real {ξ t ω} + have hP : 0 < P := prod_pos fun t ht ↦ ENNReal.toReal_pos (hξ t (mem_range.1 ht)) + (measure_ne_top _ _) + -- the maximum likelihood: `exp (n KL(p̂_n ‖ ν)) P = ∏ₐ (N a / n) ^ N a` + have h_max : exp (n * (klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) + ν).toReal) = (∏ a, ((N a : ℝ) / n) ^ N a) / P := by + have h := exp_mul_toReal_klDiv_empiricalFiniteMeasure (ν := ν) + (x := fun k : Fin n ↦ ξ k ω) fun k ↦ hξ k k.2 + rw [Fintype.card_fin] at h + rw [h, Fin.prod_univ_eq_prod_range (fun t ↦ (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : + Measure α).real {ξ t ω} / ν.real {ξ t ω}) n, prod_div_distrib] + simp_rw [measureReal_empiricalFiniteMeasure_singleton_eq_pullCount] + rw [← prod_pow_pullCount (A := ξ) (fun a ↦ (pullCount ξ a n ω : ℝ) / n) n ω] + -- the likelihood of the rule of succession: `L_n P = ∏ₐ N a ! / m^{(n)}` + have h_lap : predictorLikelihoodRatio ν (laplacePredictor ξ) ξ n ω = + (∏ a, ((N a)! : ℝ)) / m.ascFactorial n / P := by + rw [predictorLikelihoodRatio_def, prod_div_distrib, prod_range_laplacePredictor] + -- the multinomial bound: `∏ₐ (N a / n) ^ N a ≤ ∏ₐ N a ! / n!` + have h_mult : ∏ a, ((N a : ℝ) / n) ^ N a ≤ (∏ a, ((N a)! : ℝ)) / n ! := by + have h1 := Nat.multinomial_mul_prod_pow_le_one univ N (p := fun a ↦ (N a : ℝ) / n) + (fun a _ ↦ by positivity) (by rw [← sum_div, ← Nat.cast_sum, hN_sum, div_self hnR.ne']) + have h2 : (∏ a, ((N a)! : ℝ)) * (Nat.multinomial univ N : ℝ) = n ! := by + exact_mod_cast hN_sum ▸ Nat.multinomial_spec univ N + have h3 : (0 : ℝ) < Nat.multinomial univ N := by exact_mod_cast Nat.multinomial_pos _ _ + rw [le_div_iff₀ (by positivity), ← h2] + nlinarith [prod_nonneg fun a (_ : a ∈ univ) ↦ (Nat.cast_nonneg (N a)! : (0 : ℝ) ≤ _), + mul_le_mul_of_nonneg_left h1 (prod_nonneg fun a (_ : a ∈ univ) ↦ + (Nat.cast_nonneg (N a)! : (0 : ℝ) ≤ _))] + -- the binomial bound: `m^{(n)} / n! = binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` + have h_choose : (m.ascFactorial n : ℝ) / n ! ≤ + (exp 1 * (1 + n / (m - 1 : ℕ))) ^ (m - 1) := by + rw [Nat.ascFactorial_eq_factorial_mul_choose', Nat.cast_mul, mul_div_cancel_left₀ _ + (by positivity), show m + n - 1 = (m - 1) + n by omega, ← Nat.choose_symm_add] + refine (Nat.choose_le_exp_one_mul_div_pow _ _).trans_eq ?_ + rcases Nat.eq_zero_or_pos (m - 1) with h0 | h0 + · simp [h0] + · have : (0 : ℝ) < (m - 1 : ℕ) := by exact_mod_cast h0 + congr 1 + push_cast + field_simp + rw [h_max, h_lap] + have h_asc : (0 : ℝ) < m.ascFactorial n := by + obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le hm + rw [hk, add_comm] + exact_mod_cast Nat.ascFactorial_pos k n + rw [div_le_iff₀ hP, mul_div_assoc', div_mul_cancel₀ _ hP.ne'] + calc ∏ a, ((N a : ℝ) / n) ^ N a ≤ (∏ a, ((N a)! : ℝ)) / n ! := h_mult + _ = (m.ascFactorial n : ℝ) / n ! * ((∏ a, ((N a)! : ℝ)) / m.ascFactorial n) := by + field_simp + _ ≤ _ := by gcongr + +/-- On the deviation event, the likelihood ratio of the rule of succession is at least `1 / δ`. -/ +private lemma one_div_le_predictorLikelihoodRatio [IsProbabilityMeasure ν] {n : ℕ} (hn : n ≠ 0) + {ω : Ω} (hξ : ∀ k < n, ν {ξ k ω} ≠ 0) {δ : ℝ} (hδ : 0 < δ) + (h : ENNReal.ofReal (log (1 / δ) + ((Fintype.card α : ℝ) - 1) * + log (exp 1 * (1 + n / ((Fintype.card α : ℝ) - 1)))) ≤ + n * klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) ν) : + 1 / δ ≤ predictorLikelihoodRatio ν (laplacePredictor ξ) ξ n ω := by + have : Nonempty α := ⟨ξ 0 ω⟩ + set p : Measure α := (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) + have hm : ((Fintype.card α - 1 : ℕ) : ℝ) = (Fintype.card α : ℝ) - 1 := by + rw [Nat.cast_sub Fintype.card_pos, Nat.cast_one] + set C := (exp 1 * (1 + n / (Fintype.card α - 1 : ℕ))) ^ (Fintype.card α - 1) with hC + have hC_pos : 0 < C := by positivity + -- the divergence is finite, since `p̂_n` is absolutely continuous with respect to `ν` + have hKL : klDiv p ν ≠ ∞ := by + refine klDiv_ne_top (Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ ?_) Integrable.of_finite + rw [empiricalFiniteMeasure_apply hs, sum_eq_zero fun (i : Fin n) _ ↦ Set.indicator_of_notMem + (fun hi ↦ hξ i i.2 (measure_mono_null (Set.singleton_subset_iff.2 hi) hνs)) _, mul_zero] + have h_le : log (1 / δ) + log C ≤ n * (klDiv p ν).toReal := by + rw [← ENNReal.ofReal_toReal hKL, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul (by simp), + ENNReal.ofReal_le_ofReal_iff'] at h + rw [hC, log_pow, hm] + rcases h with h | h + · exact h + · exact h.trans (by positivity) + have h_exp := (exp_le_exp.2 h_le).trans + (exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor hn hξ) + rw [exp_add, exp_log (by positivity), exp_log hC_pos, mul_comm] at h_exp + exact le_of_mul_le_mul_left h_exp hC_pos + +end Ratio + +/-! ### Time-uniform concentration -/ + +variable [MeasurableSpace α] [MeasurableSingletonClass α] {ν : Measure α} {μ : Measure Ω} + [IsProbabilityMeasure μ] + +omit [DecidableEq α] in +/-- **Time-uniform concentration of the empirical distribution**, for observations adapted to a +filtration [JKMDLV20, Proposition 1]: if `ξ t` is `ℱ (t + 1)`-measurable, independent of `ℱ t` +and of law `ν` on a finite type with `m` elements, then for every `δ > 0`, the probability that +`log (1/δ) + (m - 1) log (e (1 + n / (m - 1))) ≤ n KL(p̂_n ‖ ν)` for some `n ≥ 1` is at most `δ`, +where `p̂_n` is the empirical distribution of `ξ 0, …, ξ (n - 1)`. -/ +theorem measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le {ℱ : Filtration ℕ mΩ} + (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hind : ∀ t, Indep (MeasurableSpace.comap (ξ t) inferInstance) (ℱ t) μ) + (hlaw : ∀ t, HasLaw (ξ t) ν μ) {δ : ℝ} (hδ : 0 < δ) : + μ {ω | ∃ n : ℕ, 0 < n ∧ ENNReal.ofReal (log (1 / δ) + ((Fintype.card α : ℝ) - 1) * + log (exp 1 * (1 + n / ((Fintype.card α : ℝ) - 1)))) ≤ + n * klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) ν} ≤ + ENNReal.ofReal δ := by + classical + have := (hlaw 0).isProbabilityMeasure_iff.1 inferInstance + have h_ville := (supermartingale_predictorLikelihoodRatio hξ hind hlaw + (measurable_laplacePredictor hξ) laplacePredictor_nonneg + fun t ω ↦ (sum_laplacePredictor t ω).le).measure_exists_le_le + (fun n ↦ ae_of_all _ (predictorLikelihoodRatio_nonneg laplacePredictor_nonneg n)) + (one_div_pos.2 hδ) + simp only [predictorLikelihoodRatio_zero, integral_const, probReal_univ, smul_eq_mul, mul_one, + one_div_one_div] at h_ville + refine (measure_mono_ae ?_).trans h_ville + -- almost surely, `ν` charges every observation + have h_ae : ∀ᵐ ω ∂μ, ∀ k, ν {ξ k ω} ≠ 0 := by + rw [ae_all_iff] + intro k + have hν : ∀ᵐ a ∂ν, ν {a} ≠ 0 := by + rw [ae_iff, ← Set.biUnion_of_singleton {a | ¬ν {a} ≠ 0}, + measure_biUnion_null_iff (Set.to_countable _)] + exact fun a ha ↦ not_not.1 ha + exact ae_of_ae_map (hlaw k).aemeasurable (by rw [(hlaw k).map_eq]; exact hν) + filter_upwards [h_ae] with ω hω ⟨n, hn, h⟩ + exact ⟨n, one_div_le_predictorLikelihoodRatio hn.ne' (fun k _ ↦ hω k) hδ h⟩ + +omit [DecidableEq α] in +/-- **Time-uniform concentration of the empirical distribution** of independent observations +[JKMDLV20, Proposition 1]: if `ξ 0, ξ 1, …` are independent with law `ν` on a finite type with `m` +elements, then for every `δ > 0`, the probability that +`log (1/δ) + (m - 1) log (e (1 + n / (m - 1))) ≤ n KL(p̂_n ‖ ν)` for some `n ≥ 1` is at most `δ`, +where `p̂_n` is the empirical distribution of `ξ 0, …, ξ (n - 1)`. -/ +theorem _root_.ProbabilityTheory.iIndepFun.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le + (h_indep : iIndepFun ξ μ) (hlaw : ∀ t, HasLaw (ξ t) ν μ) {δ : ℝ} (hδ : 0 < δ) : + μ {ω | ∃ n : ℕ, 0 < n ∧ ENNReal.ofReal (log (1 / δ) + ((Fintype.card α : ℝ) - 1) * + log (exp 1 * (1 + n / ((Fintype.card α : ℝ) - 1)))) ≤ + n * klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) ν} ≤ + ENNReal.ofReal δ := by + have := (hlaw 0).isProbabilityMeasure_iff.1 inferInstance + -- transfer to the coordinates of `ν^{⊗ℕ}` + set P : Measure (ℕ → α) := Measure.infinitePi fun _ ↦ ν + have h_meas : AEMeasurable (fun ω k ↦ ξ k ω) μ := + aemeasurable_pi_iff.2 fun k ↦ (hlaw k).aemeasurable + set E : Set (ℕ → α) := {x | ∃ n : ℕ, 0 < n ∧ ENNReal.ofReal (log (1 / δ) + + ((Fintype.card α : ℝ) - 1) * log (exp 1 * (1 + n / ((Fintype.card α : ℝ) - 1)))) ≤ + n * klDiv (empiricalFiniteMeasure fun k : Fin n ↦ x k : Measure α) ν} + have h_map := Measure.le_map_apply h_meas E + rw [(h_indep.hasLaw_infinitePi hlaw h_meas).map_eq] at h_map + refine h_map.trans ?_ + -- the filtration generated by the coordinates of index `k < n` + let ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → α)) := + { seq n := ⨆ k < n, MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance + mono' _ _ hij := biSup_mono fun _ hk ↦ lt_of_lt_of_le hk hij + le' _ := iSup₂_le fun k _ ↦ (measurable_pi_apply k).comap_le } + have hY : ∀ n, Measurable[ℱ (n + 1)] (fun x : ℕ → α ↦ x n) := fun n ↦ + (comap_measurable _).mono (le_iSup₂ (f := fun k (_ : k < n + 1) ↦ + MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance) n n.lt_succ_self) le_rfl + have h_iIndep : iIndep (fun k ↦ MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance) P := + (iIndepFun_iff_iIndep _ _ _).1 (iIndepFun_infinitePi (X := fun _ ↦ id) fun _ ↦ measurable_id) + have hind : ∀ n, Indep (MeasurableSpace.comap (fun x : ℕ → α ↦ x n) inferInstance) (ℱ n) P := + fun n ↦ by + have h := indep_iSup_of_disjoint (fun k ↦ (measurable_pi_apply k).comap_le) h_iIndep + (S := {n}) (T := Set.Iio n) (by simp) + simpa only [Set.mem_singleton_iff, iSup_iSup_eq_left, Set.mem_Iio] using h + exact LMLExplore.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le + (ξ := fun k (x : ℕ → α) ↦ x k) hY hind + (fun n ↦ (measurePreserving_eval_infinitePi (fun _ ↦ ν) n).hasLaw) hδ + +end LMLExplore diff --git a/LMLExplore/Probability/Martingale/LikelihoodRatio.lean b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean new file mode 100644 index 00000000..a7d23338 --- /dev/null +++ b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean @@ -0,0 +1,277 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.HasLaw +public import Mathlib.Probability.Independence.Integration +public import Mathlib.Probability.Martingale.Basic + +/-! +# Likelihood ratios of sequential predictors + +Let `ξ 0, ξ 1, …` be random variables on a finite type `α`, each independent of the past and with +law `ν`. A *sequential predictor* assigns to every time `t` a vector `q t ω : α → ℝ` that depends +only on the past, here: `ω ↦ q t ω a` is measurable for the σ-algebra `ℱ t` of a filtration with +respect to which `ξ t` is `ℱ (t + 1)`-measurable and independent of `ℱ t`. Its *likelihood ratio* +against `ν` after `n` observations is +`L_n = ∏_{t < n} q t (ξ t) / ν{ξ t}` (`LMLExplore.predictorLikelihoodRatio`). + +If every `q t ω` is a sub-probability vector, `L` is a nonnegative supermartingale with `L_0 = 1`, +and if moreover every `q t ω` is a probability vector and `ν` charges every point, `L` is a +martingale, with mean `1`. Ville's inequality then bounds the probability that `L` ever reaches +`1 / δ` by `δ`. Choosing a universal predictor, whose likelihood is close to the maximum likelihood +of the observations, turns this into time-uniform concentration of the empirical distribution of +the `ξ t`, as for Laplace's rule of succession in `InformationTheory/LaplaceMixture.lean`. + +A mixture of fixed alternatives over a prior is the predictor of its posterior predictive laws; +`SequentialLearning/LikelihoodRatio.lean` treats such mixtures, along a bandit run, through the +exponentials of sums of log-likelihood ratios instead. A predictor needs no prior, and no integral +over the alternatives. + +## Main statements + +* `LMLExplore.supermartingale_predictorLikelihoodRatio`: the likelihood ratio of a + sub-probability predictor is a supermartingale. +* `LMLExplore.martingale_predictorLikelihoodRatio`: the likelihood ratio of a probability + predictor against a law that charges every point is a martingale. +* `LMLExplore.integral_predictorLikelihoodRatio`: it has mean `1`. + +## References + +* [JKMDLV20] A. Jonsson, E. Kaufmann, P. Ménard, O. D. Domingues, E. Leurent and M. Valko, + *Planning in Markov decision processes with gap-dependent sample complexity*, NeurIPS 2020, + Proposition 1 and its proof. +-/ + +public section + +open MeasureTheory ProbabilityTheory Finset + +namespace LMLExplore + +variable {α Ω : Type*} [MeasurableSpace α] {mΩ : MeasurableSpace Ω} + +/-- The **likelihood ratio of a sequential predictor** `q` against a measure `ν`, along the +observations `ξ 0, ξ 1, …`: after `n` observations, `∏_{t < n} q t (ξ t) / ν{ξ t}`. -/ +noncomputable def predictorLikelihoodRatio (ν : Measure α) (q : ℕ → Ω → α → ℝ) + (ξ : ℕ → Ω → α) (n : ℕ) (ω : Ω) : ℝ := + ∏ t ∈ range n, q t ω (ξ t ω) / ν.real {ξ t ω} + +variable {ν : Measure α} {q : ℕ → Ω → α → ℝ} {ξ : ℕ → Ω → α} + +lemma predictorLikelihoodRatio_def (n : ℕ) (ω : Ω) : + predictorLikelihoodRatio ν q ξ n ω = ∏ t ∈ range n, q t ω (ξ t ω) / ν.real {ξ t ω} := + (rfl) + +@[simp] +lemma predictorLikelihoodRatio_zero (ω : Ω) : predictorLikelihoodRatio ν q ξ 0 ω = 1 := by + simp [predictorLikelihoodRatio_def] + +lemma predictorLikelihoodRatio_succ (n : ℕ) (ω : Ω) : + predictorLikelihoodRatio ν q ξ (n + 1) ω = + predictorLikelihoodRatio ν q ξ n ω * (q n ω (ξ n ω) / ν.real {ξ n ω}) := by + simp_rw [predictorLikelihoodRatio_def, prod_range_succ] + +lemma predictorLikelihoodRatio_nonneg (hq0 : ∀ t ω a, 0 ≤ q t ω a) (n : ℕ) (ω : Ω) : + 0 ≤ predictorLikelihoodRatio ν q ξ n ω := + prod_nonneg fun _ _ ↦ div_nonneg (hq0 _ _ _) measureReal_nonneg + +section Filtration + +variable [Fintype α] [MeasurableSingletonClass α] {ℱ : Filtration ℕ mΩ} + +omit [Fintype α] in +/-- The likelihood ratio after `n` observations is `ℱ n`-measurable. -/ +lemma measurable_predictorLikelihoodRatio [Finite α] (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) (n : ℕ) : + Measurable[ℱ n] (predictorLikelihoodRatio ν q ξ n) := by + classical + have := Fintype.ofFinite α + have h_factor : ∀ t < n, Measurable[ℱ n] (fun ω ↦ q t ω (ξ t ω) / ν.real {ξ t ω}) := by + intro t ht + have hξt : Measurable[ℱ n] (ξ t) := (hξ t).mono (ℱ.mono ht) le_rfl + have h_eq : (fun ω ↦ q t ω (ξ t ω) / ν.real {ξ t ω}) = + fun ω ↦ ∑ a, if ξ t ω = a then q t ω a / ν.real {a} else 0 := by + ext ω + simp + rw [h_eq] + exact Finset.measurable_sum _ fun a _ ↦ Measurable.ite (hξt (measurableSet_singleton a)) + (((hq t a).mono (ℱ.mono ht.le) le_rfl).div_const _) measurable_const + rw [show predictorLikelihoodRatio ν q ξ n = + fun ω ↦ ∏ t ∈ range n, q t ω (ξ t ω) / ν.real {ξ t ω} from + funext (predictorLikelihoodRatio_def n)] + exact Finset.measurable_prod _ fun t ht ↦ h_factor t (mem_range.1 ht) + +omit [MeasurableSingletonClass α] in +/-- A sub-probability predictor has coordinates at most `1`, so that every factor +`q t ω a / ν{a}` of its likelihood ratio is at most `∑ b, ν{b}⁻¹`. -/ +private lemma div_measureReal_le_sum_inv (hq0 : ∀ t ω a, 0 ≤ q t ω a) + (hq1 : ∀ t ω, ∑ a, q t ω a ≤ 1) (t : ℕ) (ω : Ω) (a : α) : + q t ω a / ν.real {a} ≤ ∑ b, (ν.real {b})⁻¹ := by + rw [div_eq_mul_inv] + calc q t ω a * (ν.real {a})⁻¹ ≤ 1 * (ν.real {a})⁻¹ := by + gcongr + exact (single_le_sum (fun b _ ↦ hq0 t ω b) (mem_univ _)).trans (hq1 t ω) + _ ≤ ∑ b, (ν.real {b})⁻¹ := by + rw [one_mul] + exact single_le_sum (f := fun b ↦ (ν.real {b})⁻¹) + (fun _ _ ↦ inv_nonneg.2 measureReal_nonneg) (mem_univ _) + +omit [MeasurableSingletonClass α] in +/-- The likelihood ratio of a sub-probability predictor after `n` observations is at most +`(∑ a, ν{a}⁻¹) ^ n`. -/ +private lemma predictorLikelihoodRatio_le (hq0 : ∀ t ω a, 0 ≤ q t ω a) + (hq1 : ∀ t ω, ∑ a, q t ω a ≤ 1) (n : ℕ) (ω : Ω) : + predictorLikelihoodRatio ν q ξ n ω ≤ (∑ a, (ν.real {a})⁻¹) ^ n := by + rw [predictorLikelihoodRatio_def] + exact (prod_le_prod₀ (g := fun _ ↦ ∑ a, (ν.real {a})⁻¹) + (fun t _ ↦ div_nonneg (hq0 _ _ _) measureReal_nonneg) + fun t _ ↦ div_measureReal_le_sum_inv hq0 hq1 t ω (ξ t ω)).trans_eq (by simp) + +/-- The likelihood ratio of a sub-probability predictor is integrable. -/ +lemma integrable_predictorLikelihoodRatio {μ : Measure Ω} [IsFiniteMeasure μ] + (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) + (hq0 : ∀ t ω a, 0 ≤ q t ω a) (hq1 : ∀ t ω, ∑ a, q t ω a ≤ 1) (n : ℕ) : + Integrable (predictorLikelihoodRatio ν q ξ n) μ := + Integrable.of_mem_Icc 0 _ + ((measurable_predictorLikelihoodRatio hξ hq n).mono (ℱ.le n) le_rfl).aemeasurable + (ae_of_all _ fun ω ↦ + ⟨predictorLikelihoodRatio_nonneg hq0 n ω, predictorLikelihoodRatio_le hq0 hq1 n ω⟩) + +variable {μ : Measure Ω} [IsProbabilityMeasure μ] + +/-- The one-step identity behind the (super)martingale property: for `s ∈ ℱ n`, +`∫_s L_{n + 1} = ∫_s L_n ∑ a, ν{a} q n a / ν{a}`, since `ξ n` is independent of `ℱ n` with law +`ν`. -/ +private lemma setIntegral_predictorLikelihoodRatio_succ (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hind : ∀ t, Indep (MeasurableSpace.comap (ξ t) inferInstance) (ℱ t) μ) + (hlaw : ∀ t, HasLaw (ξ t) ν μ) (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) + (hq0 : ∀ t ω a, 0 ≤ q t ω a) (hq1 : ∀ t ω, ∑ a, q t ω a ≤ 1) (n : ℕ) {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫ ω in s, predictorLikelihoodRatio ν q ξ (n + 1) ω ∂μ = + ∫ ω in s, predictorLikelihoodRatio ν q ξ n ω * + ∑ a, ν.real {a} * (q n ω a / ν.real {a}) ∂μ := by + classical + set L := predictorLikelihoodRatio ν q ξ with hL + set C : ℝ := ∑ a, (ν.real {a})⁻¹ + have hC0 : 0 ≤ C := sum_nonneg fun a _ ↦ inv_nonneg.2 measureReal_nonneg + have hξm : Measurable (ξ n) := (hξ n).mono (ℱ.le _) le_rfl + have hsm : MeasurableSet s := ℱ.le n s hs + -- `F a = 1_s L_n q n a / ν{a}`, measurable for `ℱ n`, and `G a = 1_{ξ n = a}` + set F : α → Ω → ℝ := fun a ↦ s.indicator fun ω ↦ L n ω * (q n ω a / ν.real {a}) with hF + set G : α → Ω → ℝ := fun a ↦ (ξ n ⁻¹' {a}).indicator 1 with hG + have hFmeas : ∀ a, Measurable[ℱ n] (F a) := fun a ↦ + ((measurable_predictorLikelihoodRatio hξ hq n).mul ((hq n a).div_const _)).indicator hs + have hGmeas : ∀ a, Measurable[MeasurableSpace.comap (ξ n) inferInstance] (G a) := fun a ↦ + measurable_const.indicator (comap_measurable (ξ n) (measurableSet_singleton a)) + have hFm : ∀ a, Measurable (F a) := fun a ↦ (hFmeas a).mono (ℱ.le n) le_rfl + have hGm : ∀ a, Measurable (G a) := fun a ↦ + measurable_const.indicator (hξm (measurableSet_singleton a)) + have hFint : ∀ a, Integrable (F a) μ := fun a ↦ by + refine Integrable.of_mem_Icc 0 (C ^ n * C) (hFm a).aemeasurable (ae_of_all _ fun ω ↦ ?_) + have h0 : 0 ≤ q n ω a / ν.real {a} := div_nonneg (hq0 n ω a) measureReal_nonneg + simp only [hF, Set.indicator_apply] + split_ifs + · exact ⟨mul_nonneg (predictorLikelihoodRatio_nonneg hq0 n ω) h0, + mul_le_mul (predictorLikelihoodRatio_le hq0 hq1 n ω) + (div_measureReal_le_sum_inv hq0 hq1 n ω a) h0 (pow_nonneg hC0 n)⟩ + · exact ⟨le_rfl, mul_nonneg (pow_nonneg hC0 n) hC0⟩ + -- `1_s L_{n + 1} = ∑ a, F a G a`, by the value of `ξ n` + have h_decomp : s.indicator (L (n + 1)) = fun ω ↦ ∑ a, F a ω * G a ω := by + ext ω + by_cases hω : ω ∈ s + · simp only [hF, hG, Set.indicator_apply, hω, ite_true, Set.mem_preimage, + Set.mem_singleton_iff, Pi.one_apply, mul_ite, mul_one, mul_zero, sum_ite_eq, mem_univ, + hL, predictorLikelihoodRatio_succ] + · simp [hF, Set.indicator_of_notMem hω] + -- independence of `ξ n` from `ℱ n` + have h_indep : ∀ a, ∫ ω, F a ω * G a ω ∂μ = ∫ ω, F a ω * ν.real {a} ∂μ := fun a ↦ by + have hFG : IndepFun (F a) (G a) μ := by + rw [IndepFun_iff_Indep] + exact indep_of_indep_of_le_right (indep_of_indep_of_le_left (hind n).symm + (hFmeas a).comap_le) (hGmeas a).comap_le + rw [hFG.integral_fun_mul_eq_mul_integral (hFm a).aestronglyMeasurable + (hGm a).aestronglyMeasurable, hG, integral_indicator_one (hξm (measurableSet_singleton a)), + ← map_measureReal_apply hξm (measurableSet_singleton a), (hlaw n).map_eq, + integral_mul_const] + have hFG_int : ∀ a, Integrable (fun ω ↦ F a ω * G a ω) μ := fun a ↦ + (hFint a).mul_of_top_left (memLp_top_of_bound (hGm a).aestronglyMeasurable 1 + (ae_of_all _ fun ω ↦ by simp only [hG, Set.indicator]; split_ifs <;> simp)) + calc ∫ ω in s, L (n + 1) ω ∂μ = ∫ ω, ∑ a, F a ω * G a ω ∂μ := by + rw [← integral_indicator hsm, h_decomp] + _ = ∫ ω, ∑ a, F a ω * ν.real {a} ∂μ := by + rw [integral_finsetSum _ fun a _ ↦ hFG_int a, + integral_finsetSum _ fun a _ ↦ (hFint a).mul_const _] + exact sum_congr rfl fun a _ ↦ h_indep a + _ = ∫ ω in s, L n ω * ∑ a, ν.real {a} * (q n ω a / ν.real {a}) ∂μ := by + rw [← integral_indicator hsm] + refine integral_congr_ae (ae_of_all _ fun ω ↦ ?_) + by_cases hω : ω ∈ s + · simp only [hF, Set.indicator_of_mem hω, mul_sum] + exact sum_congr rfl fun a _ ↦ by ring + · simp [hF, Set.indicator_of_notMem hω] + +/-- **The likelihood ratio of a sub-probability predictor is a supermartingale.** Let `ξ t` be +`ℱ (t + 1)`-measurable, independent of `ℱ t` and of law `ν`, and let the predictor `q t` be +`ℱ t`-measurable with `q t ω` nonnegative of total mass at most `1`. Then +`L_n = ∏_{t < n} q t (ξ t) / ν{ξ t}` is a supermartingale for `ℱ`. -/ +theorem supermartingale_predictorLikelihoodRatio (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hind : ∀ t, Indep (MeasurableSpace.comap (ξ t) inferInstance) (ℱ t) μ) + (hlaw : ∀ t, HasLaw (ξ t) ν μ) (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) + (hq0 : ∀ t ω a, 0 ≤ q t ω a) (hq1 : ∀ t ω, ∑ a, q t ω a ≤ 1) : + Supermartingale (predictorLikelihoodRatio ν q ξ) ℱ μ := by + refine supermartingale_of_setIntegral_succ_le + (fun n ↦ (measurable_predictorLikelihoodRatio hξ hq n).stronglyMeasurable) + (integrable_predictorLikelihoodRatio hξ hq hq0 hq1) fun n s hs ↦ ?_ + rw [setIntegral_predictorLikelihoodRatio_succ hξ hind hlaw hq hq0 hq1 n hs] + -- `∑ a, ν{a} q n a / ν{a} ≤ ∑ a, q n a ≤ 1` + refine integral_mono_of_nonneg (ae_of_all _ fun ω ↦ mul_nonneg + (predictorLikelihoodRatio_nonneg hq0 n ω) (sum_nonneg fun a _ ↦ mul_nonneg measureReal_nonneg + (div_nonneg (hq0 n ω a) measureReal_nonneg))) + (integrable_predictorLikelihoodRatio hξ hq hq0 hq1 n).integrableOn (ae_of_all _ fun ω ↦ ?_) + refine mul_le_of_le_one_right (predictorLikelihoodRatio_nonneg hq0 n ω) + ((sum_le_sum fun a _ ↦ ?_).trans (hq1 n ω)) + rcases eq_or_ne (ν.real {a}) 0 with h0 | h0 + · rw [h0, zero_mul] + exact hq0 n ω a + · rw [mul_div_cancel₀ _ h0] + +/-- **The likelihood ratio of a probability predictor is a martingale.** Let `ξ t` be +`ℱ (t + 1)`-measurable, independent of `ℱ t` and of a law `ν` that charges every point, and let +the predictor `q t` be `ℱ t`-measurable with `q t ω` a probability vector. Then +`L_n = ∏_{t < n} q t (ξ t) / ν{ξ t}` is a martingale for `ℱ`. -/ +theorem martingale_predictorLikelihoodRatio (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hind : ∀ t, Indep (MeasurableSpace.comap (ξ t) inferInstance) (ℱ t) μ) + (hlaw : ∀ t, HasLaw (ξ t) ν μ) (hν : ∀ a, ν {a} ≠ 0) + (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) (hq0 : ∀ t ω a, 0 ≤ q t ω a) + (hq1 : ∀ t ω, ∑ a, q t ω a = 1) : + Martingale (predictorLikelihoodRatio ν q ξ) ℱ μ := by + have hq1' : ∀ t ω, ∑ a, q t ω a ≤ 1 := fun t ω ↦ (hq1 t ω).le + have := (hlaw 0).isProbabilityMeasure_iff.1 inferInstance + have hν' : ∀ a, ν.real {a} ≠ 0 := fun a ↦ (measureReal_ne_zero_iff (measure_ne_top _ _)).2 (hν a) + refine martingale_of_setIntegral_eq_succ + (fun n ↦ (measurable_predictorLikelihoodRatio hξ hq n).stronglyMeasurable) + (integrable_predictorLikelihoodRatio hξ hq hq0 hq1') fun n s hs ↦ ?_ + rw [setIntegral_predictorLikelihoodRatio_succ hξ hind hlaw hq hq0 hq1' n hs] + -- `∑ a, ν{a} q n a / ν{a} = ∑ a, q n a = 1` + refine setIntegral_congr_fun (ℱ.le n s hs) fun ω _ ↦ ?_ + simp_rw [mul_div_cancel₀ _ (hν' _), hq1, mul_one] + +/-- **The likelihood ratio of a probability predictor has mean one**, under the hypotheses of +`LMLExplore.martingale_predictorLikelihoodRatio`. -/ +theorem integral_predictorLikelihoodRatio (hξ : ∀ t, Measurable[ℱ (t + 1)] (ξ t)) + (hind : ∀ t, Indep (MeasurableSpace.comap (ξ t) inferInstance) (ℱ t) μ) + (hlaw : ∀ t, HasLaw (ξ t) ν μ) (hν : ∀ a, ν {a} ≠ 0) + (hq : ∀ t a, Measurable[ℱ t] (fun ω ↦ q t ω a)) (hq0 : ∀ t ω a, 0 ≤ q t ω a) + (hq1 : ∀ t ω, ∑ a, q t ω a = 1) (n : ℕ) : + ∫ ω, predictorLikelihoodRatio ν q ξ n ω ∂μ = 1 := by + have h := (martingale_predictorLikelihoodRatio hξ hind hlaw hν hq hq0 hq1).setIntegral_eq + (Nat.zero_le n) MeasurableSet.univ + simpa using h.symm + +end Filtration + +end LMLExplore diff --git a/LMLExplore/SequentialLearning/FiniteActions.lean b/LMLExplore/SequentialLearning/FiniteActions.lean index af76acc9..cf8d8714 100644 --- a/LMLExplore/SequentialLearning/FiniteActions.lean +++ b/LMLExplore/SequentialLearning/FiniteActions.lean @@ -27,6 +27,9 @@ Facts about LML's `pullCount` that hold for any sequence of actions `A : ℕ → round `n`. * `sum_natCast_pullCount`: the pull counts of all arms before `K` add up to `K`, cast to an additive commutative monoid with one. +* `prod_pow_pullCount`, `prod_comp_pullCount`: products over the rounds regrouped arm by arm, the + multiplicative forms of LML's `sum_pullCount_mul` and `sum_comp_pullCount`; in particular + `prod_range_pullCount_action_add_one`: `∏_{s < t} (N_s(A_s) + 1) = ∏_a N_t(a)!`. * `exists_pullCount_eq_zero_of_lt_card`: before round `Fintype.card α`, some arm has not been pulled yet. * `pullCount_card_eq_one_of_forall_pullCount_action_eq_zero`: if each of the first @@ -45,7 +48,7 @@ Facts about LML's `pullCount` that hold for any sequence of actions `A : ℕ → public section open Finset Learning MeasureTheory -open scoped ENNReal +open scoped ENNReal Nat namespace LMLExplore @@ -109,6 +112,31 @@ lemma sum_natCast_pullCount {R : Type*} [AddCommMonoidWithOne R] (ω : Ω) (K : ∑ a, (pullCount A a K ω : R) = K := by rw [← Nat.cast_sum, sum_pullCount] +/-- `∏_a f(a) ^ N_t(a) = ∏_{s < t} f(A_s)`: the multiplicative form of LML's `sum_pullCount_mul`. -/ +lemma prod_pow_pullCount {M : Type*} [CommMonoid M] (f : α → M) (t : ℕ) (ω : Ω) : + ∏ a, f a ^ pullCount A a t ω = ∏ s ∈ range t, f (A s ω) := by + simp_rw [pullCount, ← prod_const] + exact prod_fiberwise' (range t) (A · ω) f + +/-- `∏_{s < t} f(N_s(A_s)) = ∏_a ∏_{j < N_t(a)} f(j)`: the product over the rounds of a function of +the number of previous pulls of the arm played is, arm by arm, its product over `0, …, N_t(a) - 1`. +This is the multiplicative form of LML's `sum_comp_pullCount`. -/ +lemma prod_comp_pullCount {M : Type*} [CommMonoid M] (f : ℕ → M) (t : ℕ) (ω : Ω) : + ∏ s ∈ range t, f (pullCount A (A s ω) s ω) = ∏ a, ∏ j ∈ range (pullCount A a t ω), f j := by + induction t with + | zero => simp + | succ n ih => + have hf : f (pullCount A (A n ω) n ω) = + ∏ a, if A n ω = a then f (pullCount A a n ω) else 1 := by simp + simp_rw [prod_range_succ, ih, hf, ← prod_mul_distrib, pullCount_add_one] + refine prod_congr rfl fun a _ ↦ ?_ + split_ifs <;> simp [prod_range_succ] + +/-- `∏_{s < t} (N_s(A_s) + 1) = ∏_a N_t(a)!`. -/ +lemma prod_range_pullCount_action_add_one (t : ℕ) (ω : Ω) : + ∏ s ∈ range t, (pullCount A (A s ω) s ω + 1) = ∏ a, (pullCount A a t ω)! := by + simp_rw [prod_comp_pullCount (fun j ↦ j + 1), prod_range_add_one_eq_factorial] + /-- Before round `Fintype.card α`, some arm has not been pulled yet. -/ lemma exists_pullCount_eq_zero_of_lt_card (hn : n < Fintype.card α) : ∃ b, pullCount A b n ω = 0 := by From 2fe2241685b710ebea0b8fe59819f3fc8726b81b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 09:13:47 +0100 Subject: [PATCH 2/5] chore: name LMLExplore contributors in the headers of the new files Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- LMLExplore/Data/Nat/Choose/Bounds.lean | 4 ++-- LMLExplore/InformationTheory/LaplaceMixture.lean | 4 ++-- LMLExplore/Probability/Martingale/LikelihoodRatio.lean | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/LMLExplore/Data/Nat/Choose/Bounds.lean b/LMLExplore/Data/Nat/Choose/Bounds.lean index 708182f6..4afc45db 100644 --- a/LMLExplore/Data/Nat/Choose/Bounds.lean +++ b/LMLExplore/Data/Nat/Choose/Bounds.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 LMLExplore contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne +Authors: LMLExplore contributors -/ module diff --git a/LMLExplore/InformationTheory/LaplaceMixture.lean b/LMLExplore/InformationTheory/LaplaceMixture.lean index 7bfcbda3..591f4f84 100644 --- a/LMLExplore/InformationTheory/LaplaceMixture.lean +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 LMLExplore contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne +Authors: LMLExplore contributors -/ module diff --git a/LMLExplore/Probability/Martingale/LikelihoodRatio.lean b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean index a7d23338..1cc32ab9 100644 --- a/LMLExplore/Probability/Martingale/LikelihoodRatio.lean +++ b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 LMLExplore contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne +Authors: LMLExplore contributors -/ module From a3c01c1c37bec0d9bf1a261cb0b294e95a3b4ca4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 10:38:02 +0100 Subject: [PATCH 3/5] refactor: share the strict-past filtration and factor the Laplace mixture bounds Add Filtration.naturalLT with measurable_naturalLT and indep_naturalLT, used by LaplaceMixture, SubGaussian and RateFunction instead of three inline copies. Factor empiricalFiniteMeasure_absolutelyContinuous, and move the multinomial and ascending-factorial bounds to Data/Nat/Choose/Bounds.lean as Nat.prod_div_pow_le_prod_factorial_div and Nat.ascFactorial_div_factorial_le. Rename measureReal_empiricalFiniteMeasure_singleton_eq_pullCount to ..._eq_pullCount_div and credit the source formalization in LikelihoodRatio.lean. Co-Authored-By: Claude Code --- LMLExplore/Data/Nat/Choose/Bounds.lean | 52 ++++++++++++-- .../InformationTheory/LaplaceMixture.lean | 70 +++++++------------ .../Martingale/LikelihoodRatio.lean | 6 ++ .../Probability/Martingale/RateFunction.lean | 17 ++--- .../Probability/Martingale/SubGaussian.lean | 17 ++--- .../Probability/Process/Filtration.lean | 59 +++++++++++++++- 6 files changed, 145 insertions(+), 76 deletions(-) diff --git a/LMLExplore/Data/Nat/Choose/Bounds.lean b/LMLExplore/Data/Nat/Choose/Bounds.lean index 4afc45db..5783e245 100644 --- a/LMLExplore/Data/Nat/Choose/Bounds.lean +++ b/LMLExplore/Data/Nat/Choose/Bounds.lean @@ -12,17 +12,21 @@ public import Mathlib.Data.Nat.Choose.Multinomial /-! # Bounds on binomial and multinomial coefficients -Two classical upper bounds on the number of words with prescribed letter counts. +Two classical upper bounds on the number of words with prescribed letter counts, and their +consequences for ascending factorials and maximum likelihoods. * `Nat.choose_le_exp_one_mul_div_pow`: `n.choose k ≤ (e n / k) ^ k`, from Mathlib's `Nat.choose_le_pow_div` and `k ^ k / k! ≤ e ^ k`. +* `Nat.ascFactorial_div_factorial_le`: `(m + 1)^{(n)} / n! = binom(m + n, m) ≤ (e (1 + n / m)) ^ m`, + where `(m + 1)^{(n)} = (m + 1) (m + 2) ⋯ (m + n)` is the ascending factorial. * `Nat.multinomial_mul_prod_pow_le_one`: for a probability vector `p` on `s`, the term `multinomial s f * ∏ i ∈ s, p i ^ f i` of the multinomial expansion of `(∑ i ∈ s, p i) ^ n` is at - most `1`. It is the probability of the counts `f` in `n` independent draws from `p`. With - `p i = f i / n`, it bounds the maximum likelihood `∏ i ∈ s, (f i / n) ^ f i` of a word with counts - `f` by `∏ i ∈ s, (f i)! / n!`. + most `1`. It is the probability of the counts `f` in `n` independent draws from `p`. +* `Nat.prod_div_pow_le_prod_factorial_div`: with `p i = f i / n`, the previous bound bounds the + maximum likelihood `∏ i ∈ s, (f i / n) ^ f i` of a word with counts `f` by + `∏ i ∈ s, (f i)! / n!`. -Both bounds control the likelihood ratios of universal (mixture) predictors against the maximum +These bounds control the likelihood ratios of universal (mixture) predictors against the maximum likelihood, as in the analysis of Laplace's rule of succession. -/ @@ -50,6 +54,19 @@ theorem choose_le_exp_one_mul_div_pow (n k : ℕ) : _ ≤ ((n : ℝ) / k) ^ k * exp 1 ^ k := by gcongr _ = (exp 1 * n / k) ^ k := by rw [← mul_pow, mul_comm, mul_div_assoc] +/-- **Ascending factorials over factorials**: `(m + 1)^{(n)} / n! ≤ (e (1 + n / m)) ^ m`, where +`(m + 1)^{(n)} = (m + 1) (m + 2) ⋯ (m + n)`. The left-hand side is `binom(m + n, m)`. -/ +theorem ascFactorial_div_factorial_le (m n : ℕ) : + ((m + 1).ascFactorial n : ℝ) / n ! ≤ (exp 1 * (1 + n / m)) ^ m := by + rw [ascFactorial_eq_factorial_mul_choose, cast_mul, + mul_div_cancel_left₀ _ (cast_ne_zero.2 n.factorial_ne_zero), ← choose_symm_add] + refine (choose_le_exp_one_mul_div_pow _ _).trans_eq ?_ + rcases eq_zero_or_pos m with rfl | hm + · simp + · have : (0 : ℝ) < m := by exact_mod_cast hm + push_cast + field_simp + /-- **A multinomial probability is at most one**: for `p` nonnegative on `s` with `∑ i ∈ s, p i = 1`, `multinomial s f * ∏ i ∈ s, p i ^ f i ≤ 1`. This term of the multinomial expansion of `(∑ i ∈ s, p i) ^ (∑ i ∈ s, f i)` is the probability of the counts `f` under @@ -75,4 +92,29 @@ theorem multinomial_mul_prod_pow_le_one {R ι : Type*} [CommSemiring R] [Partial (fun k _ ↦ mul_nonneg (Nat.cast_nonneg _) (prod_nonneg fun i hi ↦ pow_nonneg (hp0 i hi) _)) hg_mem +/-- **The maximum likelihood of a word is at most its multinomial probability bound**: for counts +`f` on `s` with sum `n`, `∏ i ∈ s, (f i / n) ^ f i ≤ ∏ i ∈ s, (f i)! / n!`. -/ +theorem prod_div_pow_le_prod_factorial_div {R ι : Type*} [Field R] [LinearOrder R] + [IsStrictOrderedRing R] (s : Finset ι) (f : ι → ℕ) : + ∏ i ∈ s, ((f i : R) / ∑ j ∈ s, f j) ^ f i ≤ + (∏ i ∈ s, ((f i)! : R)) / (∑ i ∈ s, f i)! := by + rcases eq_or_ne (∑ i ∈ s, f i) 0 with h0 | h0 + · have hf : ∀ i ∈ s, f i = 0 := sum_eq_zero_iff.1 h0 + rw [h0, prod_eq_one fun i hi ↦ by rw [hf i hi, pow_zero], + prod_eq_one fun i hi ↦ by rw [hf i hi, factorial_zero, cast_one], factorial_zero, cast_one, + div_one] + have hn : (0 : R) < ∑ j ∈ s, f j := by exact_mod_cast pos_of_ne_zero h0 + have h_le := multinomial_mul_prod_pow_le_one s f (p := fun i ↦ (f i : R) / ∑ j ∈ s, f j) + (fun i _ ↦ by positivity) (by + simp_rw [div_eq_mul_inv] + rw [← Finset.sum_mul, ← cast_sum, mul_inv_cancel₀ hn.ne']) + have h_spec : (∏ i ∈ s, ((f i)! : R)) * multinomial s f = (∑ i ∈ s, f i)! := by + exact_mod_cast multinomial_spec s f + have h_fact : (0 : R) ≤ ∏ i ∈ s, ((f i)! : R) := prod_nonneg fun _ _ ↦ cast_nonneg _ + rw [le_div_iff₀ (by positivity), ← h_spec] + calc (∏ i ∈ s, ((f i : R) / ∑ j ∈ s, f j) ^ f i) * ((∏ i ∈ s, ((f i)! : R)) * multinomial s f) + = (∏ i ∈ s, ((f i)! : R)) * + (multinomial s f * ∏ i ∈ s, ((f i : R) / ∑ j ∈ s, f j) ^ f i) := by ring + _ ≤ ∏ i ∈ s, ((f i)! : R) := mul_le_of_le_one_right h_fact h_le + end Nat diff --git a/LMLExplore/InformationTheory/LaplaceMixture.lean b/LMLExplore/InformationTheory/LaplaceMixture.lean index 591f4f84..bf25250c 100644 --- a/LMLExplore/InformationTheory/LaplaceMixture.lean +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -10,6 +10,7 @@ public import Mathlib.Probability.Independence.InfinitePi public import LMLExplore.Data.Nat.Choose.Bounds public import LMLExplore.Probability.Martingale.LikelihoodRatio public import LMLExplore.Probability.Martingale.Ville +public import LMLExplore.Probability.Process.Filtration public import LMLExplore.SequentialLearning.FiniteActions public import TauCeti.MeasureTheory.Measure.Decomposition.Lebesgue public import TauCeti.Probability.Process.EmpiricalMeasure @@ -31,9 +32,9 @@ the probability that it ever reaches `1 / δ`. The likelihood of the rule of suc `∏_{t < n} q_t(ξ t) = ∏ₐ N_n(a)! / (m (m + 1) ⋯ (m + n - 1))` (`LMLExplore.prod_range_laplacePredictor`), the mixture of the likelihoods `∏_{t < n} p(ξ t)` over the uniform law of the probability vector `p`. It is within the factor -`binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` of the maximum likelihood -`∏ₐ (N_n(a) / n)^{N_n(a)} = exp (n KL(p̂_n ‖ ν)) ∏_{t < n} ν{ξ t}`, by the multinomial bound -`Nat.multinomial_mul_prod_pow_le_one` +`binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` (`Nat.ascFactorial_div_factorial_le`) +of the maximum likelihood `∏ₐ (N_n(a) / n)^{N_n(a)} = exp (n KL(p̂_n ‖ ν)) ∏_{t < n} ν{ξ t}`, by the +multinomial bound `Nat.prod_div_pow_le_prod_factorial_div` (`LMLExplore.exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor`). ## Main statements @@ -129,7 +130,7 @@ variable [MeasurableSpace α] [MeasurableSingletonClass α] omit [Fintype α] in /-- The mass of a point under the empirical distribution of `ξ 0, …, ξ (n - 1)` is its frequency `N_n(a) / n`. -/ -lemma measureReal_empiricalFiniteMeasure_singleton_eq_pullCount (n : ℕ) (ω : Ω) (a : α) : +lemma measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div (n : ℕ) (ω : Ω) (a : α) : (empiricalFiniteMeasure (fun k : Fin n ↦ ξ k ω) : Measure α).real {a} = pullCount ξ a n ω / n := by have h_sum : ∑ k : Fin n, ({a} : Set α).indicator (1 : α → ℝ≥0∞) (ξ k ω) = pullCount ξ a n ω := by @@ -141,6 +142,15 @@ lemma measureReal_empiricalFiniteMeasure_singleton_eq_pullCount (n : ℕ) (ω : ENNReal.toReal_mul, ENNReal.toReal_inv, Fintype.card_fin, ENNReal.toReal_natCast, ENNReal.toReal_natCast, inv_mul_eq_div] +omit [Fintype α] [DecidableEq α] [MeasurableSingletonClass α] in +/-- The empirical distribution of a finite family `x` of points charged by `ν` is absolutely +continuous with respect to `ν`. -/ +lemma empiricalFiniteMeasure_absolutelyContinuous {κ : Type*} [Fintype κ] {ν : Measure α} + {x : κ → α} (hx : ∀ i, ν {x i} ≠ 0) : (empiricalFiniteMeasure x : Measure α) ≪ ν := + Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ by + rw [empiricalFiniteMeasure_apply hs, sum_eq_zero fun i _ ↦ Set.indicator_of_notMem + (fun hi ↦ hx i (measure_mono_null (Set.singleton_subset_iff.2 hi) hνs)) _, mul_zero] + omit [Fintype α] [DecidableEq α] in /-- **The divergence of an empirical distribution**: for a nonempty finite family `x` of points charged by a probability measure `ν`, with empirical distribution `p̂`, @@ -152,9 +162,7 @@ theorem exp_mul_toReal_klDiv_empiricalFiniteMeasure {κ : Type*} [Fintype κ] [N set p : Measure α := (empiricalFiniteMeasure x : Measure α) have hκ : (0 : ℝ) < Fintype.card κ := by exact_mod_cast Fintype.card_pos -- the empirical distribution only charges the points `x i` - have hac : p ≪ ν := Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ by - rw [empiricalFiniteMeasure_apply hs, sum_eq_zero fun i _ ↦ Set.indicator_of_notMem - (fun hi ↦ hx i (measure_mono_null (Set.singleton_subset_iff.2 hi) hνs)) _, mul_zero] + have hac : p ≪ ν := empiricalFiniteMeasure_absolutelyContinuous hx have hp_pos : ∀ i, 0 < p.real {x i} := fun i ↦ by refine ENNReal.toReal_pos ?_ (measure_ne_top _ _) rw [empiricalFiniteMeasure_apply (measurableSet_singleton _)] @@ -195,7 +203,6 @@ theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor set m := Fintype.card α with hm_def have hm : 1 ≤ m := Fintype.card_pos set N : α → ℕ := fun a ↦ pullCount ξ a n ω with hN - have hnR : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn have hN_sum : ∑ a, N a = n := sum_pullCount -- `P = ∏_{t < n} ν{ξ t} > 0` set P := ∏ t ∈ range n, ν.real {ξ t ω} @@ -209,7 +216,7 @@ theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor rw [Fintype.card_fin] at h rw [h, Fin.prod_univ_eq_prod_range (fun t ↦ (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α).real {ξ t ω} / ν.real {ξ t ω}) n, prod_div_distrib] - simp_rw [measureReal_empiricalFiniteMeasure_singleton_eq_pullCount] + simp_rw [measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div] rw [← prod_pow_pullCount (A := ξ) (fun a ↦ (pullCount ξ a n ω : ℝ) / n) n ω] -- the likelihood of the rule of succession: `L_n P = ∏ₐ N a ! / m^{(n)}` have h_lap : predictorLikelihoodRatio ν (laplacePredictor ξ) ξ n ω = @@ -217,27 +224,11 @@ theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor rw [predictorLikelihoodRatio_def, prod_div_distrib, prod_range_laplacePredictor] -- the multinomial bound: `∏ₐ (N a / n) ^ N a ≤ ∏ₐ N a ! / n!` have h_mult : ∏ a, ((N a : ℝ) / n) ^ N a ≤ (∏ a, ((N a)! : ℝ)) / n ! := by - have h1 := Nat.multinomial_mul_prod_pow_le_one univ N (p := fun a ↦ (N a : ℝ) / n) - (fun a _ ↦ by positivity) (by rw [← sum_div, ← Nat.cast_sum, hN_sum, div_self hnR.ne']) - have h2 : (∏ a, ((N a)! : ℝ)) * (Nat.multinomial univ N : ℝ) = n ! := by - exact_mod_cast hN_sum ▸ Nat.multinomial_spec univ N - have h3 : (0 : ℝ) < Nat.multinomial univ N := by exact_mod_cast Nat.multinomial_pos _ _ - rw [le_div_iff₀ (by positivity), ← h2] - nlinarith [prod_nonneg fun a (_ : a ∈ univ) ↦ (Nat.cast_nonneg (N a)! : (0 : ℝ) ≤ _), - mul_le_mul_of_nonneg_left h1 (prod_nonneg fun a (_ : a ∈ univ) ↦ - (Nat.cast_nonneg (N a)! : (0 : ℝ) ≤ _))] + simpa only [hN_sum] using Nat.prod_div_pow_le_prod_factorial_div (R := ℝ) univ N -- the binomial bound: `m^{(n)} / n! = binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` have h_choose : (m.ascFactorial n : ℝ) / n ! ≤ (exp 1 * (1 + n / (m - 1 : ℕ))) ^ (m - 1) := by - rw [Nat.ascFactorial_eq_factorial_mul_choose', Nat.cast_mul, mul_div_cancel_left₀ _ - (by positivity), show m + n - 1 = (m - 1) + n by omega, ← Nat.choose_symm_add] - refine (Nat.choose_le_exp_one_mul_div_pow _ _).trans_eq ?_ - rcases Nat.eq_zero_or_pos (m - 1) with h0 | h0 - · simp [h0] - · have : (0 : ℝ) < (m - 1 : ℕ) := by exact_mod_cast h0 - congr 1 - push_cast - field_simp + simpa only [Nat.sub_add_cancel hm] using Nat.ascFactorial_div_factorial_le (m - 1) n rw [h_max, h_lap] have h_asc : (0 : ℝ) < m.ascFactorial n := by obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le hm @@ -263,10 +254,8 @@ private lemma one_div_le_predictorLikelihoodRatio [IsProbabilityMeasure ν] {n : set C := (exp 1 * (1 + n / (Fintype.card α - 1 : ℕ))) ^ (Fintype.card α - 1) with hC have hC_pos : 0 < C := by positivity -- the divergence is finite, since `p̂_n` is absolutely continuous with respect to `ν` - have hKL : klDiv p ν ≠ ∞ := by - refine klDiv_ne_top (Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ ?_) Integrable.of_finite - rw [empiricalFiniteMeasure_apply hs, sum_eq_zero fun (i : Fin n) _ ↦ Set.indicator_of_notMem - (fun hi ↦ hξ i i.2 (measure_mono_null (Set.singleton_subset_iff.2 hi) hνs)) _, mul_zero] + have hKL : klDiv p ν ≠ ∞ := + klDiv_ne_top (empiricalFiniteMeasure_absolutelyContinuous fun i ↦ hξ i i.2) Integrable.of_finite have h_le : log (1 / δ) + log C ≤ n * (klDiv p ν).toReal := by rw [← ENNReal.ofReal_toReal hKL, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul (by simp), ENNReal.ofReal_le_ofReal_iff'] at h @@ -346,22 +335,11 @@ theorem _root_.ProbabilityTheory.iIndepFun.measure_exists_le_mul_klDiv_empirical rw [(h_indep.hasLaw_infinitePi hlaw h_meas).map_eq] at h_map refine h_map.trans ?_ -- the filtration generated by the coordinates of index `k < n` - let ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → α)) := - { seq n := ⨆ k < n, MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance - mono' _ _ hij := biSup_mono fun _ hk ↦ lt_of_lt_of_le hk hij - le' _ := iSup₂_le fun k _ ↦ (measurable_pi_apply k).comap_le } - have hY : ∀ n, Measurable[ℱ (n + 1)] (fun x : ℕ → α ↦ x n) := fun n ↦ - (comap_measurable _).mono (le_iSup₂ (f := fun k (_ : k < n + 1) ↦ - MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance) n n.lt_succ_self) le_rfl - have h_iIndep : iIndep (fun k ↦ MeasurableSpace.comap (fun x : ℕ → α ↦ x k) inferInstance) P := - (iIndepFun_iff_iIndep _ _ _).1 (iIndepFun_infinitePi (X := fun _ ↦ id) fun _ ↦ measurable_id) - have hind : ∀ n, Indep (MeasurableSpace.comap (fun x : ℕ → α ↦ x n) inferInstance) (ℱ n) P := - fun n ↦ by - have h := indep_iSup_of_disjoint (fun k ↦ (measurable_pi_apply k).comap_le) h_iIndep - (S := {n}) (T := Set.Iio n) (by simp) - simpa only [Set.mem_singleton_iff, iSup_iSup_eq_left, Set.mem_Iio] using h exact LMLExplore.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le - (ξ := fun k (x : ℕ → α) ↦ x k) hY hind + (ξ := fun k (x : ℕ → α) ↦ x k) (ℱ := Filtration.naturalLT _ measurable_pi_apply) + (fun n ↦ Filtration.measurable_naturalLT measurable_pi_apply n.lt_succ_self) + (Filtration.indep_naturalLT measurable_pi_apply + (iIndepFun_infinitePi (X := fun _ ↦ id) fun _ ↦ measurable_id)) (fun n ↦ (measurePreserving_eval_infinitePi (fun _ ↦ ν) n).hasLaw) hδ end LMLExplore diff --git a/LMLExplore/Probability/Martingale/LikelihoodRatio.lean b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean index 1cc32ab9..4ad7c7e8 100644 --- a/LMLExplore/Probability/Martingale/LikelihoodRatio.lean +++ b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean @@ -39,6 +39,12 @@ over the alternatives. predictor against a law that charges every point is a martingale. * `LMLExplore.integral_predictorLikelihoodRatio`: it has mean `1`. +## Implementation notes + +The supermartingale property is adapted, and generalised from Laplace's rule of succession to +every predictor, from `InformationTheory/KLTimeUniform.lean` of the formalization +RemyDegenne/Essakine2026Tight (commit 38bbd16f, directory `ForLMLExplore/`). + ## References * [JKMDLV20] A. Jonsson, E. Kaufmann, P. Ménard, O. D. Domingues, E. Leurent and M. Valko, diff --git a/LMLExplore/Probability/Martingale/RateFunction.lean b/LMLExplore/Probability/Martingale/RateFunction.lean index 7a15d252..ad512831 100644 --- a/LMLExplore/Probability/Martingale/RateFunction.lean +++ b/LMLExplore/Probability/Martingale/RateFunction.lean @@ -7,6 +7,7 @@ module public import LMLExplore.Probability.Martingale.MGFBound public import LMLExplore.Probability.Moments.RateFunction +public import LMLExplore.Probability.Process.Filtration /-! # Self-normalized deviations of selected variables, measured by the rate function @@ -349,18 +350,10 @@ private lemma exists_filtration_hasCondMGFBound (h_indep : iIndepFun Z P) ∃ ℱ : Filtration ℕ mΩ, (∀ n, Measurable[ℱ (n + 1)] (Z n)) ∧ ∀ n, HasCondMGFBound (ℱ n) (ℱ.le n) (Z n) (cgf Y Q) (Λ ∩ integrableExpSet Y Q) P := by -- the filtration of the past variables, of which `Z n` is independent - let ℱ : Filtration ℕ mΩ := - { seq n := ⨆ i ∈ Set.Iio n, MeasurableSpace.comap (Z i) inferInstance - mono' _ _ hnm := biSup_mono fun i hi ↦ lt_of_lt_of_le hi hnm - le' _ := iSup₂_le fun i _ ↦ (hZm i).comap_le } - refine ⟨ℱ, fun n ↦ ?_, fun n ↦ ?_⟩ - · exact Measurable.of_comap_le (le_iSup₂ (f := fun i (_ : i ∈ Set.Iio (n + 1)) ↦ - MeasurableSpace.comap (Z i) inferInstance) n (Nat.lt_succ_self n)) - · refine HasMGFBound.hasCondMGFBound_of_indep - (mgfDominatedOn_iff_hasMGFBound.1 (hZ n)) (hZm n) ?_ - have h := indep_iSup_of_disjoint (fun i ↦ (hZm i).comap_le) h_indep - (S := {n}) (T := Set.Iio n) (by simp) - simpa only [Set.mem_singleton_iff, iSup_iSup_eq_left] using h + refine ⟨Filtration.naturalLT Z hZm, fun n ↦ Filtration.measurable_naturalLT hZm n.lt_succ_self, + fun n ↦ ?_⟩ + exact HasMGFBound.hasCondMGFBound_of_indep (mgfDominatedOn_iff_hasMGFBound.1 (hZ n)) (hZm n) + (Filtration.indep_naturalLT hZm h_indep n) /-- **Time-uniform Chernoff bound for sums of independent variables, with the rate function.** Let `Z 0, Z 1, …` be independent, each dominated on `Set.Ici 0`, in moment generating function, by the diff --git a/LMLExplore/Probability/Martingale/SubGaussian.lean b/LMLExplore/Probability/Martingale/SubGaussian.lean index 0aad1f37..3e4e4a67 100644 --- a/LMLExplore/Probability/Martingale/SubGaussian.lean +++ b/LMLExplore/Probability/Martingale/SubGaussian.lean @@ -9,6 +9,7 @@ public import LMLExplore.Analysis.SpecialFunctions.Exp public import LMLExplore.Probability.Martingale.MGFBound public import LMLExplore.Probability.Martingale.Ville public import LMLExplore.Probability.Moments.SubGaussian.Basic +public import LMLExplore.Probability.Process.Filtration public import Mathlib.Analysis.SpecialFunctions.Log.PosLog public import Mathlib.Probability.Independence.InfinitePi @@ -287,24 +288,18 @@ theorem measure_exists_sum_div_add_sqrt_add_le_zero_le_of_iIndepFun [IsProbabili set P := Measure.infinitePi fun n ↦ μ.map (X n) -- the filtration generated by the coordinates of index `k < n` let ℱ' : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → ℝ)) := - { seq n := ⨆ k < n, MeasurableSpace.comap (fun x : ℕ → ℝ ↦ x k) inferInstance - mono' _ _ hij := biSup_mono fun _ hk ↦ lt_of_lt_of_le hk hij - le' _ := iSup₂_le fun k _ ↦ (measurable_pi_apply k).comap_le } + Filtration.naturalLT (fun k (x : ℕ → ℝ) ↦ x k) measurable_pi_apply have hY : ∀ n, Measurable[ℱ' (n + 1)] (fun x : ℕ → ℝ ↦ x n) := fun n ↦ - (comap_measurable _).mono (le_iSup₂ (f := fun k (_ : k < n + 1) ↦ - MeasurableSpace.comap (fun x : ℕ → ℝ ↦ x k) inferInstance) n n.lt_succ_self) le_rfl - have h_iIndep : iIndep (fun k ↦ MeasurableSpace.comap (fun x : ℕ → ℝ ↦ x k) inferInstance) P := - (iIndepFun_iff_iIndep _ _ _).1 (iIndepFun_infinitePi (X := fun _ ↦ id) fun _ ↦ measurable_id) + Filtration.measurable_naturalLT measurable_pi_apply n.lt_succ_self have hsubG : ∀ n, HasCondSubgaussianMGF (ℱ' n) (ℱ'.le n) (fun x : ℕ → ℝ ↦ x n) c P := by intro n have h_sub : HasSubgaussianMGF (fun x : ℕ → ℝ ↦ x n) c P := by rw [← HasSubgaussianMGF.id_map_iff (measurable_pi_apply n).aemeasurable, Measure.infinitePi_map_eval] exact (HasSubgaussianMGF.id_map_iff (hX_meas n)).2 (hX n) - have h_ind := indep_iSup_of_disjoint (fun k ↦ (measurable_pi_apply k).comap_le) h_iIndep - (S := {n}) (T := Set.Iio n) (by simp) - simp only [Set.mem_singleton_iff, iSup_iSup_eq_left, Set.mem_Iio] at h_ind - exact h_sub.hasCondSubgaussianMGF_of_indep (measurable_pi_apply n) h_ind + exact h_sub.hasCondSubgaussianMGF_of_indep (measurable_pi_apply n) + (Filtration.indep_naturalLT measurable_pi_apply (iIndepFun_infinitePi (X := fun _ ↦ id) + fun _ ↦ measurable_id) n) set E : Set (ℕ → ℝ) := {x | ∃ s : ℕ, 0 < s ∧ (∑ k ∈ range s, x k) / s + √(4 * c / s * log⁺ (1 / (s * δ))) + Δ ≤ 0} have h_map := Measure.le_map_apply (aemeasurable_pi_iff.2 hX_meas) E diff --git a/LMLExplore/Probability/Process/Filtration.lean b/LMLExplore/Probability/Process/Filtration.lean index 2564d34a..0895fd23 100644 --- a/LMLExplore/Probability/Process/Filtration.lean +++ b/LMLExplore/Probability/Process/Filtration.lean @@ -5,27 +5,48 @@ Authors: Rémy Degenne -/ module +public import Mathlib.Probability.Independence.Basic public import TauCeti.Probability.Process.PathLaw.Filtration /-! -# Measurability of coordinates for the natural filtration of a product +# Natural filtrations of products and of the strict past of a process Mathlib's natural filtration `MeasureTheory.Filtration.piLE` of a product `Π i, X i` contains at time `i` the measurable sets that depend only on the coordinates `≤ i`. Tau Ceti's `MeasureTheory.Filtration.adapted_piLE` states that the coordinate `x ↦ x i` is measurable at time `i`. This file records that every earlier coordinate `x ↦ x j`, `j ≤ i`, is measurable at time `i`. +It also defines the filtration `MeasureTheory.Filtration.naturalLT` of the strict past of a +measurable process `u`: at time `i`, the σ-algebra generated by the `u j` with `j < i`. The +variable `u i` is measurable at every later time, and if the `u i` are independent, `u i` is +independent of its strict past. For the coordinates of a product measure, this is the filtration +with respect to which each coordinate is drawn independently of the previous ones. + +## Main definitions + +* `MeasureTheory.Filtration.naturalLT`: the filtration of the strict past of a measurable process. + ## Main statements * `MeasureTheory.Filtration.measurable_eval_piLE`: for `j ≤ i`, the coordinate `x ↦ x j` is measurable for `piLE i`. +* `MeasureTheory.Filtration.measurable_naturalLT`: for `j < i`, `u j` is measurable for + `naturalLT u hu i`. +* `MeasureTheory.Filtration.indep_naturalLT`: if the `u i` are independent, `u i` is independent + of `naturalLT u hu i`. -/ public section +open ProbabilityTheory + namespace MeasureTheory.Filtration -variable {ι : Type*} [Preorder ι] {X : ι → Type*} [∀ i, MeasurableSpace (X i)] +variable {ι : Type*} [Preorder ι] + +section piLE + +variable {X : ι → Type*} [∀ i, MeasurableSpace (X i)] /-- For `j ≤ i`, the coordinate `x ↦ x j` of a product `Π i, X i` is measurable for its natural filtration `piLE` at time `i`. -/ @@ -33,4 +54,38 @@ theorem measurable_eval_piLE {i j : ι} (hji : j ≤ i) : Measurable[piLE (X := X) i] fun x : Π i, X i ↦ x j := (adapted_piLE (X := X) j).mono (piLE.mono hji) le_rfl +end piLE + +section naturalLT + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {β : ι → Type*} [∀ i, MeasurableSpace (β i)] + {u : (i : ι) → Ω → β i} + +/-- The filtration of the **strict past** of a measurable process `u`: at time `i`, the σ-algebra +generated by the variables `u j` with `j < i`. -/ +def naturalLT (u : (i : ι) → Ω → β i) (hu : ∀ i, Measurable (u i)) : Filtration ι mΩ where + seq i := ⨆ j < i, MeasurableSpace.comap (u j) inferInstance + mono' _ _ hii' := biSup_mono fun _ hj ↦ lt_of_lt_of_le hj hii' + le' _ := iSup₂_le fun j _ ↦ (hu j).comap_le + +lemma naturalLT_apply (hu : ∀ i, Measurable (u i)) (i : ι) : + naturalLT u hu i = ⨆ j < i, MeasurableSpace.comap (u j) inferInstance := + (rfl) + +/-- For `j < i`, the variable `u j` is measurable for the strict past `naturalLT u hu i`. -/ +theorem measurable_naturalLT (hu : ∀ i, Measurable (u i)) {i j : ι} (hji : j < i) : + Measurable[naturalLT u hu i] (u j) := + Measurable.of_comap_le (le_iSup₂ (f := fun k (_ : k < i) ↦ + MeasurableSpace.comap (u k) inferInstance) j hji) + +/-- If the variables `u i` are independent, each `u i` is independent of its strict past +`naturalLT u hu i`. -/ +theorem indep_naturalLT (hu : ∀ i, Measurable (u i)) {μ : Measure Ω} (h_indep : iIndepFun u μ) + (i : ι) : Indep (MeasurableSpace.comap (u i) inferInstance) (naturalLT u hu i) μ := by + have h := indep_iSup_of_disjoint (fun j ↦ (hu j).comap_le) + ((iIndepFun_iff_iIndep _ _ _).1 h_indep) (S := {i}) (T := Set.Iio i) (by simp) + simpa only [Set.mem_singleton_iff, iSup_iSup_eq_left, Set.mem_Iio, naturalLT_apply] using h + +end naturalLT + end MeasureTheory.Filtration From 6b4cd1b02febaa8b777add6142f4a67c093a186a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 23:37:23 +0100 Subject: [PATCH 4/5] refactor: reuse the method-of-types identity for the maximum likelihood Identify the counts of the observations with their type counts (typeCount_eq_pullCount) and derive the maximum-likelihood identity from prod_measureReal_pow_typeCount_eq_mul_exp and toReal_klDiv_eq_sum_mul_log_div, dropping the parallel exp_mul_toReal_klDiv_empiricalFiniteMeasure and measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div. Co-Authored-By: Claude Code --- .../InformationTheory/LaplaceMixture.lean | 89 ++++++------------- 1 file changed, 25 insertions(+), 64 deletions(-) diff --git a/LMLExplore/InformationTheory/LaplaceMixture.lean b/LMLExplore/InformationTheory/LaplaceMixture.lean index 7999b87f..16ae5b4e 100644 --- a/LMLExplore/InformationTheory/LaplaceMixture.lean +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -8,15 +8,13 @@ module public import Mathlib.InformationTheory.KullbackLeibler.Basic public import Mathlib.Probability.Independence.InfinitePi public import LMLExplore.Data.Nat.Choose.Bounds +public import LMLExplore.InformationTheory.MethodOfTypes public import LMLExplore.Probability.Martingale.LikelihoodRatio public import LMLExplore.Probability.Martingale.Ville public import LMLExplore.Probability.Process.Filtration public import LMLExplore.SequentialLearning.FiniteActions -public import TauCeti.MeasureTheory.Measure.Decomposition.Lebesgue public import TauCeti.Probability.Process.EmpiricalMeasure -import LMLExplore.InformationTheory.MethodOfTypes - /-! # Time-uniform concentration of empirical distributions by the Laplace mixture @@ -35,14 +33,14 @@ the probability that it ever reaches `1 / δ`. The likelihood of the rule of suc (`LMLExplore.prod_range_laplacePredictor`), the mixture of the likelihoods `∏_{t < n} p(ξ t)` over the uniform law of the probability vector `p`. It is within the factor `binom(n + m - 1, m - 1) ≤ (e (1 + n / (m - 1)))^{m - 1}` (`Nat.ascFactorial_div_factorial_le`) -of the maximum likelihood `∏ₐ (N_n(a) / n)^{N_n(a)} = exp (n KL(p̂_n ‖ ν)) ∏_{t < n} ν{ξ t}`, by the -multinomial bound `Nat.prod_div_pow_le_prod_factorial_div` +of the maximum likelihood `∏ₐ (N_n(a) / n)^{N_n(a)} = exp (n KL(p̂_n ‖ ν)) ∏_{t < n} ν{ξ t}` +(`LMLExplore.prod_measureReal_pow_typeCount_eq_mul_exp`, with the type counts identified with +`N_n` by `LMLExplore.typeCount_eq_pullCount`), by the multinomial bound +`Nat.prod_div_pow_le_prod_factorial_div` (`LMLExplore.exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor`). ## Main statements -* `LMLExplore.exp_mul_toReal_klDiv_empiricalFiniteMeasure`: for a finite family `x` of points - charged by `ν`, `exp (card κ KL(p̂ ‖ ν)) = ∏ᵢ p̂{x i} / ν{x i}`. * `LMLExplore.exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor`: `exp (n KL(p̂_n ‖ ν)) ≤ (e (1 + n / (m - 1)))^{m - 1} L_n`. * `LMLExplore.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le`: the time-uniform bound, @@ -123,57 +121,13 @@ lemma prod_range_laplacePredictor (n : ℕ) (ω : Ω) : · push_cast exact prod_congr rfl fun t _ ↦ add_comm _ _ -/-! ### The divergence of an empirical distribution -/ - -section Empirical - -variable [MeasurableSpace α] [MeasurableSingletonClass α] - omit [Fintype α] in -/-- The mass of a point under the empirical distribution of `ξ 0, …, ξ (n - 1)` is its frequency -`N_n(a) / n`. -/ -lemma measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div (n : ℕ) (ω : Ω) (a : α) : - (empiricalFiniteMeasure (fun k : Fin n ↦ ξ k ω) : Measure α).real {a} = - pullCount ξ a n ω / n := by - have h_sum : ∑ k : Fin n, ({a} : Set α).indicator (1 : α → ℝ≥0∞) (ξ k ω) = pullCount ξ a n ω := by - rw [pullCount_eq_sum, Nat.cast_sum, - ← Fin.sum_univ_eq_sum_range (fun s ↦ ((if ξ s ω = a then 1 else 0 : ℕ) : ℝ≥0∞))] - refine sum_congr rfl fun k _ ↦ ?_ - simp [Set.indicator_apply] - rw [measureReal_def, empiricalFiniteMeasure_apply (measurableSet_singleton a), h_sum, - ENNReal.toReal_mul, ENNReal.toReal_inv, Fintype.card_fin, ENNReal.toReal_natCast, - ENNReal.toReal_natCast, inv_mul_eq_div] - -omit [Fintype α] [DecidableEq α] in -/-- **The divergence of an empirical distribution**: for a nonempty finite family `x` of points -charged by a probability measure `ν`, with empirical distribution `p̂`, -`exp (card κ KL(p̂ ‖ ν)) = ∏ᵢ p̂{x i} / ν{x i}`. -/ -theorem exp_mul_toReal_klDiv_empiricalFiniteMeasure {κ : Type*} [Fintype κ] [Nonempty κ] - {ν : Measure α} [IsProbabilityMeasure ν] {x : κ → α} (hx : ∀ i, ν {x i} ≠ 0) : - exp (Fintype.card κ * (klDiv (empiricalFiniteMeasure x : Measure α) ν).toReal) = - ∏ i, (empiricalFiniteMeasure x : Measure α).real {x i} / ν.real {x i} := by - set p : Measure α := (empiricalFiniteMeasure x : Measure α) - have hκ : (0 : ℝ) < Fintype.card κ := by exact_mod_cast Fintype.card_pos - -- the empirical distribution only charges the points `x i` - have hac : p ≪ ν := empiricalFiniteMeasure_absolutelyContinuous hx - have hp_pos : ∀ i, 0 < p.real {x i} := fun i ↦ by - refine ENNReal.toReal_pos ?_ (measure_ne_top _ _) - rw [empiricalFiniteMeasure_apply (measurableSet_singleton _)] - refine mul_ne_zero (by simp) (ne_of_gt ?_) - refine lt_of_lt_of_le ?_ (single_le_sum (fun j _ ↦ zero_le) (mem_univ i)) - simp - have hν_pos : ∀ i, 0 < ν.real {x i} := fun i ↦ - ENNReal.toReal_pos (hx i) (measure_ne_top _ _) - have h_llr : ∀ i, llr p ν (x i) = log (p.real {x i} / ν.real {x i}) := fun i ↦ by - simp only [llr_def, Measure.rnDeriv_eq_measure_singleton_div (hx i) (measure_ne_top _ _), - ENNReal.toReal_div, measureReal_def] - rw [toReal_klDiv_of_measure_eq hac (by simp only [p, measure_univ]), - integral_empiricalFiniteMeasure_of_measurableSingletonClass, smul_eq_mul, ← mul_assoc, - mul_inv_cancel₀ hκ.ne', one_mul, exp_sum] - exact prod_congr rfl fun i _ ↦ by - rw [h_llr, exp_log (div_pos (hp_pos i) (hν_pos i))] - -end Empirical +/-- The type of the observations `ξ 0, …, ξ (n - 1)` is their vector of counts: the type count +of `a` is `N_n(a)`. -/ +lemma typeCount_eq_pullCount (n : ℕ) (ω : Ω) (a : α) : + typeCount (fun k : Fin n ↦ ξ k ω) a = pullCount ξ a n ω := by + rw [typeCount_def, card_filter, pullCount_eq_sum] + exact Fin.sum_univ_eq_sum_range (fun s ↦ if ξ s ω = a then 1 else 0) n /-! ### The likelihood ratio of the rule of succession -/ @@ -204,13 +158,20 @@ theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor -- the maximum likelihood: `exp (n KL(p̂_n ‖ ν)) P = ∏ₐ (N a / n) ^ N a` have h_max : exp (n * (klDiv (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : Measure α) ν).toReal) = (∏ a, ((N a : ℝ) / n) ^ N a) / P := by - have h := exp_mul_toReal_klDiv_empiricalFiniteMeasure (ν := ν) - (x := fun k : Fin n ↦ ξ k ω) fun k ↦ hξ k k.2 - rw [Fintype.card_fin] at h - rw [h, Fin.prod_univ_eq_prod_range (fun t ↦ (empiricalFiniteMeasure fun k : Fin n ↦ ξ k ω : - Measure α).real {ξ t ω} / ν.real {ξ t ω}) n, prod_div_distrib] - simp_rw [measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div] - rw [← prod_pow_pullCount (A := ξ) (fun a ↦ (pullCount ξ a n ω : ℝ) / n) n ω] + set x : Fin n → α := fun k ↦ ξ k ω + have hx : ∀ k, ν {x k} ≠ 0 := fun k ↦ hξ k k.2 + have hN_type : typeCount x = N := funext fun a ↦ typeCount_eq_pullCount n ω a + -- `P = ∏ₐ ν{a} ^ N a = (∏ₐ (N a / n) ^ N a) exp (-n KL(p̂_n ‖ ν))` + have hP_eq : P = (∏ a, ((N a : ℝ) / n) ^ N a) * + exp (-(n * (klDiv (empiricalFiniteMeasure x : Measure α) ν).toReal)) := by + have h := prod_measureReal_pow_typeCount_eq_mul_exp hx + simp_rw [measureReal_empiricalFiniteMeasure_singleton, hN_type] at h + rw [toReal_klDiv_eq_sum_mul_log_div (empiricalFiniteMeasure_absolutelyContinuous hx), + probReal_univ, probReal_univ, add_sub_cancel_right] + simp_rw [measureReal_empiricalFiniteMeasure_singleton, hN_type] + rw [← h, prod_pow_pullCount (fun a ↦ ν.real {a}) n ω] + rw [eq_div_iff hP.ne', hP_eq, exp_neg] + field_simp -- the likelihood of the rule of succession: `L_n P = ∏ₐ N a ! / m^{(n)}` have h_lap : predictorLikelihoodRatio ν (laplacePredictor ξ) ξ n ω = (∏ a, ((N a)! : ℝ)) / m.ascFactorial n / P := by From 375b19d3e2d0225efc2652cedf04f93a8fbe016d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 23:57:43 +0100 Subject: [PATCH 5/5] refactor: reuse prod_comp_eq_prod_pow_typeCount instead of prod_pow_pullCount Delete prod_pow_pullCount, a parallel copy of MethodOfTypes' prod_comp_eq_prod_pow_typeCount; its only use in LaplaceMixture now goes through prod_comp_eq_prod_pow_typeCount and Fin.prod_univ_eq_prod_range. Co-Authored-By: Claude Code --- LMLExplore/InformationTheory/LaplaceMixture.lean | 4 +++- LMLExplore/SequentialLearning/FiniteActions.lean | 12 +++--------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/LMLExplore/InformationTheory/LaplaceMixture.lean b/LMLExplore/InformationTheory/LaplaceMixture.lean index 16ae5b4e..63ce4139 100644 --- a/LMLExplore/InformationTheory/LaplaceMixture.lean +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -165,11 +165,13 @@ theorem exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor have hP_eq : P = (∏ a, ((N a : ℝ) / n) ^ N a) * exp (-(n * (klDiv (empiricalFiniteMeasure x : Measure α) ν).toReal)) := by have h := prod_measureReal_pow_typeCount_eq_mul_exp hx + rw [← prod_comp_eq_prod_pow_typeCount (fun a ↦ ν.real {a}) x, + Fin.prod_univ_eq_prod_range (fun k ↦ ν.real {ξ k ω})] at h simp_rw [measureReal_empiricalFiniteMeasure_singleton, hN_type] at h rw [toReal_klDiv_eq_sum_mul_log_div (empiricalFiniteMeasure_absolutelyContinuous hx), probReal_univ, probReal_univ, add_sub_cancel_right] simp_rw [measureReal_empiricalFiniteMeasure_singleton, hN_type] - rw [← h, prod_pow_pullCount (fun a ↦ ν.real {a}) n ω] + exact h rw [eq_div_iff hP.ne', hP_eq, exp_neg] field_simp -- the likelihood of the rule of succession: `L_n P = ∏ₐ N a ! / m^{(n)}` diff --git a/LMLExplore/SequentialLearning/FiniteActions.lean b/LMLExplore/SequentialLearning/FiniteActions.lean index 06951eaf..1db0073a 100644 --- a/LMLExplore/SequentialLearning/FiniteActions.lean +++ b/LMLExplore/SequentialLearning/FiniteActions.lean @@ -27,9 +27,9 @@ Facts about LML's `pullCount` that hold for any sequence of actions `A : ℕ → round `n`. * `sum_natCast_pullCount`: the pull counts of all arms before `K` add up to `K`, cast to an additive commutative monoid with one. -* `prod_pow_pullCount`, `prod_comp_pullCount`: products over the rounds regrouped arm by arm, the - multiplicative forms of LML's `sum_pullCount_mul` and `sum_comp_pullCount`; in particular - `prod_range_pullCount_action_add_one`: `∏_{s < t} (N_s(A_s) + 1) = ∏_a N_t(a)!`. +* `prod_comp_pullCount`: a product over the rounds of a function of the number of previous pulls + of the arm played, regrouped arm by arm, the multiplicative form of LML's `sum_comp_pullCount`; + in particular `prod_range_pullCount_action_add_one`: `∏_{s < t} (N_s(A_s) + 1) = ∏_a N_t(a)!`. * `exists_pullCount_eq_zero_of_lt_card`: before round `Fintype.card α`, some arm has not been pulled yet. * `pullCount_card_eq_one_of_forall_pullCount_action_eq_zero`: if each of the first @@ -112,12 +112,6 @@ lemma sum_natCast_pullCount {R : Type*} [AddCommMonoidWithOne R] (ω : Ω) (K : ∑ a, (pullCount A a K ω : R) = K := by rw [← Nat.cast_sum, sum_pullCount] -/-- `∏_a f(a) ^ N_t(a) = ∏_{s < t} f(A_s)`: the multiplicative form of LML's `sum_pullCount_mul`. -/ -lemma prod_pow_pullCount {M : Type*} [CommMonoid M] (f : α → M) (t : ℕ) (ω : Ω) : - ∏ a, f a ^ pullCount A a t ω = ∏ s ∈ range t, f (A s ω) := by - simp_rw [pullCount, ← prod_const] - exact prod_fiberwise' (range t) (A · ω) f - /-- `∏_{s < t} f(N_s(A_s)) = ∏_a ∏_{j < N_t(a)} f(j)`: the product over the rounds of a function of the number of previous pulls of the arm played is, arm by arm, its product over `0, …, N_t(a) - 1`. This is the multiplicative form of LML's `sum_comp_pullCount`. -/