From 23fea681cede9482b33b69973cd956584545e01b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 13:32:09 +0100 Subject: [PATCH 1/7] feat: large deviations of the empirical means of a run under static allocations, and the error exponent of static proportions Co-Authored-By: Claude Code --- .../Identification/StaticProportions.lean | 120 ++++- .../Probability/LargeDeviations/Pi.lean | 4 +- .../SequentialLearning/StaticAllocation.lean | 502 ++++++++++++++++++ LMLExplore/SequentialLearning/SumRewards.lean | 53 +- 4 files changed, 663 insertions(+), 16 deletions(-) create mode 100644 LMLExplore/SequentialLearning/StaticAllocation.lean diff --git a/LMLExplore/Identification/StaticProportions.lean b/LMLExplore/Identification/StaticProportions.lean index 535ba420..85f45383 100644 --- a/LMLExplore/Identification/StaticProportions.lean +++ b/LMLExplore/Identification/StaticProportions.lean @@ -7,6 +7,7 @@ module public import LMLExplore.Identification.CumulativeTracking public import LMLExplore.Identification.DifficultyRatio +public import LMLExplore.SequentialLearning.StaticAllocation public import LeanMachineLearning.SequentialLearning.SumRewards /-! @@ -56,6 +57,19 @@ in exponential families and a regular task [D23, Theorem 1]. * `LMLExplore.Identification.IdentTask.IsStaticProportions.errorProb_eq`: the probability of error of a static proportions family is the probability that the recommendation of the empirical means is not correct. +* `LMLExplore.Identification.IdentTask.IsStaticProportions.hasLDP_empMean`: for arms whose + cumulant generating functions are finite near `0`, the laws of the empirical means of a static + proportions family satisfy the large deviation principle with rate function + `x ↦ ∑ a, w a I_a(x a)`, for the Cramér rate functions `I_a` of the arms. +* `LMLExplore.Identification.IdentTask.IsStaticProportions.limsup_log_errorProb_div_le`, + `LMLExplore.Identification.IdentTask.IsStaticProportions.neg_le_liminf_log_errorProb_div`: the + error exponent of a static proportions family is between the infima of `∑ a, w a I_a(x a)` over + the interior and over the closure of the set of the vectors `x` whose recommendation `rec x` is + not correct [GJ04; D23, Theorem 12]. +* `LMLExplore.Identification.IdentTask.IsStaticProportions.tendsto_log_errorProb_div`, + `LMLExplore.Identification.IdentTask.IsStaticProportions.tendsto_errorComplexity`: when the two + infima agree, the error exponent is their common value `c`, and the error complexity + `T / log (1 / p_{θ,T})` tends to `c⁻¹`. ## References @@ -71,9 +85,10 @@ in exponential families and a regular task [D23, Theorem 1]. public section -open MeasureTheory Learning +open MeasureTheory Learning Filter Topology ProbabilityTheory +open TauCeti.Probability (HasLDP) -open scoped ENNReal +open scoped ENNReal NNReal namespace LMLExplore.Identification.IdentTask @@ -250,4 +265,105 @@ lemma IsStaticProportions.errorProb_eq (h𝒜 : task.IsStaticProportions rec lintegral_map (ProbabilityTheory.Kernel.measurable_coe _ hθ.compl) (IT.measurable_hist T), lintegral_congr heq, lintegral_indicator_one hE] +/-! ### The error exponent of static proportions families -/ + +variable [MeasurableSingletonClass α] {θ : Θ} + +/-- **Large deviations of the empirical means of a static proportions family** [GJ04; +D23, Theorem 12]. If the cumulant generating function of each arm of the admissible model `θ` is +finite on a neighbourhood of `0`, the laws of the vectors of the empirical means after `T` rounds +of a static proportions family with proportions `w` satisfy the large deviation principle with +speed `1 / T` and rate function `x ↦ ∑ a, w a I_a(x a)`, with `I_a` the Cramér rate function of +the law `ν_a(θ)` of arm `a`. -/ +theorem IsStaticProportions.hasLDP_empMean (h𝒜 : task.IsStaticProportions rec 𝒜 w) + (hθ : θ ∈ task.M) (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) : + HasLDP atTop (fun T : ℕ ↦ (T : ℝ≥0)⁻¹) + (fun T ↦ (trajMeasure (𝒜 T).alg (Environment.bandit (task.ν θ))).map + fun h a ↦ empMean IT.action IT.feedback a T h) + (fun x ↦ ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) := + hasLDP_empMean_rateFunction_of_abs_pullCount_sub_le hν h𝒜.pos (Fintype.card α) + (fun T ↦ IT.isAlgEnvSeq_trajMeasure (𝒜 T).alg (Environment.bandit (task.ν θ))) + (h𝒜.ae_abs_pullCount_sub_le θ hθ) + +/-- **Upper bound on the error exponent of a static proportions family** [GJ04; D23, Theorem 12]. +If the set of correct answers of the admissible model `θ` is measurable and the cumulant generating +function of each of its arms is finite on a neighbourhood of `0`, the probability of error +`p_{θ,T}` of a static proportions family with proportions `w` and recommendation rule `rec` +satisfies `limsup_T (1 / T) log p_{θ,T} ≤ -inf_x ∑ a, w a I_a(x a)`, the infimum over the closure +of the set of the vectors `x` with `rec x` not correct for `θ`, with `I_a` the Cramér rate function +of the law `ν_a(θ)` of arm `a`. -/ +theorem IsStaticProportions.limsup_log_errorProb_div_le (h𝒜 : task.IsStaticProportions rec 𝒜 w) + (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ)) + (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) : + limsup (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop ≤ + -((⨅ x ∈ closure {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal) := by + have h := (h𝒜.hasLDP_empMean hθ hν).limsup_le_neg_iInf_closure {x | rec x ∉ task.correct θ} + simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h + refine le_trans (limsup_le_limsup (Eventually.of_forall fun T ↦ ?_)) h + -- The error is the event that the empirical means lie in the set where `rec` is not correct. + have hmeas : Measurable fun (h : ℕ → Round Unit α ℝ) a ↦ empMean IT.action IT.feedback a T h := + .of_eval fun a ↦ measurable_empMean IT.measurable_action IT.measurable_feedback a T + rw [h𝒜.errorProb_eq hcorrect] + exact EReal.div_le_div_right_of_nonneg (by positivity) (ENNReal.log_monotone + (Measure.le_map_apply hmeas.aemeasurable {x | rec x ∉ task.correct θ})) + +/-- **Lower bound on the error exponent of a static proportions family** [GJ04; D23, Theorem 12]. +If the set of correct answers of the admissible model `θ` is measurable and the cumulant generating +function of each of its arms is finite on a neighbourhood of `0`, the probability of error +`p_{θ,T}` of a static proportions family with proportions `w` and recommendation rule `rec` +satisfies `-inf_x ∑ a, w a I_a(x a) ≤ liminf_T (1 / T) log p_{θ,T}`, the infimum over the +interior of the set of the vectors `x` with `rec x` not correct for `θ`, with `I_a` the Cramér rate +function of the law `ν_a(θ)` of arm `a`. -/ +theorem IsStaticProportions.neg_le_liminf_log_errorProb_div + (h𝒜 : task.IsStaticProportions rec 𝒜 w) (hθ : θ ∈ task.M) + (hcorrect : MeasurableSet (task.correct θ)) + (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) : + -((⨅ x ∈ interior {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal) ≤ + liminf (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop := by + have h := (h𝒜.hasLDP_empMean hθ hν).lower_bound (interior {x | rec x ∉ task.correct θ}) + isOpen_interior + simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h + refine h.trans (liminf_le_liminf (Eventually.of_forall fun T ↦ ?_)) + -- The empirical means in the interior of the set where `rec` is not correct give an error. + have hmeas : Measurable fun (h : ℕ → Round Unit α ℝ) a ↦ empMean IT.action IT.feedback a T h := + .of_eval fun a ↦ measurable_empMean IT.measurable_action IT.measurable_feedback a T + rw [h𝒜.errorProb_eq hcorrect, Measure.map_apply hmeas isOpen_interior.measurableSet] + exact EReal.div_le_div_right_of_nonneg (by positivity) + (ENNReal.log_monotone (measure_mono (Set.preimage_mono interior_subset))) + +/-- **The error exponent of a static proportions family** [GJ04; D23, Theorem 12]. If moreover the +infima of `x ↦ ∑ a, w a I_a(x a)` over the interior and over the closure of the set of the vectors +`x` with `rec x` not correct for `θ` agree, then `(1 / T) log p_{θ,T}` tends to minus their common +value. -/ +theorem IsStaticProportions.tendsto_log_errorProb_div (h𝒜 : task.IsStaticProportions rec 𝒜 w) + (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ)) + (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) + (h_eq : ⨅ x ∈ interior {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) = + ⨅ x ∈ closure {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) : + Tendsto (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop + (𝓝 (-((⨅ x ∈ closure {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal))) := + tendsto_of_le_liminf_of_limsup_le (h_eq ▸ h𝒜.neg_le_liminf_log_errorProb_div hθ hcorrect hν) + (h𝒜.limsup_log_errorProb_div_le hθ hcorrect hν) + +/-- **The error complexity of a static proportions family** [D23, Theorem 12]. Under the hypotheses +of `IsStaticProportions.tendsto_log_errorProb_div`, the error complexity `T / log (1 / p_{θ,T})` +tends to the inverse of the error exponent `inf_x ∑ a, w a I_a(x a)`. -/ +theorem IsStaticProportions.tendsto_errorComplexity (h𝒜 : task.IsStaticProportions rec 𝒜 w) + (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ)) + (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) + (h_eq : ⨅ x ∈ interior {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) = + ⨅ x ∈ closure {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) : + Tendsto (task.errorComplexity 𝒜 θ) atTop + (𝓝 (⨅ x ∈ closure {x | rec x ∉ task.correct θ}, + ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a))⁻¹) := + tendsto_errorComplexity_of_tendsto_log_div + (h𝒜.tendsto_log_errorProb_div hθ hcorrect hν h_eq) + end LMLExplore.Identification.IdentTask diff --git a/LMLExplore/Probability/LargeDeviations/Pi.lean b/LMLExplore/Probability/LargeDeviations/Pi.lean index 24475dd7..84dcd518 100644 --- a/LMLExplore/Probability/LargeDeviations/Pi.lean +++ b/LMLExplore/Probability/LargeDeviations/Pi.lean @@ -40,6 +40,8 @@ rates is above `r`. * `LMLExplore.hasLDP_pi`: the large deviation principle of the product measures, with rate function `x ↦ ∑ a, I a (x a)`. +* `LMLExplore.neg_sum_le_liminf_log_pi`: the lower bound of the product principle at a point, + which needs no goodness of the rate functions. * `LMLExplore.hasLDP_pi_comp_of_tendsto_div`: the large deviation principle of the product measures `Measure.pi fun a ↦ P a (m a n)` with `m a n / n → w a > 0`, with rate function `x ↦ ∑ a, w a I a (x a)`. @@ -89,7 +91,7 @@ variable {ι : Type*} [Fintype ι] {X : ι → Type*} [∀ a, MeasurableSpace (X /-- **The lower bound of the product principle.** If each `P a` satisfies the lower bound of a large deviation principle at the speed `1 / n` with rate function `I a`, every neighbourhood `s` of a point `x` satisfies `-∑ a, I a (x a) ≤ liminf_n (1 / n) log (∏ a, P a n) s`. -/ -private lemma neg_sum_le_liminf_log_pi [∀ a, TopologicalSpace (X a)] +theorem neg_sum_le_liminf_log_pi [∀ a, TopologicalSpace (X a)] [∀ a n, SigmaFinite (P a n)] (h : ∀ a, HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) (P a) (I a)) {x : ∀ a, X a} {s : Set (∀ a, X a)} (hs : s ∈ 𝓝 x) : -((∑ a, I a (x a) : ℝ≥0∞) : EReal) ≤ liminf (fun n : ℕ ↦ diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean new file mode 100644 index 00000000..cb941714 --- /dev/null +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -0,0 +1,502 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.Probability.LargeDeviations.Pi +public import LMLExplore.SequentialLearning.SumRewards + +/-! +# Large deviations of the empirical means of a run under static allocations + +Let the arms `a` of a stochastic bandit `ν : Kernel α ℝ`, finitely many, have laws whose empirical +means satisfy the large deviation principle with good rate functions `I a`, for instance by +Cramér's theorem when their cumulant generating functions are finite near `0`. Consider runs of +algorithms whose numbers of pulls after `T` rounds satisfy `|N_{T,a} - T w a| ≤ k` almost surely, +for proportions `w a > 0`, as the static proportions algorithms of fixed-budget identification do. +Then the laws of the vectors `μ̂_T` of the empirical means after `T` rounds satisfy the large +deviation principle with speed `1 / T` and rate function `x ↦ ∑ a, w a I a (x a)` +[GJ04; D23, Theorem 12]. The numbers of pulls are random and may depend on the rewards, so the +law of `μ̂_T` is not a product, unlike the laws of `LMLExplore.hasLDP_pi_comp_of_tendsto_div`. + +The proof goes through LML's reward stream model `streamMeasure ν`, the stack of rewards of +[LS, Section 4.6], whose rows are independent i.i.d. sequences +(`LMLExplore.streamMeasure_forall_row_mem`): the empirical mean of arm `a` +after `T` rounds is the mean of the first `N_{T,a}` entries of its row +(`hasLaw_rewardByCount_streamMeasure`). + +* The upper bound is uniform over the numbers of samples in a window around `T w` + (`eventually_streamMeasure_mean_mem_le_exp`), by the product principle for fixed numbers of + samples growing like `T w`; the `(2 k + 1)^K` possible numbers of pulls then cost a constant + factor. +* The lower bound asks the mean of the first `⌈T w a - k⌉₊` entries of each row to be close to the + target and the next `2 k` entries to lie in a fixed ball + (`exists_eventually_le_streamMeasure_forall_mean_mem`): the means after every number of pulls in + the window are then close to the target, at the price of a constant factor. + +## Main statements + +* `MeasureTheory.Measure.infinitePi_mean_mem_and_forall_mem`: for an i.i.d. sequence, the mean of + the first `n` terms and the next `m` terms are independent. +* `LMLExplore.eventually_streamMeasure_mean_mem_le_exp`, + `LMLExplore.exists_eventually_le_streamMeasure_forall_mean_mem`: the exponential upper and lower + bounds for the empirical means of the rows, uniformly over the numbers of samples in a window. +* `LMLExplore.measure_empMean_mem_le_streamMeasure`, + `LMLExplore.streamMeasure_le_measure_empMean_mem`: the transfer of events about the empirical + means of a run to the stream model, in both directions, when the numbers of pulls lie in a set + almost surely. +* `LMLExplore.hasLDP_empMean_of_abs_pullCount_sub_le`: the large deviation principle of the + empirical means of runs with numbers of pulls within `k` of `T w`. +* `LMLExplore.hasLDP_empMean_rateFunction_of_abs_pullCount_sub_le`: the same with the Cramér rate + functions of arms whose cumulant generating functions are finite near `0`. + +## Implementation notes + +The statements and proofs are adapted from the formalization of [D23] in the paper project +RemyDegenne/Degenne2023Existence (same author), which works in LML's array model for trajectory +measures. Here the theorems hold for every algorithm-environment sequence against the bandit, the +transfer to the stream goes through the rewards by count of the run, and the bounds for fixed +numbers of samples come from the product principle `LMLExplore.hasLDP_pi_comp_of_tendsto_div`. + +## References + +* [D23] R. Degenne, *On the existence of a complexity in fixed budget bandit identification*, + COLT 2023, arXiv:2303.09468v2, Theorem 12. +* [GJ04] P. Glynn and S. Juneja, *A large deviations perspective on ordinal optimization*, + Winter Simulation Conference 2004. +* [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020. +-/ + +public section + +open MeasureTheory ProbabilityTheory Filter Topology Finset Learning Bandits +open TauCeti.Probability (HasLDP IsGoodRateFunction) + +open scoped ENNReal NNReal + +namespace MeasureTheory.Measure + +/-- **The mean of the first terms of an i.i.d. sequence and the next terms are independent.** For +an i.i.d. sequence of law `μ`, the mean of the first `n` terms lies in `B` and the next `m` terms +lie in `C` with probability `P(μ̂_n ∈ B) μ(C)^m`, where `μ̂_n` is the mean of `n` independent +samples of `μ`. -/ +theorem infinitePi_mean_mem_and_forall_mem (μ : Measure ℝ) [IsProbabilityMeasure μ] (n m : ℕ) + {B C : Set ℝ} (hB : MeasurableSet B) (hC : MeasurableSet C) : + (Measure.infinitePi fun _ : ℕ ↦ μ) + {z | (∑ i ∈ range n, z i) / (n : ℝ) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + ((Measure.pi fun _ : Fin n ↦ μ).map fun y ↦ (∑ i, y i) / (n : ℝ)) B * μ C ^ m := by + -- The first `n` terms and the next `m` terms are independent. + have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) + (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) + (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) + simp only [id] at h_ind + have h_mean : Measurable fun u : {i // i ∈ range n} → ℝ ↦ (∑ i, u i) / (n : ℝ) := by fun_prop + have h_set : {z : ℕ → ℝ | (∑ i ∈ range n, z i) / (n : ℝ) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + (fun z (i : range n) ↦ z i) ⁻¹' ((fun u ↦ (∑ i, u i) / (n : ℝ)) ⁻¹' B) ∩ + (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by + ext z + simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, + Set.mem_univ, true_implies, Subtype.forall, mem_Ico] + refine and_congr ?_ ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ + · rw [Finset.sum_coe_sort (range n) z] + · obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 + exact h j (by omega) + rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_mean hB) (.univ_pi fun _ ↦ hC)] + congr 1 + · -- The first `n` terms are `n` independent samples of `μ`. + have h_fin : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = + Measure.pi fun _ : Fin n ↦ μ := by + rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] + rw [← h_fin, Measure.map_map (by fun_prop) (by fun_prop), + Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] + congr 1 + ext z + simp only [Set.mem_preimage, Function.comp_apply] + rw [Finset.sum_coe_sort (range n) z, Fin.sum_univ_eq_sum_range (fun i ↦ z i)] + · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = + ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by + ext z + simp + rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, + Nat.add_sub_cancel_left] + +end MeasureTheory.Measure + +namespace LMLExplore + +variable {α : Type*} {mα : MeasurableSpace α} + +/-! ### Large deviations of the empirical means of the rows of the stream -/ + +section Stream + +variable [Fintype α] {ν : Kernel α ℝ} [IsMarkovKernel ν] {I : α → ℝ → ℝ≥0∞} {w : α → ℝ} + +/-- If `|m T - T w| ≤ c` for every `T`, then `m T / T → w`. -/ +private lemma tendsto_div_of_abs_sub_le {m : ℕ → ℕ} {w c : ℝ} (h : ∀ T, |(m T : ℝ) - T * w| ≤ c) : + Tendsto (fun T ↦ (m T : ℝ) / T) atTop (𝓝 w) := by + have h0 : Tendsto (fun T : ℕ ↦ ((m T : ℝ) - T * w) / T) atTop (𝓝 0) := by + refine squeeze_zero_norm (fun T ↦ ?_) (tendsto_const_div_atTop_nhds_zero_nat c) + rw [norm_div, Real.norm_eq_abs, Real.norm_eq_abs, Nat.abs_cast] + exact div_le_div_of_nonneg_right (h T) T.cast_nonneg + have h1 : Tendsto (fun T : ℕ ↦ ((m T : ℝ) - T * w) / T + w) atTop (𝓝 w) := by + simpa using h0.add_const w + refine h1.congr' ?_ + filter_upwards [eventually_ne_atTop 0] with T hT + rw [sub_div, mul_div_cancel_left₀ _ (Nat.cast_ne_zero.2 hT), sub_add_cancel] + +/-- **The exponential upper bound for the rows of the reward stream, uniformly in a window.** Let +the laws of the empirical means of `m` independent samples of `ν a` satisfy the large deviation +principle with speed `1 / m` and a good rate function `I a`, and let `w a > 0`. For a closed set +`F` and every real `r` below the infimum of `x ↦ ∑ a, w a I a (x a)` on `F`, for every large `T` +and every `n : α → ℕ` with `|n a - T w a| ≤ c`, the vector of the empirical means of the first +`n a` entries of the rows lies in `F` with probability at most `exp (-(T r))`. -/ +theorem eventually_streamMeasure_mean_mem_le_exp + (hP : ∀ a, HasLDP atTop (fun m : ℕ ↦ (m : ℝ≥0)⁻¹) + (fun m ↦ (Measure.pi fun _ : Fin m ↦ ν a).map fun z : Fin m → ℝ ↦ (∑ i, z i) / (m : ℝ)) + (I a)) + (hI : ∀ a, IsGoodRateFunction (I a)) (hw : ∀ a, 0 < w a) (c : ℝ) {F : Set (α → ℝ)} + (hF : IsClosed F) {r : ℝ} + (hr : (r : EReal) < ((⨅ x ∈ F, ∑ a, ENNReal.ofReal (w a) * I a (x a) : ℝ≥0∞) : EReal)) : + ∀ᶠ T : ℕ in atTop, ∀ n : α → ℕ, (∀ a, |(n a : ℝ) - T * w a| ≤ c) → + streamMeasure ν {ω | (fun a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ∈ F} ≤ + ENNReal.ofReal (Real.exp (-(T * r))) := by + classical + -- For each `T`, pick numbers of samples in the window that violate the bound if there are some, + -- and `⌈T w⌉₊` otherwise. They grow like `T w`, so the product principle applies to them. + set B : ℕ → (α → ℕ) → Prop := fun T n ↦ (∀ a, |(n a : ℝ) - T * w a| ≤ c) ∧ + ENNReal.ofReal (Real.exp (-(T * r))) < + streamMeasure ν {ω | (fun a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ∈ F} with hB + set m : ℕ → α → ℕ := fun T ↦ if h : ∃ n, B T n then h.choose else fun a ↦ ⌈T * w a⌉₊ with hm + have hm_abs (T : ℕ) (a : α) : |(m T a : ℝ) - T * w a| ≤ max c 1 := by + by_cases h : ∃ n, B T n + · simp only [hm, h, dite_true] + exact (h.choose_spec.1 a).trans (le_max_left _ _) + · simp only [hm, h, dite_false] + have h0 : 0 ≤ (T : ℝ) * w a := mul_nonneg T.cast_nonneg (hw a).le + rw [abs_of_nonneg (sub_nonneg.2 (Nat.le_ceil _))] + linarith [Nat.ceil_lt_add_one h0, le_max_right c 1] + have hLDP := hasLDP_pi_comp_of_tendsto_div hP hI (m := fun a T ↦ m T a) hw + fun a ↦ tendsto_div_of_abs_sub_le fun T ↦ hm_abs T a + filter_upwards [hLDP.eventually_measure_le_exp hF hr] with T hT n hn + by_contra hlt + have h : ∃ n, B T n := ⟨n, hn, not_le.1 hlt⟩ + have hmT : m T = h.choose := by simp only [hm, h, dite_true] + have h_eq := congrArg (· F) (streamMeasure_map_mean (ν := ν) (m T)) + rw [Measure.map_apply (by fun_prop) hF.measurableSet] at h_eq + have h_bad := h.choose_spec.2 + rw [← hmT] at h_bad + exact absurd (h_bad.trans_le (h_eq.trans_le hT)) (lt_irrefl _) + +omit [Fintype α] in +/-- The natural numbers within `k` of a real `x` are `⌈x - k⌉₊ + d` for some `d ≤ 2 k`. -/ +private lemma exists_eq_ceil_sub_add {x : ℝ} {k n : ℕ} (hn : |(n : ℝ) - x| ≤ k) : + ∃ d ≤ 2 * k, n = ⌈x - k⌉₊ + d := by + have h := abs_le.1 hn + have hlo : ⌈x - k⌉₊ ≤ n := Nat.ceil_le.2 (by linarith) + have hhi : n ≤ ⌈x - k⌉₊ + 2 * k := by + have : (n : ℝ) ≤ ⌈x - k⌉₊ + 2 * k := by linarith [Nat.le_ceil (x - k)] + exact_mod_cast this + exact ⟨n - ⌈x - k⌉₊, by omega, (Nat.add_sub_cancel' hlo).symm⟩ + +omit [Fintype α] in +/-- For a real `x ≥ 0` and `d ≤ 2 k`, the natural number `⌈x - k⌉₊ + d` is within `2 k + 1` +of `x`. -/ +private lemma abs_ceil_sub_add_sub_le {x : ℝ} (hx : 0 ≤ x) {k d : ℕ} (hd : d ≤ 2 * k) : + |((⌈x - k⌉₊ + d : ℕ) : ℝ) - x| ≤ 2 * k + 1 := by + have h1 : x - k ≤ ⌈x - k⌉₊ := Nat.le_ceil _ + have h2 : (⌈x - k⌉₊ : ℝ) < x + 1 := (Nat.cast_le.2 (Nat.ceil_mono + (by linarith [k.cast_nonneg (α := ℝ)]))).trans_lt (Nat.ceil_lt_add_one hx) + have h3 : (d : ℝ) ≤ 2 * k := by exact_mod_cast hd + rw [abs_le] + push_cast + constructor <;> linarith [d.cast_nonneg (α := ℝ)] + +omit [Fintype α] in +/-- If the mean of `n₀` numbers of sum `S` is within `δ / 2` of `x`, and `j` further numbers are +within `L` of `x`, with `2 j L < n₀ δ`, then the mean of all the `n₀ + j` numbers is within `δ` +of `x`. -/ +private lemma dist_mean_add_lt {n₀ j : ℕ} (hn₀ : 0 < n₀) {S x δ L : ℝ} {z : ℕ → ℝ} + (hS : dist (S / n₀) x < δ / 2) (hz : ∀ i < j, dist (z i) x ≤ L) (hjL : 2 * (j * L) < n₀ * δ) : + dist ((S + ∑ i ∈ range j, z i) / ((n₀ + j : ℕ) : ℝ)) x < δ := by + have hn₀' : (0 : ℝ) < n₀ := by exact_mod_cast hn₀ + have hm : (0 : ℝ) < ((n₀ + j : ℕ) : ℝ) := by positivity + have hS' : |S - n₀ * x| < n₀ * (δ / 2) := by + rw [Real.dist_eq, show S / n₀ - x = (S - n₀ * x) / n₀ by field_simp, abs_div, + abs_of_pos hn₀', div_lt_iff₀ hn₀'] at hS + linarith + have hsum : |∑ i ∈ range j, (z i - x)| ≤ j * L := by + refine (Finset.abs_sum_le_sum_abs _ _).trans ?_ + refine (Finset.sum_le_sum fun i hi ↦ (?_ : |z i - x| ≤ L)).trans (by simp) + rw [← Real.dist_eq] + exact hz i (Finset.mem_range.1 hi) + have h_eq : (S + ∑ i ∈ range j, z i) / ((n₀ + j : ℕ) : ℝ) - x = + ((S - n₀ * x) + ∑ i ∈ range j, (z i - x)) / ((n₀ + j : ℕ) : ℝ) := by + rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul] + field_simp + push_cast + ring + have hδ : 0 < δ := by linarith [dist_nonneg.trans_lt hS] + have hj : (n₀ : ℝ) ≤ ((n₀ + j : ℕ) : ℝ) := by exact_mod_cast Nat.le_add_right n₀ j + rw [Real.dist_eq, h_eq, abs_div, abs_of_pos hm, div_lt_iff₀ hm] + calc |S - n₀ * x + ∑ i ∈ range j, (z i - x)| + ≤ |S - n₀ * x| + |∑ i ∈ range j, (z i - x)| := abs_add_le _ _ + _ < n₀ * δ := by linarith + _ ≤ δ * ((n₀ + j : ℕ) : ℝ) := by nlinarith + +omit [Fintype α] in +/-- If the mean of the first `n₀ > 0` terms of `z` is within `δ / 2` of `x`, the next `2 k` terms +are within `L` of `x`, and `4 k L < n₀ δ`, then the mean of the first `n₀ + d` terms of `z` is +within `δ` of `x` for every `d ≤ 2 k`. -/ +private lemma dist_mean_lt {z : ℕ → ℝ} {n₀ k d : ℕ} {x δ L : ℝ} (hn₀ : 0 < n₀) (hL : 0 ≤ L) + (hδL : 4 * k * L < n₀ * δ) (hz : dist ((∑ i ∈ range n₀, z i) / n₀) x < δ / 2) + (hzL : ∀ j < 2 * k, dist (z (n₀ + j)) x ≤ L) (hd : d ≤ 2 * k) : + dist ((∑ i ∈ range (n₀ + d), z i) / ((n₀ + d : ℕ) : ℝ)) x < δ := by + rw [Finset.sum_range_add] + refine dist_mean_add_lt hn₀ hz (fun i hi ↦ hzL i (by omega)) ?_ + have : (d : ℝ) ≤ 2 * k := by exact_mod_cast hd + nlinarith + +/-- **The exponential lower bound for the rows of the reward stream, uniformly in a window.** Let +the laws of the empirical means of `m` independent samples of `ν a` satisfy the large deviation +principle with speed `1 / m` and rate function `I a`, and let `w a > 0`. For a neighbourhood `U` of +`x` and every real `r > ∑ a, w a I a (x a)`, there is `C > 0` such that for every large `T`, with +probability at least `C exp (-(T r))`, the vectors of the empirical means of the first `n a` entries +of the rows lie in `U` for all the `n : α → ℕ` in the window `|n a - T w a| ≤ k`. -/ +theorem exists_eventually_le_streamMeasure_forall_mean_mem + (hP : ∀ a, HasLDP atTop (fun m : ℕ ↦ (m : ℝ≥0)⁻¹) + (fun m ↦ (Measure.pi fun _ : Fin m ↦ ν a).map fun z : Fin m → ℝ ↦ (∑ i, z i) / (m : ℝ)) + (I a)) + (hw : ∀ a, 0 < w a) (k : ℕ) {x : α → ℝ} {U : Set (α → ℝ)} (hU : U ∈ 𝓝 x) {r : ℝ} + (hr : ((∑ a, ENNReal.ofReal (w a) * I a (x a) : ℝ≥0∞) : EReal) < r) : + ∃ C : ℝ≥0∞, C ≠ 0 ∧ ∀ᶠ T : ℕ in atTop, C * ENNReal.ofReal (Real.exp (-(T * r))) ≤ + streamMeasure ν {ω | ∀ n : α → ℕ, (∀ a, |(n a : ℝ) - T * w a| ≤ k) → + (fun a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ∈ U} := by + obtain ⟨δ, hδ, hδU⟩ := Metric.mem_nhds_iff.1 hU + -- A closed ball of positive probability for each arm. + have hL (a : α) : ∃ L : ℕ, ν a (Metric.closedBall (x a) L) ≠ 0 := by + by_contra! h + have h_null := measure_iUnion_null (μ := ν a) h + rw [Metric.iUnion_closedBall_nat, measure_univ] at h_null + exact one_ne_zero h_null + choose L hL using hL + -- The first `n₀ T a = ⌈T w a - k⌉₊` entries of the row of `a`, a number within `2 k + 1` of + -- `T w a`, have a mean close to `x a` with probability at least `exp (-(T r))` jointly. + set n₀ : ℕ → α → ℕ := fun T a ↦ ⌈T * w a - k⌉₊ with hn₀ + have hn₀_le (T : ℕ) (a : α) : T * w a - k ≤ n₀ T a := Nat.le_ceil _ + have hn₀_abs (T : ℕ) (a : α) : |(n₀ T a : ℝ) - T * w a| ≤ 2 * k + 1 := + abs_ceil_sub_add_sub_le (d := 0) (mul_nonneg T.cast_nonneg (hw a).le) (Nat.zero_le _) + set V : Set (α → ℝ) := Set.univ.pi fun a ↦ Metric.ball (x a) (δ / 2) + have h_box := eventually_exp_le_of_neg_le_liminf_inv_mul_log + (neg_sum_le_liminf_log_pi (fun a ↦ (hP a).comp_of_tendsto_div (hw a) + (tendsto_div_of_abs_sub_le fun T ↦ hn₀_abs T a)) + (x := x) (s := V) (set_pi_mem_nhds Set.finite_univ fun a _ ↦ + Metric.ball_mem_nhds (x a) (half_pos hδ))) hr + refine ⟨∏ a, ν a (Metric.closedBall (x a) (L a)) ^ (2 * k), + Finset.prod_ne_zero_iff.2 fun a _ ↦ pow_ne_zero _ (hL a), ?_⟩ + filter_upwards [h_box, eventually_all.2 fun a ↦ (tendsto_natCast_atTop_atTop.atTop_mul_const + (hw a)).eventually_ge_atTop ((k : ℝ) + 1 + 4 * k * L a / δ)] with T hT hT_large + have hLδ (a : α) : 0 ≤ 4 * k * (L a : ℝ) / δ := by positivity + have hn₀_pos (a : α) : 0 < n₀ T a := by + have : (0 : ℝ) < n₀ T a := by linarith [hn₀_le T a, hT_large a, hLδ a] + exact_mod_cast this + have hn₀_L (a : α) : 4 * k * (L a : ℝ) < n₀ T a * δ := by + have h1 : 4 * k * (L a : ℝ) / δ < n₀ T a := by linarith [hn₀_le T a, hT_large a] + rwa [div_lt_iff₀ hδ] at h1 + -- The event on the rows: the mean of the first `n₀ T a` entries is within `δ / 2` of `x a`, and + -- the next `2 k` entries are within `L a` of `x a`. + set E : α → Set (ℕ → ℝ) := fun a ↦ {z | (∑ i ∈ range (n₀ T a), z i) / (n₀ T a : ℝ) ∈ + Metric.ball (x a) (δ / 2) ∧ ∀ j < 2 * k, z (n₀ T a + j) ∈ Metric.closedBall (x a) (L a)} + have hE (a : α) : MeasurableSet (E a) := by + have : E a = (fun z : ℕ → ℝ ↦ (∑ i ∈ range (n₀ T a), z i) / (n₀ T a : ℝ)) ⁻¹' + Metric.ball (x a) (δ / 2) ∩ ⋂ j ∈ Finset.range (2 * k), + (fun z : ℕ → ℝ ↦ z (n₀ T a + j)) ⁻¹' Metric.closedBall (x a) (L a) := by + ext z + simp [E] + rw [this] + exact ((by fun_prop : Measurable fun z : ℕ → ℝ ↦ (∑ i ∈ range (n₀ T a), z i) / (n₀ T a : ℝ)) + Metric.isOpen_ball.measurableSet).inter (Finset.measurableSet_biInter _ fun j _ ↦ + (measurable_pi_apply _) Metric.isClosed_closedBall.measurableSet) + -- On this event, the means after every number of samples in the window are within `δ` of `x`. + have h_sub : {ω : ℕ → α → ℝ | ∀ a, (fun i ↦ ω i a) ∈ E a} ⊆ + {ω | ∀ n : α → ℕ, (∀ a, |(n a : ℝ) - T * w a| ≤ k) → + (fun a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ∈ U} := by + intro ω hω n hn + refine hδU ?_ + rw [ball_pi _ hδ] + intro a _ + obtain ⟨d, hd, hnd⟩ := exists_eq_ceil_sub_add (hn a) + simp only [Metric.mem_ball, hnd] + exact dist_mean_lt (hn₀_pos a) (L a).cast_nonneg (hn₀_L a) (hω a).1 (hω a).2 hd + refine le_trans ?_ (measure_mono h_sub) + rw [streamMeasure_forall_row_mem ν hE] + simp only [E] + simp_rw [Measure.infinitePi_mean_mem_and_forall_mem _ _ _ Metric.isOpen_ball.measurableSet + Metric.isClosed_closedBall.measurableSet] + rw [Finset.prod_mul_distrib, mul_comm] + gcongr + refine hT.trans_eq ?_ + rw [Measure.pi_pi] + +end Stream + +/-! ### Transfer of the empirical means of a run to the stream -/ + +section Transfer + +variable [DecidableEq α] [MeasurableSingletonClass α] {Ω : Type*} + {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {R : ℕ → Ω → ℝ} {P : Measure Ω} + [IsProbabilityMeasure P] {alg : Algorithm Unit α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] + +/-- **Upper transfer of the empirical means of a run to the stream.** In a run of any algorithm +against the stochastic bandit `Environment.bandit ν`, if the numbers of pulls after `T` rounds lie +almost surely in a set `S`, the probability that the vector of the empirical means after `T` +rounds lies in `F` is at most the probability that for some `n ∈ S`, the vector of the empirical +means of the first `n a` entries of the rows of the reward stream lies in `F`. Neither `S` nor `F` +needs to be measurable: for non-measurable events, both sides are outer measures. -/ +theorem measure_empMean_mem_le_streamMeasure [Countable α] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) + (T : ℕ) {S : Set (α → ℕ)} (hS : ∀ᵐ ω ∂P, (fun a ↦ pullCount A a T ω) ∈ S) (F : Set (α → ℝ)) : + P {ω | (fun a ↦ empMean A R a T ω) ∈ F} ≤ + streamMeasure ν {y | ∃ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := by + calc P {ω | (fun a ↦ empMean A R a T ω) ∈ F} + _ ≤ P {ω | ∃ t, (fun a ↦ pullCount A a t ω) ∈ S ∧ + (fun a ↦ (∑ i, armObs A R a t ω i) / (pullCount A a t ω : ℝ)) ∈ F} := by + refine measure_mono_ae ?_ + filter_upwards [hS] with ω hω hF + exact ⟨T, hω, by simpa only [sum_armObs, empMean] using hF⟩ + _ ≤ streamMeasure ν {y | ∃ s : α → ℕ, s ∈ S ∧ + (fun a ↦ (∑ i : Fin (s a), y i a) / (s a : ℝ)) ∈ F} := + measure_exists_pullCount_armObs_pi_le h + fun s y ↦ s ∈ S ∧ (fun a ↦ (∑ i, y a i) / (s a : ℝ)) ∈ F + _ = streamMeasure ν {y | ∃ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := by + simp only [Finset.sum_range] + +/-- **Lower transfer of the empirical means of a run to the stream.** In a run of any algorithm +against the stochastic bandit `Environment.bandit ν`, if the numbers of pulls after `T` rounds lie +almost surely in a set `S`, the probability that the vector of the empirical means after `T` +rounds lies in a measurable set `U` is at least the probability that for all `n ∈ S`, the vector of +the empirical means of the first `n a` entries of the rows of the reward stream lies in `U`. -/ +theorem streamMeasure_le_measure_empMean_mem [Finite α] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) + (T : ℕ) {S : Set (α → ℕ)} (hS : ∀ᵐ ω ∂P, (fun a ↦ pullCount A a T ω) ∈ S) + {U : Set (α → ℝ)} (hU : MeasurableSet U) : + streamMeasure ν {y | ∀ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ U} ≤ + P {ω | (fun a ↦ empMean A R a T ω) ∈ U} := by + -- The rewards by count of the run, arranged as a reward stream, have the law of the stream. + have hZ := hasLaw_rewardByCount_streamMeasure h + have hG : MeasurableSet + {y : ℕ → α → ℝ | ∀ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ U} := by + simp_rw [Set.ofPred_forall] + exact MeasurableSet.iInter fun n ↦ MeasurableSet.iInter fun _ ↦ + (by fun_prop : Measurable fun y : ℕ → α → ℝ ↦ + fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) hU + rw [← hZ.map_eq, Measure.map_apply_of_aemeasurable hZ.aemeasurable hG, + ← one_mul (P _), ← measure_univ (μ := streamMeasure ν), ← Measure.prod_preimage_fst] + -- The empirical mean of arm `a` is the mean of its first `N_{T,a}` rewards by count. + refine measure_mono_ae ?_ + filter_upwards [Measure.quasiMeasurePreserving_fst.ae hS] with ω hω hG + simp only [Set.mem_preimage, Set.mem_ofPred_eq] at hG ⊢ + convert hG _ hω using 2 with a + rw [empMean, sumRewards_eq_sum_range_rewardByCount a T ω] + +end Transfer + +/-! ### Large deviations of the empirical means under static allocations -/ + +section LDP + +variable [Fintype α] [DecidableEq α] [MeasurableSingletonClass α] {Ω : Type*} + {mΩ : MeasurableSpace Ω} {O : ℕ → ℕ → Ω → Unit} {A : ℕ → ℕ → Ω → α} {R : ℕ → ℕ → Ω → ℝ} + {P : ℕ → Measure Ω} [∀ T, IsProbabilityMeasure (P T)] {alg : ℕ → Algorithm Unit α ℝ} + {ν : Kernel α ℝ} [IsMarkovKernel ν] {I : α → ℝ → ℝ≥0∞} {w : α → ℝ} + +/-- **Large deviations of the empirical means under static allocations** [GJ04; D23, Theorem 12]. +Let the laws of the empirical means of `m` independent samples of `ν a` satisfy the large deviation +principle with speed `1 / m` and a good rate function `I a`, and let `w a > 0`. For runs of +algorithms `alg T` against the bandit `ν` whose numbers of pulls after `T` rounds satisfy +`|N_{T,a} - T w a| ≤ k` almost surely, the laws of the vectors of the empirical means after `T` +rounds satisfy the large deviation principle with speed `1 / T` and rate function +`x ↦ ∑ a, w a I a (x a)`, a good rate function by `LMLExplore.isGoodRateFunction_sum_mul`. -/ +theorem hasLDP_empMean_of_abs_pullCount_sub_le + (hP : ∀ a, HasLDP atTop (fun m : ℕ ↦ (m : ℝ≥0)⁻¹) + (fun m ↦ (Measure.pi fun _ : Fin m ↦ ν a).map fun z : Fin m → ℝ ↦ (∑ i, z i) / (m : ℝ)) + (I a)) + (hI : ∀ a, IsGoodRateFunction (I a)) (hw : ∀ a, 0 < w a) (k : ℕ) + (h : ∀ T, IsAlgEnvSeq (O T) (A T) (R T) (alg T) (Environment.bandit ν) (P T)) + (h_pull : ∀ T, ∀ᵐ ω ∂(P T), ∀ a, |(pullCount (A T) a T ω : ℝ) - T * w a| ≤ k) : + HasLDP atTop (fun T : ℕ ↦ (T : ℝ≥0)⁻¹) + (fun T ↦ (P T).map fun ω a ↦ empMean (A T) (R T) a T ω) + (fun x ↦ ∑ a, ENNReal.ofReal (w a) * I a (x a)) := by + have hmeas (T : ℕ) : Measurable fun ω a ↦ empMean (A T) (R T) a T ω := + .of_eval fun a ↦ + measurable_empMean (h T).measurable_action (h T).measurable_feedback a T + have hS (T : ℕ) : ∀ᵐ ω ∂(P T), (fun a ↦ pullCount (A T) a T ω) ∈ + {n : α → ℕ | ∀ a, |(n a : ℝ) - T * w a| ≤ k} := h_pull T + refine .of_isClosed_of_mem_nhds (isGoodRateFunction_sum_mul hI hw).lowerSemicontinuous + (fun F hF ↦ ?_) (fun x U hU ↦ ?_) + · -- Every number of pulls in the window is `n₀ + d` for `n₀ a = ⌈T w a - k⌉₊` and some + -- `d : α → Fin (2 k + 1)`, a number within `2 k + 1` of `T w a`. + refine limsup_inv_mul_log_le_neg_of_le_mul_exp fun r hr ↦ + ⟨Fintype.card (α → Fin (2 * k + 1)), ENNReal.natCast_ne_top _, ?_⟩ + filter_upwards [eventually_streamMeasure_mean_mem_le_exp hP hI hw (2 * k + 1) hF hr] + with T hT + set n₀ : α → ℕ := fun a ↦ ⌈T * w a - k⌉₊ + rw [Measure.map_apply (hmeas T) hF.measurableSet] + calc (P T) ((fun ω a ↦ empMean (A T) (R T) a T ω) ⁻¹' F) + _ ≤ streamMeasure ν {y | ∃ n ∈ {n : α → ℕ | ∀ a, |(n a : ℝ) - T * w a| ≤ k}, + (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := + measure_empMean_mem_le_streamMeasure (h T) T (hS T) F + _ ≤ streamMeasure ν (⋃ d : α → Fin (2 * k + 1), {y | (fun a ↦ + (∑ i ∈ range (n₀ a + d a), y i a) / ((n₀ a + d a : ℕ) : ℝ)) ∈ F}) := by + refine measure_mono fun y ⟨n, hn, hnF⟩ ↦ Set.mem_iUnion.2 ?_ + choose d hd hnd using fun a ↦ exists_eq_ceil_sub_add (hn a) + refine ⟨fun a ↦ ⟨d a, Nat.lt_succ_of_le (hd a)⟩, ?_⟩ + obtain rfl : n = fun a ↦ n₀ a + d a := funext hnd + exact hnF + _ ≤ ∑ d : α → Fin (2 * k + 1), streamMeasure ν {y | (fun a ↦ + (∑ i ∈ range (n₀ a + d a), y i a) / ((n₀ a + d a : ℕ) : ℝ)) ∈ F} := + measure_iUnion_fintype_le _ _ + _ ≤ ∑ _d : α → Fin (2 * k + 1), ENNReal.ofReal (Real.exp (-(T * r))) := + Finset.sum_le_sum fun d _ ↦ hT (fun a ↦ n₀ a + d a) fun a ↦ + abs_ceil_sub_add_sub_le (mul_nonneg T.cast_nonneg (hw a).le) (Nat.lt_succ_iff.1 (d a).2) + _ = Fintype.card (α → Fin (2 * k + 1)) * ENNReal.ofReal (Real.exp (-(T * r))) := by + rw [Finset.sum_const, nsmul_eq_mul, Finset.card_univ] + · -- The means of the stream are in the interior of `U` for all the numbers of pulls in the + -- window with probability at least `C exp (-(T r))`. + refine neg_le_liminf_inv_mul_log_of_mul_exp_le fun r hr ↦ ?_ + obtain ⟨C, hC, hev⟩ := exists_eventually_le_streamMeasure_forall_mean_mem hP hw k + (interior_mem_nhds.2 hU) hr + refine ⟨C, hC, hev.mono fun T hT ↦ hT.trans ?_⟩ + calc streamMeasure ν {y | ∀ n : α → ℕ, (∀ a, |(n a : ℝ) - T * w a| ≤ k) → + (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ interior U} + _ ≤ (P T) {ω | (fun a ↦ empMean (A T) (R T) a T ω) ∈ interior U} := + streamMeasure_le_measure_empMean_mem (h T) T (hS T) isOpen_interior.measurableSet + _ ≤ (P T).map (fun ω a ↦ empMean (A T) (R T) a T ω) U := + (Measure.map_apply (hmeas T) isOpen_interior.measurableSet).symm.trans_le + (measure_mono interior_subset) + +/-- **Cramér's theorem under static allocations** [GJ04; D23, Theorem 12]. If the cumulant +generating function of each arm `ν a` is finite on a neighbourhood of `0`, `w a > 0`, and the +numbers of pulls after `T` rounds of runs of algorithms `alg T` against the bandit `ν` satisfy +`|N_{T,a} - T w a| ≤ k` almost surely, then the laws of the vectors of the empirical means after +`T` rounds satisfy the large deviation principle with speed `1 / T` and rate function +`x ↦ ∑ a, w a I_a(x a)`, with `I_a` the Cramér rate function of `ν a`. This rate function is +good, by `LMLExplore.isGoodRateFunction_sum_mul` and `LMLExplore.isGoodRateFunction_rateFunction`. +-/ +theorem hasLDP_empMean_rateFunction_of_abs_pullCount_sub_le + (hν : ∀ a, 0 ∈ interior (integrableExpSet id (ν a))) (hw : ∀ a, 0 < w a) (k : ℕ) + (h : ∀ T, IsAlgEnvSeq (O T) (A T) (R T) (alg T) (Environment.bandit ν) (P T)) + (h_pull : ∀ T, ∀ᵐ ω ∂(P T), ∀ a, |(pullCount (A T) a T ω : ℝ) - T * w a| ≤ k) : + HasLDP atTop (fun T : ℕ ↦ (T : ℝ≥0)⁻¹) + (fun T ↦ (P T).map fun ω a ↦ empMean (A T) (R T) a T ω) + (fun x ↦ ∑ a, ENNReal.ofReal (w a) * rateFunction id (ν a) (x a)) := + hasLDP_empMean_of_abs_pullCount_sub_le + (fun a ↦ hasLDP_cramer (integrable_of_mem_interior_integrableExpSet (hν a))) + (fun a ↦ isGoodRateFunction_rateFunction (hν a)) hw k h h_pull + +end LDP + +end LMLExplore diff --git a/LMLExplore/SequentialLearning/SumRewards.lean b/LMLExplore/SequentialLearning/SumRewards.lean index cfbff7e9..714ce12b 100644 --- a/LMLExplore/SequentialLearning/SumRewards.lean +++ b/LMLExplore/SequentialLearning/SumRewards.lean @@ -56,13 +56,14 @@ this way. * `hasLaw_rewardByCount_streamMeasure`: the rewards by count of all arms, arranged as a reward stream, have the law `streamMeasure ν` of the stream model. * `hasLaw_arm_streamMeasure`: in the stream model, the array of the reward sequences of the arms - has law `⨂ a, ⨂ i, ν a`, and `iIndepFun_arm_streamMeasure`: these sequences are independent. + has law `⨂ a, ⨂ i, ν a`, and `iIndepFun_arm_streamMeasure`: these sequences are independent; + `streamMeasure_forall_row_mem` is the product formula for events about them. * `hasLaw_arm_fin_streamMeasure`: in the stream model, the first `n` rewards of an arm `a` are `n` independent samples of `ν a`, and `hasLaw_pi_arm_fin_streamMeasure`: for finitely many arms, the first `n a` rewards of the arms `a` are independent across the arms. -* `streamMeasure_forall_mean_mem`: in the stream model, the empirical means of the first `n a` - rewards of the arms `a` are independent, with the laws of the empirical means of `n a` - independent samples of `ν a`. +* `streamMeasure_map_mean`: in the stream model, the vector of the empirical means of the first + `n a` rewards of the arms `a` has independent coordinates, with the laws of the empirical means + of `n a` independent samples of `ν a`; `streamMeasure_forall_mean_mem` is its form for boxes. * `armObs`: the observations of an arm before a round, in the order of the pulls; `armObs_eq_rewardByCount` relates them to LML's rewards by count, and `sum_armObs` to the sum of rewards. @@ -325,6 +326,21 @@ theorem iIndepFun_arm_streamMeasure {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : ext a : 1 rw [← (hasLaw_eval_infinitePi _ a).comp h_arms |>.map_eq, Function.comp_def] +omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in +/-- **Independence of the rows of the reward stream.** For finitely many arms, events about the +reward sequences `(ω i a)_i` of different arms `a` in LML's reward stream model are independent, +and the reward sequence of `a` is an i.i.d. sequence of law `ν a`. -/ +theorem streamMeasure_forall_row_mem [Fintype α] {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : Kernel α 𝓡) + [IsMarkovKernel ν] {E : α → Set (ℕ → 𝓡)} (hE : ∀ a, MeasurableSet (E a)) : + streamMeasure ν {ω | ∀ a, (fun i ↦ ω i a) ∈ E a} = + ∏ a, (Measure.infinitePi fun _ : ℕ ↦ ν a) (E a) := by + have h_set : {ω : ℕ → α → 𝓡 | ∀ a, (fun i ↦ ω i a) ∈ E a} = + (fun ω a i ↦ ω i a) ⁻¹' ((Finset.univ : Finset α) : Set α).pi E := by + ext ω + simp + rw [h_set, ← Measure.map_apply (by fun_prop) (.pi (Finset.univ : Finset α).countable_toSet + fun a _ ↦ hE a), (hasLaw_arm_streamMeasure ν).map_eq, Measure.infinitePi_pi _ fun a _ ↦ hE a] + omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in /-- In LML's reward stream model, the first `n` rewards `(ω i a)_{i < n}` of arm `a` are `n` independent samples of `ν a`. -/ @@ -349,6 +365,22 @@ theorem hasLaw_pi_arm_fin_streamMeasure [Fintype α] {𝓡 : Type*} [MeasurableS ((iIndepFun_arm_streamMeasure ν).comp (fun a (z : ℕ → 𝓡) (i : Fin (n a)) ↦ z i) fun _ ↦ by fun_prop).hasLaw_pi fun a ↦ hasLaw_arm_fin_streamMeasure ν a (n a) +omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in +/-- **The law of the empirical means in the stream model.** For finitely many arms and numbers of +samples `n a`, the vector of the empirical means of the first `n a` rewards of the arms `a` in +LML's reward stream model has independent coordinates, the one of arm `a` with the law of the +empirical mean of `n a` independent samples of `ν a`. -/ +theorem streamMeasure_map_mean [Fintype α] (n : α → ℕ) : + (streamMeasure ν).map (fun ω a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) = + Measure.pi fun a ↦ (Measure.pi fun _ : Fin (n a) ↦ ν a).map + fun z : Fin (n a) → ℝ ↦ (∑ i, z i) / (n a : ℝ) := by + rw [← Measure.pi_map_pi fun a ↦ (by fun_prop : Measurable fun z : Fin (n a) → ℝ ↦ + (∑ i, z i) / n a).aemeasurable, ← (hasLaw_pi_arm_fin_streamMeasure ν n).map_eq, + Measure.map_map (by fun_prop) (by fun_prop)] + congr 1 + ext ω a + exact congrArg (· / (n a : ℝ)) (Fin.sum_univ_eq_sum_range (fun i ↦ ω i a) (n a)).symm + omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in /-- **Independence of the empirical means across the arms in the stream model.** For finitely many arms and numbers of samples `n a`, the empirical means of the first `n a` rewards of the arms `a` @@ -359,18 +391,13 @@ theorem streamMeasure_forall_mean_mem [Fintype α] (n : α → ℕ) {B : α → streamMeasure ν {ω | ∀ a, (∑ i ∈ range (n a), ω i a) / n a ∈ B a} = ∏ a, (Measure.pi fun _ : Fin (n a) ↦ ν a).map (fun z : Fin (n a) → ℝ ↦ (∑ i, z i) / n a) (B a) := by - have hmean (a : α) : Measurable fun z : Fin (n a) → ℝ ↦ (∑ i, z i) / n a := by fun_prop - have hX := hasLaw_pi_arm_fin_streamMeasure ν n - -- the event is a box for the first `n a` rewards of the arms + -- the event is the preimage of a box under the vector of the empirical means have h_set : {ω : ℕ → α → ℝ | ∀ a, (∑ i ∈ range (n a), ω i a) / n a ∈ B a} = - (fun ω a (i : Fin (n a)) ↦ ω i a) ⁻¹' - Set.univ.pi fun a ↦ (fun z : Fin (n a) → ℝ ↦ (∑ i, z i) / n a) ⁻¹' B a := by + (fun ω a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ⁻¹' Set.univ.pi B := by ext ω - simp only [Set.mem_ofPred_eq, Set.mem_preimage, Set.mem_univ_pi] - exact forall_congr' fun a ↦ by rw [Fin.sum_univ_eq_sum_range (fun i ↦ ω i a)] - rw [h_set, ← Measure.map_apply (by fun_prop) (.univ_pi fun a ↦ hmean a (hB a)), hX.map_eq, + simp + rw [h_set, ← Measure.map_apply (by fun_prop) (.univ_pi hB), streamMeasure_map_mean, Measure.pi_pi] - exact prod_congr rfl fun a _ ↦ (Measure.map_apply (hmean a) (hB a)).symm /-- **Counting transfer of the observations to the reward stream, weighted form.** In a run of any algorithm against the stochastic bandit `Environment.bandit ν`, for measurable functions From 52b71a5f32a3a80fba42fa5544e90b6cb8df7a19 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 17:11:55 +0100 Subject: [PATCH 2/7] refactor: address review of the static-allocation LDP MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - reuse measure_exists_pullCount_sumRewards_pi_le in the upper transfer - state the i.i.d. split lemma for a general space and a set of Fin n → X - make the convergence lemma public in Analysis/SpecificLimits/Basic - add measurable_empMean_pi and use it at the three call sites Co-Authored-By: Claude Code --- LMLExplore/Analysis/SpecificLimits/Basic.lean | 44 +++++++++ .../Identification/StaticProportions.lean | 12 +-- .../SequentialLearning/StaticAllocation.lean | 99 ++++++++----------- LMLExplore/SequentialLearning/SumRewards.lean | 7 ++ 4 files changed, 100 insertions(+), 62 deletions(-) create mode 100644 LMLExplore/Analysis/SpecificLimits/Basic.lean diff --git a/LMLExplore/Analysis/SpecificLimits/Basic.lean b/LMLExplore/Analysis/SpecificLimits/Basic.lean new file mode 100644 index 00000000..1ac5d475 --- /dev/null +++ b/LMLExplore/Analysis/SpecificLimits/Basic.lean @@ -0,0 +1,44 @@ +/- +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.Normed.Group.Continuity +public import Mathlib.Analysis.Normed.Group.Real +public import Mathlib.Analysis.SpecificLimits.Basic + +/-! +# Limits of ratios to `n` of sequences within bounded distance of a linear sequence + +A real sequence `u` that stays within a fixed distance `c` of the linear sequence `n ↦ n w` +satisfies `u n / n → w`. Numbers of pulls of bandit algorithms that track static proportions `w` +up to a bounded error have this form. + +## Main statements + +* `LMLExplore.tendsto_div_natCast_of_abs_sub_mul_le`: if `|u n - n w| ≤ c` for every `n`, then + `u n / n → w`. +-/ + +public section + +open Filter Topology + +namespace LMLExplore + +/-- If `|u n - n w| ≤ c` for every `n`, then `u n / n → w`. -/ +theorem tendsto_div_natCast_of_abs_sub_mul_le {u : ℕ → ℝ} {w c : ℝ} + (h : ∀ n : ℕ, |u n - n * w| ≤ c) : Tendsto (fun n : ℕ ↦ u n / n) atTop (𝓝 w) := by + have h0 : Tendsto (fun n : ℕ ↦ (u n - n * w) / n) atTop (𝓝 0) := by + refine squeeze_zero_norm (fun n ↦ ?_) (tendsto_const_div_atTop_nhds_zero_nat c) + rw [Real.norm_eq_abs, abs_div, Nat.abs_cast] + exact div_le_div_of_nonneg_right (h n) n.cast_nonneg + have h1 : Tendsto (fun n : ℕ ↦ (u n - n * w) / n + w) atTop (𝓝 w) := by + simpa using h0.add_const w + refine h1.congr' ?_ + filter_upwards [eventually_ne_atTop 0] with n hn + rw [sub_div, mul_div_cancel_left₀ _ (Nat.cast_ne_zero.2 hn), sub_add_cancel] + +end LMLExplore diff --git a/LMLExplore/Identification/StaticProportions.lean b/LMLExplore/Identification/StaticProportions.lean index 85f45383..10af0aa3 100644 --- a/LMLExplore/Identification/StaticProportions.lean +++ b/LMLExplore/Identification/StaticProportions.lean @@ -302,11 +302,11 @@ theorem IsStaticProportions.limsup_log_errorProb_div_le (h𝒜 : task.IsStaticPr simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h refine le_trans (limsup_le_limsup (Eventually.of_forall fun T ↦ ?_)) h -- The error is the event that the empirical means lie in the set where `rec` is not correct. - have hmeas : Measurable fun (h : ℕ → Round Unit α ℝ) a ↦ empMean IT.action IT.feedback a T h := - .of_eval fun a ↦ measurable_empMean IT.measurable_action IT.measurable_feedback a T rw [h𝒜.errorProb_eq hcorrect] exact EReal.div_le_div_right_of_nonneg (by positivity) (ENNReal.log_monotone - (Measure.le_map_apply hmeas.aemeasurable {x | rec x ∉ task.correct θ})) + (Measure.le_map_apply + (measurable_empMean_pi IT.measurable_action IT.measurable_feedback T).aemeasurable + {x | rec x ∉ task.correct θ})) /-- **Lower bound on the error exponent of a static proportions family** [GJ04; D23, Theorem 12]. If the set of correct answers of the admissible model `θ` is measurable and the cumulant generating @@ -327,9 +327,9 @@ theorem IsStaticProportions.neg_le_liminf_log_errorProb_div simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h refine h.trans (liminf_le_liminf (Eventually.of_forall fun T ↦ ?_)) -- The empirical means in the interior of the set where `rec` is not correct give an error. - have hmeas : Measurable fun (h : ℕ → Round Unit α ℝ) a ↦ empMean IT.action IT.feedback a T h := - .of_eval fun a ↦ measurable_empMean IT.measurable_action IT.measurable_feedback a T - rw [h𝒜.errorProb_eq hcorrect, Measure.map_apply hmeas isOpen_interior.measurableSet] + rw [h𝒜.errorProb_eq hcorrect, Measure.map_apply + (measurable_empMean_pi IT.measurable_action IT.measurable_feedback T) + isOpen_interior.measurableSet] exact EReal.div_le_div_right_of_nonneg (by positivity) (ENNReal.log_monotone (measure_mono (Set.preimage_mono interior_subset))) diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index cb941714..9785bae7 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -5,6 +5,7 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.Analysis.SpecificLimits.Basic public import LMLExplore.Probability.LargeDeviations.Pi public import LMLExplore.SequentialLearning.SumRewards @@ -38,8 +39,8 @@ after `T` rounds is the mean of the first `N_{T,a}` entries of its row ## Main statements -* `MeasureTheory.Measure.infinitePi_mean_mem_and_forall_mem`: for an i.i.d. sequence, the mean of - the first `n` terms and the next `m` terms are independent. +* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the + first `n` terms and the next `m` terms are independent. * `LMLExplore.eventually_streamMeasure_mean_mem_le_exp`, `LMLExplore.exists_eventually_le_streamMeasure_forall_mean_mem`: the exponential upper and lower bounds for the empirical means of the rows, uniformly over the numbers of samples in a window. @@ -78,43 +79,38 @@ open scoped ENNReal NNReal namespace MeasureTheory.Measure -/-- **The mean of the first terms of an i.i.d. sequence and the next terms are independent.** For -an i.i.d. sequence of law `μ`, the mean of the first `n` terms lies in `B` and the next `m` terms -lie in `C` with probability `P(μ̂_n ∈ B) μ(C)^m`, where `μ̂_n` is the mean of `n` independent -samples of `μ`. -/ -theorem infinitePi_mean_mem_and_forall_mem (μ : Measure ℝ) [IsProbabilityMeasure μ] (n m : ℕ) - {B C : Set ℝ} (hB : MeasurableSet B) (hC : MeasurableSet C) : - (Measure.infinitePi fun _ : ℕ ↦ μ) - {z | (∑ i ∈ range n, z i) / (n : ℝ) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - ((Measure.pi fun _ : Fin n ↦ μ).map fun y ↦ (∑ i, y i) / (n : ℝ)) B * μ C ^ m := by +/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. +sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie +in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ +theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) + [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) + (hC : MeasurableSet C) : + (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by -- The first `n` terms and the next `m` terms are independent. have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) simp only [id] at h_ind - have h_mean : Measurable fun u : {i // i ∈ range n} → ℝ ↦ (∑ i, u i) / (n : ℝ) := by fun_prop - have h_set : {z : ℕ → ℝ | (∑ i ∈ range n, z i) / (n : ℝ) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - (fun z (i : range n) ↦ z i) ⁻¹' ((fun u ↦ (∑ i, u i) / (n : ℝ)) ⁻¹' B) ∩ + have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ + u ⟨i, mem_range.2 i.2⟩ := by fun_prop + have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by ext z simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, Set.mem_univ, true_implies, Subtype.forall, mem_Ico] - refine and_congr ?_ ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ - · rw [Finset.sum_coe_sort (range n) z] - · obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 - exact h j (by omega) - rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_mean hB) (.univ_pi fun _ ↦ hC)] + refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ + obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 + exact h j (by omega) + rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] congr 1 · -- The first `n` terms are `n` independent samples of `μ`. - have h_fin : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = + have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = Measure.pi fun _ : Fin n ↦ μ := by rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] - rw [← h_fin, Measure.map_map (by fun_prop) (by fun_prop), - Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] - congr 1 - ext z - simp only [Set.mem_preimage, Function.comp_apply] - rw [Finset.sum_coe_sort (range n) z, Fin.sum_univ_eq_sum_range (fun i ↦ z i)] + rw [← h_pi, Measure.map_apply (by fun_prop) hB] + rfl · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by ext z @@ -134,19 +130,6 @@ section Stream variable [Fintype α] {ν : Kernel α ℝ} [IsMarkovKernel ν] {I : α → ℝ → ℝ≥0∞} {w : α → ℝ} -/-- If `|m T - T w| ≤ c` for every `T`, then `m T / T → w`. -/ -private lemma tendsto_div_of_abs_sub_le {m : ℕ → ℕ} {w c : ℝ} (h : ∀ T, |(m T : ℝ) - T * w| ≤ c) : - Tendsto (fun T ↦ (m T : ℝ) / T) atTop (𝓝 w) := by - have h0 : Tendsto (fun T : ℕ ↦ ((m T : ℝ) - T * w) / T) atTop (𝓝 0) := by - refine squeeze_zero_norm (fun T ↦ ?_) (tendsto_const_div_atTop_nhds_zero_nat c) - rw [norm_div, Real.norm_eq_abs, Real.norm_eq_abs, Nat.abs_cast] - exact div_le_div_of_nonneg_right (h T) T.cast_nonneg - have h1 : Tendsto (fun T : ℕ ↦ ((m T : ℝ) - T * w) / T + w) atTop (𝓝 w) := by - simpa using h0.add_const w - refine h1.congr' ?_ - filter_upwards [eventually_ne_atTop 0] with T hT - rw [sub_div, mul_div_cancel_left₀ _ (Nat.cast_ne_zero.2 hT), sub_add_cancel] - /-- **The exponential upper bound for the rows of the reward stream, uniformly in a window.** Let the laws of the empirical means of `m` independent samples of `ν a` satisfy the large deviation principle with speed `1 / m` and a good rate function `I a`, and let `w a > 0`. For a closed set @@ -179,7 +162,7 @@ theorem eventually_streamMeasure_mean_mem_le_exp rw [abs_of_nonneg (sub_nonneg.2 (Nat.le_ceil _))] linarith [Nat.ceil_lt_add_one h0, le_max_right c 1] have hLDP := hasLDP_pi_comp_of_tendsto_div hP hI (m := fun a T ↦ m T a) hw - fun a ↦ tendsto_div_of_abs_sub_le fun T ↦ hm_abs T a + fun a ↦ tendsto_div_natCast_of_abs_sub_mul_le fun T ↦ hm_abs T a filter_upwards [hLDP.eventually_measure_le_exp hF hr] with T hT n hn by_contra hlt have h : ∃ n, B T n := ⟨n, hn, not_le.1 hlt⟩ @@ -291,7 +274,7 @@ theorem exists_eventually_le_streamMeasure_forall_mean_mem set V : Set (α → ℝ) := Set.univ.pi fun a ↦ Metric.ball (x a) (δ / 2) have h_box := eventually_exp_le_of_neg_le_liminf_inv_mul_log (neg_sum_le_liminf_log_pi (fun a ↦ (hP a).comp_of_tendsto_div (hw a) - (tendsto_div_of_abs_sub_le fun T ↦ hn₀_abs T a)) + (tendsto_div_natCast_of_abs_sub_mul_le fun T ↦ hn₀_abs T a)) (x := x) (s := V) (set_pi_mem_nhds Set.finite_univ fun a _ ↦ Metric.ball_mem_nhds (x a) (half_pos hδ))) hr refine ⟨∏ a, ν a (Metric.closedBall (x a) (L a)) ^ (2 * k), @@ -331,11 +314,20 @@ theorem exists_eventually_le_streamMeasure_forall_mean_mem simp only [Metric.mem_ball, hnd] exact dist_mean_lt (hn₀_pos a) (L a).cast_nonneg (hn₀_L a) (hω a).1 (hω a).2 hd refine le_trans ?_ (measure_mono h_sub) - rw [streamMeasure_forall_row_mem ν hE] - simp only [E] - simp_rw [Measure.infinitePi_mean_mem_and_forall_mem _ _ _ Metric.isOpen_ball.measurableSet - Metric.isClosed_closedBall.measurableSet] - rw [Finset.prod_mul_distrib, mul_comm] + -- The event on each row splits into an event on its first `n₀ T a` entries and on the next ones. + have hE_eq (a : α) : (Measure.infinitePi fun _ : ℕ ↦ ν a) (E a) = + ((Measure.pi fun _ : Fin (n₀ T a) ↦ ν a).map fun y ↦ (∑ i, y i) / (n₀ T a : ℝ)) + (Metric.ball (x a) (δ / 2)) * ν a (Metric.closedBall (x a) (L a)) ^ (2 * k) := by + rw [Measure.map_apply (by fun_prop) Metric.isOpen_ball.measurableSet, + ← Measure.infinitePi_fin_mem_and_forall_add_mem _ _ _ + ((by fun_prop : Measurable fun y : Fin (n₀ T a) → ℝ ↦ (∑ i, y i) / (n₀ T a : ℝ)) + Metric.isOpen_ball.measurableSet) Metric.isClosed_closedBall.measurableSet] + congr 1 + ext z + simp only [E, Set.mem_ofPred_eq, Set.mem_preimage, + Fin.sum_univ_eq_sum_range (fun i ↦ z i)] + rw [streamMeasure_forall_row_mem ν hE, Finset.prod_congr rfl fun a _ ↦ hE_eq a, + Finset.prod_mul_distrib, mul_comm] gcongr refine hT.trans_eq ?_ rw [Measure.pi_pi] @@ -363,16 +355,12 @@ theorem measure_empMean_mem_le_streamMeasure [Countable α] streamMeasure ν {y | ∃ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := by calc P {ω | (fun a ↦ empMean A R a T ω) ∈ F} _ ≤ P {ω | ∃ t, (fun a ↦ pullCount A a t ω) ∈ S ∧ - (fun a ↦ (∑ i, armObs A R a t ω i) / (pullCount A a t ω : ℝ)) ∈ F} := by + (fun a ↦ sumRewards A R a t ω / (pullCount A a t ω : ℝ)) ∈ F} := by refine measure_mono_ae ?_ filter_upwards [hS] with ω hω hF - exact ⟨T, hω, by simpa only [sum_armObs, empMean] using hF⟩ - _ ≤ streamMeasure ν {y | ∃ s : α → ℕ, s ∈ S ∧ - (fun a ↦ (∑ i : Fin (s a), y i a) / (s a : ℝ)) ∈ F} := - measure_exists_pullCount_armObs_pi_le h - fun s y ↦ s ∈ S ∧ (fun a ↦ (∑ i, y a i) / (s a : ℝ)) ∈ F - _ = streamMeasure ν {y | ∃ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := by - simp only [Finset.sum_range] + exact ⟨T, hω, by simpa only [empMean] using hF⟩ + _ ≤ streamMeasure ν {y | ∃ n ∈ S, (fun a ↦ (∑ i ∈ range (n a), y i a) / (n a : ℝ)) ∈ F} := + measure_exists_pullCount_sumRewards_pi_le h fun s y ↦ s ∈ S ∧ (fun a ↦ y a / (s a : ℝ)) ∈ F /-- **Lower transfer of the empirical means of a run to the stream.** In a run of any algorithm against the stochastic bandit `Environment.bandit ν`, if the numbers of pulls after `T` rounds lie @@ -431,8 +419,7 @@ theorem hasLDP_empMean_of_abs_pullCount_sub_le (fun T ↦ (P T).map fun ω a ↦ empMean (A T) (R T) a T ω) (fun x ↦ ∑ a, ENNReal.ofReal (w a) * I a (x a)) := by have hmeas (T : ℕ) : Measurable fun ω a ↦ empMean (A T) (R T) a T ω := - .of_eval fun a ↦ - measurable_empMean (h T).measurable_action (h T).measurable_feedback a T + measurable_empMean_pi (h T).measurable_action (h T).measurable_feedback T have hS (T : ℕ) : ∀ᵐ ω ∂(P T), (fun a ↦ pullCount (A T) a T ω) ∈ {n : α → ℕ | ∀ a, |(n a : ℝ) - T * w a| ≤ k} := h_pull T refine .of_isClosed_of_mem_nhds (isGoodRateFunction_sum_mul hI hw).lowerSemicontinuous diff --git a/LMLExplore/SequentialLearning/SumRewards.lean b/LMLExplore/SequentialLearning/SumRewards.lean index 714ce12b..0bab8cc5 100644 --- a/LMLExplore/SequentialLearning/SumRewards.lean +++ b/LMLExplore/SequentialLearning/SumRewards.lean @@ -84,6 +84,7 @@ this way. `measure_exists_pullCount_sumRewards_le` and `measure_exists_lt_pullCount_sumRewards_le`: the event transfers for properties of the numbers of pulls and the sums of rewards. * `empMean_mem_Icc`: rewards in `[l, u]` give empirical means in `[l, u]`. +* `measurable_empMean_pi`: the vector of the empirical means of all arms is measurable. * `sum_ite_mul_add_one_sub_mul`: the sum over the pulls of an arm of an affine function `R x + (1 - R) y` of the reward is `S x + (N - S) y`, with `S` the sum of the rewards and `N` the number of pulls. @@ -194,6 +195,12 @@ lemma empMean_mem_Icc {a : α} {t : ℕ} {ω : Ω} {l u : ℝ} (hR : ∀ s < t, · simpa [pullCount, mul_comm] using card_nsmul_le_sum _ (fun s ↦ R s ω) l fun s hs ↦ (hR' s hs).1 · simpa [pullCount, mul_comm] using sum_le_card_nsmul _ (fun s ↦ R s ω) u fun s hs ↦ (hR' s hs).2 +/-- The vector `(empMean A R a t ω)_a` of the empirical means of all arms before round `t` is +measurable in `ω`. -/ +lemma measurable_empMean_pi [MeasurableSingletonClass α] (hA : ∀ n, Measurable (A n)) + (hR : ∀ n, Measurable (R n)) (t : ℕ) : Measurable fun ω a ↦ empMean A R a t ω := + .of_eval fun a ↦ measurable_empMean hA hR a t + /-- The sum over the pulls of an arm `a` of a function `R x + (1 - R) y` of the reward `R`, which is affine in the reward, is `S_a(n) x + (N_a(n) - S_a(n)) y`, where `S_a(n)` is the sum of the rewards of `a` and `N_a(n)` its number of pulls. For Bernoulli rewards and `x = log (q / p)`, From 4a91366dbd216615d2ec2045a0546ba0e45e8332 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 17:57:18 +0100 Subject: [PATCH 3/7] refactor: move infinitePi_fin_mem_and_forall_add_mem to MeasureTheory/Constructions/Pi Co-Authored-By: Claude Code --- .../MeasureTheory/Constructions/Pi.lean | 46 +++++++++++++++++++ .../SequentialLearning/StaticAllocation.lean | 46 +------------------ 2 files changed, 47 insertions(+), 45 deletions(-) diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index cc275003..e397208b 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.Probability.ConditionalProbability +public import Mathlib.Probability.Independence.InfinitePi import TauCeti.MeasureTheory.Constructions.Pi /-! @@ -24,6 +25,9 @@ Under a product of probability measures, a measurable set whose lines along one all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate `i` and integrating the measures of the lines. +Under the infinite product `Measure.infinitePi` of copies of `μ`, the first `n` coordinates and +the next `m` coordinates are independent. + ## Main statements * `MeasureTheory.Measure.map_pi_comp_eq_map_pi_map`: @@ -35,6 +39,8 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of probability measures, a measurable set whose lines `{t | update x i t ∈ E}` along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`. +* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the + first `n` terms and the next `m` terms are independent. -/ public section @@ -96,4 +102,44 @@ lemma pi_le_of_forall_measure_update_preimage_le [DecidableEq ι] {μ : ∀ i, M Measure.prod_apply (measurable_update' hE)] exact (lintegral_mono fun x ↦ h x).trans_eq (by simp) +open ProbabilityTheory Finset in +/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. +sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie +in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ +theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) + [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) + (hC : MeasurableSet C) : + (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by + -- The first `n` terms and the next `m` terms are independent. + have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) + (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) + (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) + simp only [id] at h_ind + have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ + u ⟨i, mem_range.2 i.2⟩ := by fun_prop + have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ + (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by + ext z + simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, + Set.mem_univ, true_implies, Subtype.forall, mem_Ico] + refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ + obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 + exact h j (by omega) + rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] + congr 1 + · -- The first `n` terms are `n` independent samples of `μ`. + have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = + Measure.pi fun _ : Fin n ↦ μ := by + rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] + rw [← h_pi, Measure.map_apply (by fun_prop) hB] + rfl + · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = + ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by + ext z + simp + rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, + Nat.add_sub_cancel_left] + end MeasureTheory.Measure diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index 9785bae7..6c383b8c 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -6,6 +6,7 @@ Authors: LMLExplore contributors module public import LMLExplore.Analysis.SpecificLimits.Basic +public import LMLExplore.MeasureTheory.Constructions.Pi public import LMLExplore.Probability.LargeDeviations.Pi public import LMLExplore.SequentialLearning.SumRewards @@ -39,8 +40,6 @@ after `T` rounds is the mean of the first `N_{T,a}` entries of its row ## Main statements -* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the - first `n` terms and the next `m` terms are independent. * `LMLExplore.eventually_streamMeasure_mean_mem_le_exp`, `LMLExplore.exists_eventually_le_streamMeasure_forall_mean_mem`: the exponential upper and lower bounds for the empirical means of the rows, uniformly over the numbers of samples in a window. @@ -77,49 +76,6 @@ open TauCeti.Probability (HasLDP IsGoodRateFunction) open scoped ENNReal NNReal -namespace MeasureTheory.Measure - -/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. -sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie -in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ -theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) - [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) - (hC : MeasurableSet C) : - (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by - -- The first `n` terms and the next `m` terms are independent. - have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) - (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) - (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) - simp only [id] at h_ind - have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ - u ⟨i, mem_range.2 i.2⟩ := by fun_prop - have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ - (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by - ext z - simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, - Set.mem_univ, true_implies, Subtype.forall, mem_Ico] - refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ - obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 - exact h j (by omega) - rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] - congr 1 - · -- The first `n` terms are `n` independent samples of `μ`. - have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = - Measure.pi fun _ : Fin n ↦ μ := by - rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] - rw [← h_pi, Measure.map_apply (by fun_prop) hB] - rfl - · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = - ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by - ext z - simp - rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, - Nat.add_sub_cancel_left] - -end MeasureTheory.Measure - namespace LMLExplore variable {α : Type*} {mα : MeasurableSpace α} From ef40cba2417d4e330dd4c798a8980d6be8c6155b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:22:56 +0100 Subject: [PATCH 4/7] refactor: make the defeq step in infinitePi_fin_mem_and_forall_add_mem explicit Rewrite with Set.preimage_comp before the closing rfl and explain why the remaining equality holds definitionally. Co-Authored-By: Claude Code --- LMLExplore/MeasureTheory/Constructions/Pi.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index e397208b..ca13ea31 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -133,7 +133,10 @@ theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] ( have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = Measure.pi fun _ : Fin n ↦ μ := by rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] - rw [← h_pi, Measure.map_apply (by fun_prop) hB] + rw [← h_pi, Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] + -- Both sides are the preimage of `B` under `z ↦ (z i)_{i : Fin n}`: the composite + -- `(fun u i ↦ u ⟨i, _⟩) ∘ (fun z i ↦ z i)` unfolds to `fun z i ↦ z ↑⟨i, _⟩`, and + -- `↑⟨i, _⟩ = i` is `Subtype.val` applied to a constructor. rfl · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by From ed5fbcb55b112e36b8592cf5ff8f8411a88670a5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:48:39 +0100 Subject: [PATCH 5/7] refactor: cite exists_pos_measure_of_cover and clarify neg_sum_le_liminf_log_pi docstring Co-Authored-By: Claude Code --- LMLExplore/Probability/LargeDeviations/Pi.lean | 9 +++++---- LMLExplore/SequentialLearning/StaticAllocation.lean | 8 +++----- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/LMLExplore/Probability/LargeDeviations/Pi.lean b/LMLExplore/Probability/LargeDeviations/Pi.lean index 84dcd518..7e58da82 100644 --- a/LMLExplore/Probability/LargeDeviations/Pi.lean +++ b/LMLExplore/Probability/LargeDeviations/Pi.lean @@ -41,7 +41,7 @@ rates is above `r`. * `LMLExplore.hasLDP_pi`: the large deviation principle of the product measures, with rate function `x ↦ ∑ a, I a (x a)`. * `LMLExplore.neg_sum_le_liminf_log_pi`: the lower bound of the product principle at a point, - which needs no goodness of the rate functions. + for laws satisfying large deviation principles whose rate functions need not be good. * `LMLExplore.hasLDP_pi_comp_of_tendsto_div`: the large deviation principle of the product measures `Measure.pi fun a ↦ P a (m a n)` with `m a n / n → w a > 0`, with rate function `x ↦ ∑ a, w a I a (x a)`. @@ -88,9 +88,10 @@ private lemma ofReal_exp_neg_mul_le (n : ℕ) {r r' : ℝ} (h : r ≤ r') : variable {ι : Type*} [Fintype ι] {X : ι → Type*} [∀ a, MeasurableSpace (X a)] {P : ∀ a, ℕ → Measure (X a)} {I : ∀ a, X a → ℝ≥0∞} -/-- **The lower bound of the product principle.** If each `P a` satisfies the lower bound of a -large deviation principle at the speed `1 / n` with rate function `I a`, every neighbourhood `s` -of a point `x` satisfies `-∑ a, I a (x a) ≤ liminf_n (1 / n) log (∏ a, P a n) s`. -/ +/-- **The lower bound of the product principle.** If each `P a` satisfies a large deviation +principle at the speed `1 / n` with rate function `I a` (goodness of `I a` is not needed), +every neighbourhood `s` of a point `x` satisfies +`-∑ a, I a (x a) ≤ liminf_n (1 / n) log (∏ a, P a n) s`. -/ theorem neg_sum_le_liminf_log_pi [∀ a, TopologicalSpace (X a)] [∀ a n, SigmaFinite (P a n)] (h : ∀ a, HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) (P a) (I a)) {x : ∀ a, X a} {s : Set (∀ a, X a)} (hs : s ∈ 𝓝 x) : diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index 6c383b8c..d66095e0 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -215,11 +215,9 @@ theorem exists_eventually_le_streamMeasure_forall_mean_mem (fun a ↦ (∑ i ∈ range (n a), ω i a) / (n a : ℝ)) ∈ U} := by obtain ⟨δ, hδ, hδU⟩ := Metric.mem_nhds_iff.1 hU -- A closed ball of positive probability for each arm. - have hL (a : α) : ∃ L : ℕ, ν a (Metric.closedBall (x a) L) ≠ 0 := by - by_contra! h - have h_null := measure_iUnion_null (μ := ν a) h - rw [Metric.iUnion_closedBall_nat, measure_univ] at h_null - exact one_ne_zero h_null + have hL (a : α) : ∃ L : ℕ, ν a (Metric.closedBall (x a) L) ≠ 0 := + (exists_pos_measure_of_cover (Metric.iUnion_closedBall_nat (x a)) + (IsProbabilityMeasure.ne_zero _)).imp fun _ h ↦ h.ne' choose L hL using hL -- The first `n₀ T a = ⌈T w a - k⌉₊` entries of the row of `a`, a number within `2 k + 1` of -- `T w a`, have a mean close to `x a` with probability at least `exp (-(T r))` jointly. From 800cfbd075f8fd69af5bbc9f4117a648ecd9b586 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:16:35 +0100 Subject: [PATCH 6/7] refactor: move infinitePi_fin_mem_and_forall_add_mem to Probability/ProductMeasure The lemma concerns `Measure.infinitePi` and uses independence, so it now lives in a new `LMLExplore/Probability/ProductMeasure.lean`, mirroring Mathlib's home of `infinitePi`. `MeasureTheory/Constructions/Pi.lean` no longer imports `Mathlib.Probability.Independence.InfinitePi`. Co-Authored-By: Claude Code --- .../MeasureTheory/Constructions/Pi.lean | 49 ------------- LMLExplore/Probability/ProductMeasure.lean | 69 +++++++++++++++++++ .../SequentialLearning/StaticAllocation.lean | 2 +- 3 files changed, 70 insertions(+), 50 deletions(-) create mode 100644 LMLExplore/Probability/ProductMeasure.lean diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index ca13ea31..cc275003 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -7,7 +7,6 @@ module public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.Probability.ConditionalProbability -public import Mathlib.Probability.Independence.InfinitePi import TauCeti.MeasureTheory.Constructions.Pi /-! @@ -25,9 +24,6 @@ Under a product of probability measures, a measurable set whose lines along one all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate `i` and integrating the measures of the lines. -Under the infinite product `Measure.infinitePi` of copies of `μ`, the first `n` coordinates and -the next `m` coordinates are independent. - ## Main statements * `MeasureTheory.Measure.map_pi_comp_eq_map_pi_map`: @@ -39,8 +35,6 @@ the next `m` coordinates are independent. * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of probability measures, a measurable set whose lines `{t | update x i t ∈ E}` along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`. -* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the - first `n` terms and the next `m` terms are independent. -/ public section @@ -102,47 +96,4 @@ lemma pi_le_of_forall_measure_update_preimage_le [DecidableEq ι] {μ : ∀ i, M Measure.prod_apply (measurable_update' hE)] exact (lintegral_mono fun x ↦ h x).trans_eq (by simp) -open ProbabilityTheory Finset in -/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. -sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie -in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ -theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) - [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) - (hC : MeasurableSet C) : - (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by - -- The first `n` terms and the next `m` terms are independent. - have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) - (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) - (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) - simp only [id] at h_ind - have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ - u ⟨i, mem_range.2 i.2⟩ := by fun_prop - have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = - (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ - (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by - ext z - simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, - Set.mem_univ, true_implies, Subtype.forall, mem_Ico] - refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ - obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 - exact h j (by omega) - rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] - congr 1 - · -- The first `n` terms are `n` independent samples of `μ`. - have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = - Measure.pi fun _ : Fin n ↦ μ := by - rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] - rw [← h_pi, Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] - -- Both sides are the preimage of `B` under `z ↦ (z i)_{i : Fin n}`: the composite - -- `(fun u i ↦ u ⟨i, _⟩) ∘ (fun z i ↦ z i)` unfolds to `fun z i ↦ z ↑⟨i, _⟩`, and - -- `↑⟨i, _⟩ = i` is `Subtype.val` applied to a constructor. - rfl - · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = - ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by - ext z - simp - rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, - Nat.add_sub_cancel_left] - end MeasureTheory.Measure diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean new file mode 100644 index 00000000..21c9aec0 --- /dev/null +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -0,0 +1,69 @@ +/- +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.InfinitePi + +/-! +# Infinite products of probability measures: the first terms and the next terms + +Under the infinite product `Measure.infinitePi` of copies of a probability measure `μ`, the first +`n` coordinates and the next `m` coordinates are independent. + +## Main statements + +* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the + first `n` terms and the next `m` terms are independent. +-/ + +public section + +namespace MeasureTheory.Measure + +open ProbabilityTheory Finset in +/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. +sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie +in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ +theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) + [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) + (hC : MeasurableSet C) : + (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by + -- The first `n` terms and the next `m` terms are independent. + have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) + (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m)) + (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop) + simp only [id] at h_ind + have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ + u ⟨i, mem_range.2 i.2⟩ := by fun_prop + have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ + (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by + ext z + simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, + Set.mem_univ, true_implies, Subtype.forall, mem_Ico] + refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ + obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 + exact h j (by omega) + rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] + congr 1 + · -- The first `n` terms are `n` independent samples of `μ`. + have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = + Measure.pi fun _ : Fin n ↦ μ := by + rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] + rw [← h_pi, Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] + -- Both sides are the preimage of `B` under `z ↦ (z i)_{i : Fin n}`: the composite + -- `(fun u i ↦ u ⟨i, _⟩) ∘ (fun z i ↦ z i)` unfolds to `fun z i ↦ z ↑⟨i, _⟩`, and + -- `↑⟨i, _⟩ = i` is `Subtype.val` applied to a constructor. + rfl + · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) = + ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by + ext z + simp + rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, + Nat.add_sub_cancel_left] + +end MeasureTheory.Measure diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index d66095e0..8c5d540a 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -6,7 +6,7 @@ Authors: LMLExplore contributors module public import LMLExplore.Analysis.SpecificLimits.Basic -public import LMLExplore.MeasureTheory.Constructions.Pi +public import LMLExplore.Probability.ProductMeasure public import LMLExplore.Probability.LargeDeviations.Pi public import LMLExplore.SequentialLearning.SumRewards From e8f17ced80e1ea4aacffd7bd7951584236f5c740 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:37:50 +0100 Subject: [PATCH 7/7] refactor: rename streamMeasure_forall_row_mem to streamMeasure_forall_arm_mem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Match the naming of the sibling stream lemmas, which call the reward sequence (ω i a)_i of arm a "arm". Co-Authored-By: Claude Code --- LMLExplore/SequentialLearning/StaticAllocation.lean | 4 ++-- LMLExplore/SequentialLearning/SumRewards.lean | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index 8c5d540a..bea20a39 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -25,7 +25,7 @@ law of `μ̂_T` is not a product, unlike the laws of `LMLExplore.hasLDP_pi_comp_ The proof goes through LML's reward stream model `streamMeasure ν`, the stack of rewards of [LS, Section 4.6], whose rows are independent i.i.d. sequences -(`LMLExplore.streamMeasure_forall_row_mem`): the empirical mean of arm `a` +(`LMLExplore.streamMeasure_forall_arm_mem`): the empirical mean of arm `a` after `T` rounds is the mean of the first `N_{T,a}` entries of its row (`hasLaw_rewardByCount_streamMeasure`). @@ -280,7 +280,7 @@ theorem exists_eventually_le_streamMeasure_forall_mean_mem ext z simp only [E, Set.mem_ofPred_eq, Set.mem_preimage, Fin.sum_univ_eq_sum_range (fun i ↦ z i)] - rw [streamMeasure_forall_row_mem ν hE, Finset.prod_congr rfl fun a _ ↦ hE_eq a, + rw [streamMeasure_forall_arm_mem ν hE, Finset.prod_congr rfl fun a _ ↦ hE_eq a, Finset.prod_mul_distrib, mul_comm] gcongr refine hT.trans_eq ?_ diff --git a/LMLExplore/SequentialLearning/SumRewards.lean b/LMLExplore/SequentialLearning/SumRewards.lean index 0bab8cc5..a952bf4f 100644 --- a/LMLExplore/SequentialLearning/SumRewards.lean +++ b/LMLExplore/SequentialLearning/SumRewards.lean @@ -57,7 +57,7 @@ this way. stream, have the law `streamMeasure ν` of the stream model. * `hasLaw_arm_streamMeasure`: in the stream model, the array of the reward sequences of the arms has law `⨂ a, ⨂ i, ν a`, and `iIndepFun_arm_streamMeasure`: these sequences are independent; - `streamMeasure_forall_row_mem` is the product formula for events about them. + `streamMeasure_forall_arm_mem` is the product formula for events about them. * `hasLaw_arm_fin_streamMeasure`: in the stream model, the first `n` rewards of an arm `a` are `n` independent samples of `ν a`, and `hasLaw_pi_arm_fin_streamMeasure`: for finitely many arms, the first `n a` rewards of the arms `a` are independent across the arms. @@ -334,10 +334,10 @@ theorem iIndepFun_arm_streamMeasure {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : rw [← (hasLaw_eval_infinitePi _ a).comp h_arms |>.map_eq, Function.comp_def] omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in -/-- **Independence of the rows of the reward stream.** For finitely many arms, events about the +/-- **Independence of the arms of the reward stream.** For finitely many arms, events about the reward sequences `(ω i a)_i` of different arms `a` in LML's reward stream model are independent, and the reward sequence of `a` is an i.i.d. sequence of law `ν a`. -/ -theorem streamMeasure_forall_row_mem [Fintype α] {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : Kernel α 𝓡) +theorem streamMeasure_forall_arm_mem [Fintype α] {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : Kernel α 𝓡) [IsMarkovKernel ν] {E : α → Set (ℕ → 𝓡)} (hE : ∀ a, MeasurableSet (E a)) : streamMeasure ν {ω | ∀ a, (fun i ↦ ω i a) ∈ E a} = ∏ a, (Measure.infinitePi fun _ : ℕ ↦ ν a) (E a) := by