From e8e5a137c8888aee6b938fb0473bc5a62e0adb14 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 13:22:27 +0100 Subject: [PATCH] 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 0000000..708182f --- /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 0000000..7bfcbda --- /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 0000000..a7d2333 --- /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 af76acc..cf8d871 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