diff --git a/LMLExplore/Data/Nat/Choose/Bounds.lean b/LMLExplore/Data/Nat/Choose/Bounds.lean new file mode 100644 index 00000000..5783e245 --- /dev/null +++ b/LMLExplore/Data/Nat/Choose/Bounds.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.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, 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`. +* `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!`. + +These 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] + +/-- **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 +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 + +/-- **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 new file mode 100644 index 00000000..63ce4139 --- /dev/null +++ b/LMLExplore/InformationTheory/LaplaceMixture.lean @@ -0,0 +1,301 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.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.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}` (`Nat.ascFactorial_div_factorial_le`) +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_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 _ _ + +omit [Fintype α] in +/-- 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 -/ + +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 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 + 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 + 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] + 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)}` + 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 + 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 + 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 + 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 ν ≠ ∞ := + 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 + 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` + exact LMLExplore.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le + (ξ := 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 new file mode 100644 index 00000000..4ad7c7e8 --- /dev/null +++ b/LMLExplore/Probability/Martingale/LikelihoodRatio.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.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`. + +## 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, + *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/Probability/Martingale/RateFunction.lean b/LMLExplore/Probability/Martingale/RateFunction.lean index b055c7c0..1509640b 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 936e7ee9..1d672d08 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 new file mode 100644 index 00000000..affd95c0 --- /dev/null +++ b/LMLExplore/Probability/Process/Filtration.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Probability.Independence.Basic +public import Mathlib.Probability.Process.Filtration + +/-! +# The filtration of the strict past of a process + +This file 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_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 ι] {Ω : 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 MeasureTheory.Filtration diff --git a/LMLExplore/SequentialLearning/FiniteActions.lean b/LMLExplore/SequentialLearning/FiniteActions.lean index e328bd76..1db0073a 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_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 @@ -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,25 @@ lemma sum_natCast_pullCount {R : Type*} [AddCommMonoidWithOne R] (ω : Ω) (K : ∑ a, (pullCount A a K ω : R) = K := by rw [← Nat.cast_sum, sum_pullCount] +/-- `∏_{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