From 4acb9d460b4399698dce6bfb2bea6c71874b5bee Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 18:45:12 +0100 Subject: [PATCH 1/4] refactor: adopt Tau Ceti's good rate functions and large deviation principle MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Delete `LMLExplore.IsGoodRateFunction` and `LMLExplore.IsLDP` in favour of `TauCeti.Probability.IsGoodRateFunction` and `TauCeti.Probability.HasLDP` at the speed `fun n ↦ (n : ℝ≥0)⁻¹` along `atTop`. Restate the LMLExplore API on top of them: the constructor from closed sets and neighbourhoods and the bounds for every set (now for any filter and speed), the exponential bounds and exponential tightness at the speed `1 / n`, the exponential-bound criteria in the `HasLDP` normal form, the weighted sums of good rate functions, and Cramér's theorems. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- .../Probability/LargeDeviations/Basic.lean | 269 ++++++++++-------- .../Probability/LargeDeviations/Cramer.lean | 59 ++-- 2 files changed, 176 insertions(+), 152 deletions(-) diff --git a/LMLExplore/Probability/LargeDeviations/Basic.lean b/LMLExplore/Probability/LargeDeviations/Basic.lean index a204d71e..0a7e5073 100644 --- a/LMLExplore/Probability/LargeDeviations/Basic.lean +++ b/LMLExplore/Probability/LargeDeviations/Basic.lean @@ -12,48 +12,46 @@ public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef public import Mathlib.Order.LiminfLimsup public import Mathlib.Topology.Instances.EReal.Lemmas public import Mathlib.Topology.Semicontinuity.Defs +public import TauCeti.Probability.LargeDeviations.Basic /-! # Large deviation principles -A sequence of measures `P n` on a topological space `X` satisfies the *large deviation principle* -(LDP) with speed `n` and rate function `I : X → [0, ∞]` if `I` is lower semicontinuous and, for -every set `s`, -`-inf_{x ∈ int s} I(x) ≤ liminf_n (1 / n) log P n s` and -`limsup_n (1 / n) log P n s ≤ -inf_{x ∈ cl s} I(x)`. -The rate function is *good* if its sublevel sets `{x | I x ≤ c}` are compact. The logarithms are -`EReal`-valued, `log 0 = ⊥`. - -This is the definition of A. Dembo and O. Zeitouni, with the bounds stated for every set: the -measure of a set that is not measurable is its outer measure. When open sets are measurable -(`OpensMeasurableSpace X`, for example for the Borel σ-algebra), the bounds for every set follow -from the bounds for the measurable ones by monotonicity, since interiors are open and closures are -closed. - -The bounds are usually proved from exponential bounds on the probabilities: an upper bound -`P n s ≤ C exp (-(n r))` for every `r < c` gives `limsup_n (1 / n) log P n s ≤ -c`, and a lower -bound `C exp (-(n r)) ≤ P n s` for every `r > c` gives `-c ≤ liminf_n (1 / n) log P n s`. The -lower bound of the principle reduces to the neighbourhoods of single points, and the upper bound -to the closed sets. - -## Main definitions - -* `LMLExplore.IsGoodRateFunction I`: `I` is lower semicontinuous with compact sublevel sets. -* `LMLExplore.IsLDP P I`: the sequence of measures `P` satisfies the large deviation principle with - speed `n` and rate function `I`. +Tau Ceti's `TauCeti.Probability.HasLDP l ε μ I` is the large deviation principle of a family of +measures `μ i` along a filter `l`, with speed `ε` and rate function `I : X → [0, ∞]`: `I` is lower +semicontinuous, `-inf_G I ≤ liminf ε i log μ i G` for every open set `G` and +`limsup ε i log μ i F ≤ -inf_F I` for every closed set `F`. A sequence of measures `P n` satisfies +the principle with speed `1 / n` when `HasLDP atTop (fun n ↦ (n : ℝ≥0)⁻¹) P I`. The rate function +is *good* (`TauCeti.Probability.IsGoodRateFunction`) if its sublevel sets `{x | I x ≤ c}`, `c` +finite, are compact. The logarithms are `EReal`-valued, `log 0 = ⊥`. + +This file adds to Tau Ceti's definitions. The bounds extend to every set `s`, through its interior +and its closure, `-inf_{x ∈ int s} I(x) ≤ liminf ε i log μ i s` and +`limsup ε i log μ i s ≤ -inf_{x ∈ cl s} I(x)`: this is the definition of A. Dembo and +O. Zeitouni, where the measure of a set that is not measurable is its outer measure. + +At the speed `1 / n`, the bounds are usually proved from exponential bounds on the probabilities: +an upper bound `P n s ≤ C exp (-(n r))` for every `r < c` gives +`limsup_n (1 / n) log P n s ≤ -c`, and a lower bound `C exp (-(n r)) ≤ P n s` for every `r > c` +gives `-c ≤ liminf_n (1 / n) log P n s`. The lower bound of the principle reduces to the +neighbourhoods of single points. ## Main statements -* `LMLExplore.limsup_log_div_le_neg_of_le_mul_exp`: exponential upper bounds at every rate `r < c` - give `limsup_n (1 / n) log u n ≤ -c`. -* `LMLExplore.neg_le_liminf_log_div_of_mul_exp_le`: exponential lower bounds at every rate `r > c` - give `-c ≤ liminf_n (1 / n) log u n`. -* `LMLExplore.IsLDP.of_isClosed_of_mem_nhds`: the large deviation principle from the upper bound on - the closed sets and the lower bound on the neighbourhoods of each point. -* `LMLExplore.IsLDP.eventually_measure_le_exp`, `LMLExplore.IsLDP.eventually_exp_le_measure`: the - converse, exponential bounds on closed sets and on neighbourhoods of points, from the principle. -* `LMLExplore.IsLDP.exists_eventually_measure_norm_ge_le_exp`: exponential tightness on a normed - group, from a principle with a good rate function. +* `LMLExplore.limsup_inv_mul_log_le_neg_of_le_mul_exp`: exponential upper bounds at every rate + `r < c` give `limsup_n (1 / n) log u n ≤ -c`. +* `LMLExplore.neg_le_liminf_inv_mul_log_of_mul_exp_le`: exponential lower bounds at every rate + `r > c` give `-c ≤ liminf_n (1 / n) log u n`. +* `TauCeti.Probability.HasLDP.of_isClosed_of_mem_nhds`: the large deviation principle from the + upper bound on the closed sets and the lower bound on the neighbourhoods of each point. +* `TauCeti.Probability.HasLDP.neg_iInf_interior_le_liminf`, + `TauCeti.Probability.HasLDP.limsup_le_neg_iInf_closure`: the bounds of the principle for every + set, through its interior and its closure. +* `TauCeti.Probability.HasLDP.eventually_measure_le_exp`, + `TauCeti.Probability.HasLDP.eventually_exp_le_measure`: the converse at the speed `1 / n`, + exponential bounds on closed sets and on neighbourhoods of points, from the principle. +* `TauCeti.Probability.HasLDP.exists_eventually_measure_norm_ge_le_exp`: exponential tightness on a + normed group, from a principle at the speed `1 / n` with a good rate function. * `LMLExplore.isGoodRateFunction_sum_mul`: positive weighted sums of good rate functions on the coordinates of a finite product are good. @@ -62,7 +60,7 @@ to the closed sets. * [DZ98] A. Dembo and O. Zeitouni, *Large Deviations Techniques and Applications*, 2nd ed., Springer, 1998, Section 1.2. -The definitions and the exponential-bound criteria are adapted from the formalization +The exponential-bound criteria are adapted from the formalization Degenne2023Existence (`github.com/RemyDegenne/Degenne2023Existence`, file `Degenne2023Existence/ForLMLExplore/Probability/LargeDeviations/Basic.lean`, commit `5afa57772d415c17cfd89de287fb004ca51d8fb3`, by Rémy Degenne, Apache 2.0) of R. Degenne, *On the @@ -72,36 +70,17 @@ existence of a complexity in fixed budget bandit identification*, COLT 2023. public section open MeasureTheory Filter Topology +open TauCeti.Probability (HasLDP IsGoodRateFunction) open scoped ENNReal NNReal namespace LMLExplore -variable {X : Type*} [TopologicalSpace X] {mX : MeasurableSpace X} - -/-- The function `I : X → [0, ∞]` is a *good rate function*: it is lower semicontinuous and its -sublevel sets `{x | I x ≤ c}`, `c` finite, are compact [DZ98, Section 1.2]. -/ -structure IsGoodRateFunction (I : X → ℝ≥0∞) : Prop where - /-- A good rate function is lower semicontinuous. -/ - lowerSemicontinuous : LowerSemicontinuous I - /-- The sublevel sets of a good rate function at the finite levels are compact. -/ - isCompact_setOf_le (c : ℝ≥0) : IsCompact {x | I x ≤ c} - -/-- The sequence of measures `P n` satisfies the *large deviation principle* with speed `n` and -rate function `I` [DZ98, Section 1.2]: `I` is lower semicontinuous and, for every set `s`, -`-inf_{x ∈ int s} I(x) ≤ liminf_n (1 / n) log P n s` and -`limsup_n (1 / n) log P n s ≤ -inf_{x ∈ cl s} I(x)`. -/ -structure IsLDP (P : ℕ → Measure X) (I : X → ℝ≥0∞) : Prop where - /-- The rate function is lower semicontinuous. -/ - lowerSemicontinuous : LowerSemicontinuous I - /-- The lower bound, through the interior. -/ - neg_iInf_interior_le_liminf (s : Set X) : - -(((⨅ x ∈ interior s, I x : ℝ≥0∞)) : EReal) ≤ - liminf (fun n : ℕ ↦ ENNReal.log (P n s) / n) atTop - /-- The upper bound, through the closure. -/ - limsup_le_neg_iInf_closure (s : Set X) : - limsup (fun n : ℕ ↦ ENNReal.log (P n s) / n) atTop ≤ - -(((⨅ x ∈ closure s, I x : ℝ≥0∞)) : EReal) +/-- The speed `1 / n` as a multiplier in `EReal` is a division by `n`, also for `n = 0`, where +both sides vanish. -/ +private lemma coe_inv_natCast_mul (n : ℕ) (a : EReal) : + (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / n := by + rw [NNReal.coe_inv, NNReal.coe_natCast, EReal.coe_inv, EReal.coe_natCast, EReal.div_eq_inv_mul] /-! ### Exponential bounds -/ @@ -135,10 +114,12 @@ private lemma log_mul_exp_div {C : ℝ≥0∞} (hC0 : C ≠ 0) (hC : C ≠ ⊤) /-- **Exponential upper bounds give the upper bound of a large deviation principle.** If for every real `r < c` there is a finite `C` with `u n ≤ C exp (-(n r))` eventually, then `limsup_n (1 / n) log u n ≤ -c`. -/ -lemma limsup_log_div_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} +lemma limsup_inv_mul_log_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} (h : ∀ r : ℝ, (r : EReal) < c → ∃ C : ℝ≥0∞, C ≠ ⊤ ∧ ∀ᶠ n : ℕ in atTop, u n ≤ C * ENNReal.ofReal (Real.exp (-(n * r)))) : - limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop ≤ -(c : EReal) := by + limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ + -(c : EReal) := by + simp_rw [coe_inv_natCast_mul] rw [EReal.le_neg] refine EReal.ge_of_forall_gt_iff_ge.1 fun r hr ↦ ?_ rw [EReal.le_neg] @@ -155,10 +136,11 @@ lemma limsup_log_div_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ≥0 /-- **Exponential lower bounds give the lower bound of a large deviation principle.** If for every real `r > c` there is a nonzero `C` with `C exp (-(n r)) ≤ u n` eventually, then `-c ≤ liminf_n (1 / n) log u n`. -/ -lemma neg_le_liminf_log_div_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} +lemma neg_le_liminf_inv_mul_log_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} (h : ∀ r : ℝ, (c : EReal) < r → ∃ C : ℝ≥0∞, C ≠ 0 ∧ ∀ᶠ n : ℕ in atTop, C * ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n) : - -(c : EReal) ≤ liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop := by + -(c : EReal) ≤ liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop := by + simp_rw [coe_inv_natCast_mul] rw [EReal.neg_le] refine EReal.le_of_forall_lt_iff_le.1 fun r hr ↦ ?_ rw [EReal.neg_le] @@ -174,49 +156,15 @@ lemma neg_le_liminf_log_div_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ≥0 gcongr exact min_le_left _ _ -/-! ### Reduction to closed sets and to neighbourhoods of points -/ - -/-- **The large deviation principle from the bounds on closed sets and neighbourhoods.** If `I` is -lower semicontinuous, `limsup_n (1 / n) log P n s ≤ -inf_s I` for every closed set `s`, and -`-I(x) ≤ liminf_n (1 / n) log P n s` for every neighbourhood `s` of every point `x`, then the -measures `P n` satisfy the large deviation principle with rate function `I`. -/ -lemma IsLDP.of_isClosed_of_mem_nhds {P : ℕ → Measure X} {I : X → ℝ≥0∞} - (hI : LowerSemicontinuous I) - (h_upper : ∀ s, IsClosed s → - limsup (fun n : ℕ ↦ ENNReal.log (P n s) / n) atTop ≤ -(((⨅ x ∈ s, I x : ℝ≥0∞)) : EReal)) - (h_lower : ∀ x, ∀ s ∈ 𝓝 x, - -(I x : EReal) ≤ liminf (fun n : ℕ ↦ ENNReal.log (P n s) / n) atTop) : - IsLDP P I where - lowerSemicontinuous := hI - neg_iInf_interior_le_liminf s := by - have h_mono (n : ℕ) : - ENNReal.log (P n (interior s)) / n ≤ ENNReal.log (P n s) / n := - EReal.div_le_div_right_of_nonneg (by exact_mod_cast n.cast_nonneg) - (ENNReal.log_monotone (measure_mono interior_subset)) - refine le_trans ?_ (liminf_le_liminf (Eventually.of_forall h_mono)) - rw [EReal.neg_le] - set L := liminf (fun n : ℕ ↦ ENNReal.log (P n (interior s)) / n) atTop - rcases le_or_gt (-L) 0 with hL | hL - · exact hL.trans (EReal.coe_ennreal_nonneg _) - rw [← EReal.coe_toENNReal hL.le, EReal.coe_ennreal_le_coe_ennreal_iff] - refine le_iInf₂ fun x hx ↦ ?_ - rw [← EReal.coe_ennreal_le_coe_ennreal_iff, EReal.coe_toENNReal hL.le, EReal.neg_le] - exact h_lower x _ (isOpen_interior.mem_nhds hx) - limsup_le_neg_iInf_closure s := by - have h_mono (n : ℕ) : - ENNReal.log (P n s) / n ≤ ENNReal.log (P n (closure s)) / n := - EReal.div_le_div_right_of_nonneg (by exact_mod_cast n.cast_nonneg) - (ENNReal.log_monotone (measure_mono subset_closure)) - exact (limsup_le_limsup (Eventually.of_forall h_mono)).trans (h_upper _ isClosed_closure) - /-! ### Exponential bounds from the bounds of a large deviation principle -/ /-- **Exponential upper bounds from the upper bound of a large deviation principle.** If `limsup_n (1 / n) log u n ≤ -c`, then `u n ≤ exp (-(n r))` eventually, for every real `r < c`. -/ -lemma eventually_le_exp_of_limsup_log_div_le {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} - (h : limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop ≤ -(c : EReal)) {r : ℝ} - (hr : (r : EReal) < c) : +lemma eventually_le_exp_of_limsup_inv_mul_log_le {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} + (h : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ + -(c : EReal)) {r : ℝ} (hr : (r : EReal) < c) : ∀ᶠ n : ℕ in atTop, u n ≤ ENNReal.ofReal (Real.exp (-(n * r))) := by + simp_rw [coe_inv_natCast_mul] at h have h' : limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop < ((-r : ℝ) : EReal) := by rw [EReal.coe_neg] exact h.trans_lt (EReal.neg_lt_neg_iff.2 hr) @@ -228,10 +176,12 @@ lemma eventually_le_exp_of_limsup_log_div_le {u : ℕ → ℝ≥0∞} {c : ℝ /-- **Exponential lower bounds from the lower bound of a large deviation principle.** If `-c ≤ liminf_n (1 / n) log u n`, then `exp (-(n r)) ≤ u n` eventually, for every real `r > c`. -/ -lemma eventually_exp_le_of_neg_le_liminf_log_div {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} - (h : -(c : EReal) ≤ liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop) {r : ℝ} +lemma eventually_exp_le_of_neg_le_liminf_inv_mul_log {u : ℕ → ℝ≥0∞} {c : ℝ≥0∞} + (h : -(c : EReal) ≤ + liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop) {r : ℝ} (hr : (c : EReal) < r) : ∀ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n := by + simp_rw [coe_inv_natCast_mul] at h have h' : ((-r : ℝ) : EReal) < liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop := by rw [EReal.coe_neg] exact (EReal.neg_lt_neg_iff.2 hr).trans_le h @@ -241,33 +191,94 @@ lemma eventually_exp_le_of_neg_le_liminf_log_div {u : ℕ → ℝ≥0∞} {c : ENNReal.log_strictMono.lt_iff_lt] at hn exact hn.le -/-- Under a large deviation principle, the measure of a closed set `s` is eventually at most -`exp (-(n r))`, for every real `r` below the infimum of the rate function on `s`. -/ -lemma IsLDP.eventually_measure_le_exp {P : ℕ → Measure X} {I : X → ℝ≥0∞} (h : IsLDP P I) - {s : Set X} (hs : IsClosed s) {r : ℝ} (hr : (r : EReal) < ⨅ x ∈ s, I x) : +end LMLExplore + +namespace TauCeti.Probability.HasLDP + +variable {ι X : Type*} [TopologicalSpace X] {mX : MeasurableSpace X} {l : Filter ι} + {ε : ι → ℝ≥0} {μ : ι → Measure X} {I : X → ℝ≥0∞} + +/-! ### Reduction to closed sets and to neighbourhoods of points -/ + +/-- **The large deviation principle from the bounds on closed sets and neighbourhoods.** If `I` is +lower semicontinuous, `limsup ε i log μ i s ≤ -inf_s I` for every closed set `s`, and +`-I(x) ≤ liminf ε i log μ i s` for every neighbourhood `s` of every point `x`, then the measures +`μ i` satisfy the large deviation principle with speed `ε` and rate function `I`. -/ +theorem of_isClosed_of_mem_nhds (hI : LowerSemicontinuous I) + (h_upper : ∀ s, IsClosed s → + limsup (fun i ↦ ((ε i : ℝ) : EReal) * ENNReal.log (μ i s)) l ≤ + -(((⨅ x ∈ s, I x : ℝ≥0∞)) : EReal)) + (h_lower : ∀ x, ∀ s ∈ 𝓝 x, + -(I x : EReal) ≤ liminf (fun i ↦ ((ε i : ℝ) : EReal) * ENNReal.log (μ i s)) l) : + HasLDP l ε μ I where + lowerSemicontinuous := hI + lower_bound s hs := by + rw [EReal.neg_le] + set L := liminf (fun i ↦ ((ε i : ℝ) : EReal) * ENNReal.log (μ i s)) l + rcases le_or_gt (-L) 0 with hL | hL + · exact hL.trans (EReal.coe_ennreal_nonneg _) + rw [← EReal.coe_toENNReal hL.le, EReal.coe_ennreal_le_coe_ennreal_iff] + refine le_iInf₂ fun x hx ↦ ?_ + rw [← EReal.coe_ennreal_le_coe_ennreal_iff, EReal.coe_toENNReal hL.le, EReal.neg_le] + exact h_lower x s (hs.mem_nhds hx) + upper_bound := h_upper + +omit [TopologicalSpace X] in +/-- The speed `ε` multiplies the logarithms of the measures monotonically: `ε i log μ i s` is +monotone in `s`. -/ +private lemma mul_log_measure_mono (ε : ι → ℝ≥0) (μ : ι → Measure X) (i : ι) {s t : Set X} + (hst : s ⊆ t) : + ((ε i : ℝ) : EReal) * ENNReal.log (μ i s) ≤ ((ε i : ℝ) : EReal) * ENNReal.log (μ i t) := + mul_le_mul_of_nonneg_left (ENNReal.log_monotone (measure_mono hst)) + (EReal.coe_nonneg.2 (ε i).coe_nonneg) + +/-- **The lower bound of a large deviation principle for every set**, through its interior: +`-inf_{x ∈ int s} I(x) ≤ liminf ε i log μ i s`. -/ +theorem neg_iInf_interior_le_liminf (h : HasLDP l ε μ I) (s : Set X) : + -(((⨅ x ∈ interior s, I x : ℝ≥0∞)) : EReal) ≤ + liminf (fun i ↦ ((ε i : ℝ) : EReal) * ENNReal.log (μ i s)) l := by + refine (h.lower_bound _ isOpen_interior).trans (liminf_le_liminf ?_) + exact Eventually.of_forall fun i ↦ mul_log_measure_mono ε μ i interior_subset + +/-- **The upper bound of a large deviation principle for every set**, through its closure: +`limsup ε i log μ i s ≤ -inf_{x ∈ cl s} I(x)`. -/ +theorem limsup_le_neg_iInf_closure (h : HasLDP l ε μ I) (s : Set X) : + limsup (fun i ↦ ((ε i : ℝ) : EReal) * ENNReal.log (μ i s)) l ≤ + -(((⨅ x ∈ closure s, I x : ℝ≥0∞)) : EReal) := by + refine le_trans (limsup_le_limsup ?_) (h.upper_bound _ isClosed_closure) + exact Eventually.of_forall fun i ↦ mul_log_measure_mono ε μ i subset_closure + +/-! ### Exponential bounds from a principle at the speed `1 / n` -/ + +/-- Under a large deviation principle at the speed `1 / n`, the measure of a closed set `s` is +eventually at most `exp (-(n r))`, for every real `r` below the infimum of the rate function on +`s`. -/ +theorem eventually_measure_le_exp {P : ℕ → Measure X} + (h : HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) P I) {s : Set X} (hs : IsClosed s) {r : ℝ} + (hr : (r : EReal) < ⨅ x ∈ s, I x) : ∀ᶠ n : ℕ in atTop, P n s ≤ ENNReal.ofReal (Real.exp (-(n * r))) := - eventually_le_exp_of_limsup_log_div_le - ((h.limsup_le_neg_iInf_closure s).trans_eq (by rw [hs.closure_eq])) hr + LMLExplore.eventually_le_exp_of_limsup_inv_mul_log_le (h.upper_bound s hs) hr -/-- Under a large deviation principle, the measure of a neighbourhood `s` of `x` is eventually at -least `exp (-(n r))`, for every real `r > I x`. -/ -lemma IsLDP.eventually_exp_le_measure {P : ℕ → Measure X} {I : X → ℝ≥0∞} (h : IsLDP P I) - {x : X} {s : Set X} (hs : s ∈ 𝓝 x) {r : ℝ} (hr : (I x : EReal) < r) : +/-- Under a large deviation principle at the speed `1 / n`, the measure of a neighbourhood `s` of +`x` is eventually at least `exp (-(n r))`, for every real `r > I x`. -/ +theorem eventually_exp_le_measure {P : ℕ → Measure X} + (h : HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) P I) {x : X} {s : Set X} (hs : s ∈ 𝓝 x) {r : ℝ} + (hr : (I x : EReal) < r) : ∀ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (-(n * r))) ≤ P n s := by - refine eventually_exp_le_of_neg_le_liminf_log_div ((EReal.neg_le_neg_iff.2 ?_).trans - (h.neg_iInf_interior_le_liminf s)) hr + refine LMLExplore.eventually_exp_le_of_neg_le_liminf_inv_mul_log + ((EReal.neg_le_neg_iff.2 ?_).trans (h.neg_iInf_interior_le_liminf s)) hr exact EReal.coe_ennreal_le_coe_ennreal_iff.2 (iInf₂_le x (mem_interior_iff_mem_nhds.2 hs)) -/-- **Exponential tightness.** Under a large deviation principle with a good rate function on a -normed group, for every real `r` there is a radius `M` such that the measure of +/-- **Exponential tightness.** Under a large deviation principle at the speed `1 / n` with a good +rate function on a normed group, for every real `r` there is a radius `M` such that the measure of `{x | M ≤ ‖x‖}` is eventually at most `exp (-(n r))`. -/ -lemma IsLDP.exists_eventually_measure_norm_ge_le_exp {E : Type*} [SeminormedAddCommGroup E] - {mE : MeasurableSpace E} {P : ℕ → Measure E} {I : E → ℝ≥0∞} (h : IsLDP P I) - (hI : IsGoodRateFunction I) (r : ℝ) : +theorem exists_eventually_measure_norm_ge_le_exp {E : Type*} [SeminormedAddCommGroup E] + {mE : MeasurableSpace E} {P : ℕ → Measure E} {I : E → ℝ≥0∞} + (h : HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) P I) (hI : IsGoodRateFunction I) (r : ℝ) : ∃ M : ℝ, ∀ᶠ n : ℕ in atTop, P n {x | M ≤ ‖x‖} ≤ ENNReal.ofReal (Real.exp (-(n * r))) := by set c : ℝ≥0 := (max r 0 + 1).toNNReal with hc_def - obtain ⟨C, hC⟩ := - (Metric.isBounded_iff_subset_closedBall (0 : E)).1 (hI.isCompact_setOf_le c).isBounded + obtain ⟨C, hC⟩ := (Metric.isBounded_iff_subset_closedBall (0 : E)).1 + (hI.isCompact_sublevel c ENNReal.coe_ne_top).isBounded refine ⟨C + 1, h.eventually_measure_le_exp (isClosed_le continuous_const continuous_norm) ?_⟩ have hc : (((c : ℝ≥0∞)) : EReal) = ((max r 0 + 1 : ℝ) : EReal) := by rw [hc_def, ENNReal.ofNNReal_toNNReal, EReal.coe_ennreal_ofReal, @@ -282,6 +293,10 @@ lemma IsLDP.exists_eventually_measure_norm_ge_le_exp {E : Type*} [SeminormedAddC simp only [Set.mem_ofPred_eq] at hx linarith +end TauCeti.Probability.HasLDP + +namespace LMLExplore + /-- **Weighted sums of good rate functions are good.** For good rate functions `I a` on spaces `X a`, indexed by a finite type, and positive weights `w a`, the function `x ↦ ∑ a, w a I a (x a)` on the product is a good rate function. -/ @@ -293,9 +308,11 @@ lemma isGoodRateFunction_sum_mul {ι : Type*} [Fintype ι] {X : ι → Type*} lowerSemicontinuous_sum fun a _ ↦ (ENNReal.continuous_const_mul ENNReal.ofReal_ne_top).comp_lowerSemicontinuous ((hI a).lowerSemicontinuous.comp (continuous_apply a)) fun _ _ h ↦ by dsimp only; gcongr - refine ⟨h_lsc, fun c ↦ ?_⟩ + refine ⟨h_lsc, fun c hc ↦ ?_⟩ + lift c to ℝ≥0 using hc refine IsCompact.of_isClosed_subset - (isCompact_univ_pi fun a ↦ (hI a).isCompact_setOf_le (c / (w a).toNNReal)) + (isCompact_univ_pi fun a ↦ + (hI a).isCompact_sublevel ((c / (w a).toNNReal : ℝ≥0) : ℝ≥0∞) ENNReal.coe_ne_top) (h_lsc.isClosed_preimage _) fun x hx a _ ↦ ?_ have hw0 : (w a).toNNReal ≠ 0 := by simpa using hw a have h_le : ENNReal.ofReal (w a) * I a (x a) ≤ c := diff --git a/LMLExplore/Probability/LargeDeviations/Cramer.lean b/LMLExplore/Probability/LargeDeviations/Cramer.lean index 6f8f3919..be3709a5 100644 --- a/LMLExplore/Probability/LargeDeviations/Cramer.lean +++ b/LMLExplore/Probability/LargeDeviations/Cramer.lean @@ -17,9 +17,10 @@ public import LMLExplore.MeasureTheory.Constructions.Pi Let `ν` be a probability measure on `ℝ` with Cramér rate function `I(x) = sup_t (t x - log E_ν[exp (t X)])` (`LMLExplore.rateFunction id ν`). The laws of the empirical means `(∑ i < n, X i) / n` of `n` independent samples of `ν` satisfy the large deviation -principle with speed `n` and rate function `I` as soon as `ν` has a mean, and `I` is a good rate -function when the cumulant generating function of `ν` is finite on a neighbourhood of `0`: -this is Cramér's theorem [DZ98, Theorem 2.2.3]. The same holds for the empirical means of a +principle (`TauCeti.Probability.HasLDP`) with speed `1 / n` and rate function `I` as soon as `ν` +has a mean, and `I` is a good rate function (`TauCeti.Probability.IsGoodRateFunction`) when the +cumulant generating function of `ν` is finite on a neighbourhood of `0`: this is Cramér's theorem +[DZ98, Theorem 2.2.3]. The same holds for the empirical means of a sequence of independent identically distributed real random variables, and for the empirical means of the statistic `T` of the samples of a member of an exponential family, with the extended divergence `Measure.expFamilyRate` of the family as rate function [D23, Lemma 11]. These are the @@ -47,13 +48,13 @@ coercive, so a nested compact sets argument shows that their infima converge. closed sets, for `ν` with a mean. * `LMLExplore.neg_rateFunction_le_liminf_log_measure`: the lower bound of Cramér's theorem on the neighbourhoods of every level, for every probability measure `ν`. -* `LMLExplore.isLDP_cramer`: **Cramér's theorem**, the large deviation principle of the empirical +* `LMLExplore.hasLDP_cramer`: **Cramér's theorem**, the large deviation principle of the empirical means of independent samples of a law on `ℝ` with a mean. * `LMLExplore.isGoodRateFunction_rateFunction`: the rate function is good when the cumulant generating function is finite near `0`. -* `LMLExplore.isLDP_cramer_of_iIndepFun`: Cramér's theorem for a sequence of independent +* `LMLExplore.hasLDP_cramer_of_iIndepFun`: Cramér's theorem for a sequence of independent identically distributed integrable real random variables. -* `MeasureTheory.Measure.isLDP_cramer_expFamily`: Cramér's theorem for the statistic of the +* `MeasureTheory.Measure.hasLDP_cramer_expFamily`: Cramér's theorem for the statistic of the samples of a member of a one-parameter exponential family on any measurable space, with the extended divergence `Measure.expFamilyRate` as rate function, and `MeasureTheory.Measure.isGoodRateFunction_expFamilyRate_left`: that rate function is good. @@ -76,6 +77,7 @@ new. public section open MeasureTheory ProbabilityTheory Filter Real Set Finset Topology +open TauCeti.Probability (HasLDP IsGoodRateFunction) open scoped ENNReal NNReal @@ -105,10 +107,11 @@ a closed set `F`, the laws `P n` of the empirical means of `n` independent sampl [DZ98, Theorem 2.2.3]. -/ lemma limsup_log_measure_le_neg_iInf_rateFunction [IsProbabilityMeasure ν] (hν : Integrable id ν) {F : Set ℝ} (hF : IsClosed F) : - limsup (fun n : ℕ ↦ ENNReal.log (((Measure.pi fun _ : Fin n ↦ ν).map - fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) F) / n) atTop ≤ + limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * + ENNReal.log (((Measure.pi fun _ : Fin n ↦ ν).map + fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) F)) atTop ≤ -(((⨅ x ∈ F, rateFunction id ν x : ℝ≥0∞)) : EReal) := by - refine limsup_log_div_le_neg_of_le_mul_exp fun r hr ↦ + refine limsup_inv_mul_log_le_neg_of_le_mul_exp fun r hr ↦ ⟨2, ENNReal.ofNat_ne_top, Eventually.of_forall fun n ↦ ?_⟩ -- The rate function is at least `r` on `F`, and the empirical mean has rate at least `r` with -- probability at most `2 exp (-(n r))` by the two-sided Cramér–Chernoff bound. @@ -470,12 +473,12 @@ samples of `ν` satisfy `-I(x) ≤ liminf_n (1 / n) log P n U`, with `I` the Cra `ν` [DZ98, Theorem 2.2.3]. -/ lemma neg_rateFunction_le_liminf_log_measure [IsProbabilityMeasure ν] {U : Set ℝ} (hU : U ∈ 𝓝 x) : - -(rateFunction id ν x : EReal) ≤ liminf (fun n : ℕ ↦ ENNReal.log - (((Measure.pi fun _ : Fin n ↦ ν).map fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) U) / n) - atTop := by + -(rateFunction id ν x : EReal) ≤ liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * + ENNReal.log (((Measure.pi fun _ : Fin n ↦ ν).map + fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) U)) atTop := by by_cases hI : rateFunction id ν x = ⊤ · simp [hI] - refine neg_le_liminf_log_div_of_mul_exp_le fun r hr ↦ ⟨1, one_ne_zero, ?_⟩ + refine neg_le_liminf_inv_mul_log_of_mul_exp_le fun r hr ↦ ⟨1, one_ne_zero, ?_⟩ simp only [one_mul] by_cases hgt : ν (Ioi x) = 0 · -- `ν` gives no mass above `x`. @@ -499,10 +502,11 @@ lemma neg_rateFunction_le_liminf_log_measure [IsProbabilityMeasure ν] {U : Set /-- **Cramér's theorem** [DZ98, Theorem 2.2.3]. For a probability measure `ν` on `ℝ` with a mean, the laws of the empirical means `(∑ i < n, X i) / n` of `n` independent samples of `ν` satisfy the -large deviation principle with speed `n` and the Cramér rate function +large deviation principle with speed `1 / n` and the Cramér rate function `I(x) = sup_t (t x - log E_ν[exp (t X)])` of `ν`. -/ -theorem isLDP_cramer [IsProbabilityMeasure ν] (hν : Integrable id ν) : - IsLDP (fun n ↦ (Measure.pi fun _ : Fin n ↦ ν).map fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) +theorem hasLDP_cramer [IsProbabilityMeasure ν] (hν : Integrable id ν) : + HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) + (fun n ↦ (Measure.pi fun _ : Fin n ↦ ν).map fun y : Fin n → ℝ ↦ (∑ i, y i) / (n : ℝ)) (rateFunction id ν) := .of_isClosed_of_mem_nhds (lowerSemicontinuous_rateFunction id ν) (fun _ hF ↦ limsup_log_measure_le_neg_iInf_rateFunction hν hF) @@ -515,7 +519,8 @@ finite on a neighbourhood of `0` [DZ98, Lemma 2.2.5]. -/ lemma isGoodRateFunction_rateFunction {Ω : Type*} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {P : Measure Ω} (h : 0 ∈ interior (integrableExpSet X P)) : IsGoodRateFunction (rateFunction X P) := by - refine ⟨lowerSemicontinuous_rateFunction X P, fun c ↦ ?_⟩ + refine ⟨lowerSemicontinuous_rateFunction X P, fun c hc ↦ ?_⟩ + lift c to ℝ≥0 using hc obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.1 (mem_interior_iff_mem_nhds.1 h) have hε2 : 0 < ε / 2 := by positivity have ht : ε / 2 ∈ integrableExpSet X P := by @@ -543,11 +548,12 @@ lemma isGoodRateFunction_rateFunction {Ω : Type*} {mΩ : MeasurableSpace Ω} {X /-- **Cramér's theorem for independent identically distributed random variables** [DZ98, Theorem 2.2.3]. For independent real random variables `X i`, `i : ℕ`, distributed as `X 0`, with `X 0` integrable, the laws of the empirical means `(∑ i < n, X i) / n` satisfy the large -deviation principle with speed `n` and the Cramér rate function of `X 0`. -/ -theorem isLDP_cramer_of_iIndepFun {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} +deviation principle with speed `1 / n` and the Cramér rate function of `X 0`. -/ +theorem hasLDP_cramer_of_iIndepFun {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {X : ℕ → Ω → ℝ} (hint : Integrable (X 0) P) (hindep : iIndepFun X P) (hident : ∀ i, IdentDistrib (X i) (X 0) P P) : - IsLDP (fun n ↦ P.map fun ω ↦ (∑ i ∈ range n, X i ω) / (n : ℝ)) (rateFunction (X 0) P) := by + HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) + (fun n ↦ P.map fun ω ↦ (∑ i ∈ range n, X i ω) / (n : ℝ)) (rateFunction (X 0) P) := by have hX0 : HasLaw (X 0) (P.map (X 0)) P := ⟨hint.aemeasurable, rfl⟩ have := hX0.isProbabilityMeasure_iff.1 ‹_› have h_law (n : ℕ) : P.map (fun ω ↦ (∑ i ∈ range n, X i ω) / (n : ℝ)) = @@ -561,7 +567,7 @@ theorem isLDP_cramer_of_iIndepFun {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : M simp [Fin.sum_univ_eq_sum_range (fun i ↦ X i ω) n] simp_rw [h_law] rw [(hX0.identDistrib HasLaw.id).rateFunction_eq] - exact isLDP_cramer ((integrable_map_measure aestronglyMeasurable_id hint.aemeasurable).2 hint) + exact hasLDP_cramer ((integrable_map_measure aestronglyMeasurable_id hint.aemeasurable).2 hint) end LMLExplore @@ -576,12 +582,13 @@ variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {ρ : Measure 𝓧} {T : /-- **Cramér's theorem for exponential families.** For a nonzero measure `ρ` on a measurable space `𝓧`, a statistic `T` and a mean `μ` of the exponential family of `ρ` and `T`, the laws of the empirical means `(∑ i < n, T (Y i)) / n` of the statistic of `n` independent samples `Y i` of -the member of mean `μ` satisfy the large deviation principle with speed `n` and rate function +the member of mean `μ` satisfy the large deviation principle with speed `1 / n` and rate function the extended divergence `x ↦ dbar(x, μ)` (`Measure.expFamilyRate`), which is the divergence `d(x, μ)` at the means `x` of the family [D23, Lemma 11]. -/ -theorem isLDP_cramer_expFamily [NeZero ρ] (hμ : μ ∈ ρ.expFamilyMeans T) : - IsLDP (fun n ↦ (Measure.pi fun _ : Fin n ↦ ρ.expFamily T (ρ.natParam T μ)).map - fun y : Fin n → 𝓧 ↦ (∑ i, T (y i)) / (n : ℝ)) (fun x ↦ ρ.expFamilyRate T x μ) := by +theorem hasLDP_cramer_expFamily [NeZero ρ] (hμ : μ ∈ ρ.expFamilyMeans T) : + HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) + (fun n ↦ (Measure.pi fun _ : Fin n ↦ ρ.expFamily T (ρ.natParam T μ)).map + fun y : Fin n → 𝓧 ↦ (∑ i, T (y i)) / (n : ℝ)) (fun x ↦ ρ.expFamilyRate T x μ) := by have hη := natParam_mem_interior_integrableExpSet hμ have := isProbabilityMeasure_expFamily (interior_subset hη) have hT := integrable_expFamily hη @@ -596,7 +603,7 @@ theorem isLDP_cramer_expFamily [NeZero ρ] (hμ : μ ∈ ρ.expFamilyMeans T) : (measurable_mean n).aemeasurable simp_rw [h_law, expFamilyRate_def, (hlaw.identDistrib HasLaw.id).rateFunction_eq] - exact isLDP_cramer ((integrable_map_measure aestronglyMeasurable_id hT.aemeasurable).2 hT) + exact hasLDP_cramer ((integrable_map_measure aestronglyMeasurable_id hT.aemeasurable).2 hT) /-- **The extended divergence of an exponential family is a good rate function** in its first argument: for a mean `μ` of the exponential family of `ρ` and `T`, the function From 5c5d0f9616553a9572d9a70ce5f72a819d979ea4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 22:53:27 +0100 Subject: [PATCH 2/4] refactor: export the EReal inverse-multiplication lemma from a general file MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the private `coe_inv_natCast_mul` of the large-deviations base file by the public `EReal.coe_nnreal_inv_mul` in `LMLExplore/Data/EReal/Inv.lean`, stated for any `r : ℝ≥0`. Co-Authored-By: Claude Code --- LMLExplore/Data/EReal/Inv.lean | 33 +++++++++++++++++++ .../Probability/LargeDeviations/Basic.lean | 16 +++------ 2 files changed, 38 insertions(+), 11 deletions(-) create mode 100644 LMLExplore/Data/EReal/Inv.lean diff --git a/LMLExplore/Data/EReal/Inv.lean b/LMLExplore/Data/EReal/Inv.lean new file mode 100644 index 00000000..1adb9790 --- /dev/null +++ b/LMLExplore/Data/EReal/Inv.lean @@ -0,0 +1,33 @@ +/- +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.Data.EReal.Inv + +/-! +# Multiplying an extended real by the inverse of a nonnegative real + +## Main statements + +* `EReal.coe_nnreal_inv_mul`: multiplying an extended real `a` by the inverse `r⁻¹` of a + nonnegative real, taken in `ℝ≥0` and cast to `EReal`, is dividing `a` by `r`. This holds also for + `r = 0`, where both sides vanish. It converts between the forms `ε * log μ` and `log μ / r` of + the bounds of a large deviation principle with speed `ε = r⁻¹`. +-/ + +public section + +open scoped NNReal + +namespace EReal + +/-- Multiplying an extended real `a` by `r⁻¹`, for `r : ℝ≥0`, is dividing `a` by `r`, also for +`r = 0`, where both sides vanish. -/ +lemma coe_nnreal_inv_mul (r : ℝ≥0) (a : EReal) : + (((r⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / ((r : ℝ) : EReal) := by + rw [NNReal.coe_inv, EReal.coe_inv, EReal.div_eq_inv_mul] + +end EReal diff --git a/LMLExplore/Probability/LargeDeviations/Basic.lean b/LMLExplore/Probability/LargeDeviations/Basic.lean index 0a7e5073..3e2a1c55 100644 --- a/LMLExplore/Probability/LargeDeviations/Basic.lean +++ b/LMLExplore/Probability/LargeDeviations/Basic.lean @@ -7,12 +7,12 @@ module public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog public import Mathlib.Analysis.SpecialFunctions.Exp -public import Mathlib.Data.EReal.Inv public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef public import Mathlib.Order.LiminfLimsup public import Mathlib.Topology.Instances.EReal.Lemmas public import Mathlib.Topology.Semicontinuity.Defs public import TauCeti.Probability.LargeDeviations.Basic +public import LMLExplore.Data.EReal.Inv /-! # Large deviation principles @@ -76,12 +76,6 @@ open scoped ENNReal NNReal namespace LMLExplore -/-- The speed `1 / n` as a multiplier in `EReal` is a division by `n`, also for `n = 0`, where -both sides vanish. -/ -private lemma coe_inv_natCast_mul (n : ℕ) (a : EReal) : - (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / n := by - rw [NNReal.coe_inv, NNReal.coe_natCast, EReal.coe_inv, EReal.coe_natCast, EReal.div_eq_inv_mul] - /-! ### Exponential bounds -/ /-- The logarithm of `exp (-(n r))` is `-r n`, as an extended real. -/ @@ -119,7 +113,7 @@ lemma limsup_inv_mul_log_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ ∀ᶠ n : ℕ in atTop, u n ≤ C * ENNReal.ofReal (Real.exp (-(n * r)))) : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal) := by - simp_rw [coe_inv_natCast_mul] + simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] rw [EReal.le_neg] refine EReal.ge_of_forall_gt_iff_ge.1 fun r hr ↦ ?_ rw [EReal.le_neg] @@ -140,7 +134,7 @@ lemma neg_le_liminf_inv_mul_log_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ (h : ∀ r : ℝ, (c : EReal) < r → ∃ C : ℝ≥0∞, C ≠ 0 ∧ ∀ᶠ n : ℕ in atTop, C * ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n) : -(c : EReal) ≤ liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop := by - simp_rw [coe_inv_natCast_mul] + simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] rw [EReal.neg_le] refine EReal.le_of_forall_lt_iff_le.1 fun r hr ↦ ?_ rw [EReal.neg_le] @@ -164,7 +158,7 @@ lemma eventually_le_exp_of_limsup_inv_mul_log_le {u : ℕ → ℝ≥0∞} {c : (h : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal)) {r : ℝ} (hr : (r : EReal) < c) : ∀ᶠ n : ℕ in atTop, u n ≤ ENNReal.ofReal (Real.exp (-(n * r))) := by - simp_rw [coe_inv_natCast_mul] at h + simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h have h' : limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop < ((-r : ℝ) : EReal) := by rw [EReal.coe_neg] exact h.trans_lt (EReal.neg_lt_neg_iff.2 hr) @@ -181,7 +175,7 @@ lemma eventually_exp_le_of_neg_le_liminf_inv_mul_log {u : ℕ → ℝ≥0∞} {c liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop) {r : ℝ} (hr : (c : EReal) < r) : ∀ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n := by - simp_rw [coe_inv_natCast_mul] at h + simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h have h' : ((-r : ℝ) : EReal) < liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop := by rw [EReal.coe_neg] exact (EReal.neg_lt_neg_iff.2 hr).trans_le h From dbac84d4dd86e36e701c8d24b504b1dbf2474856 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 23:45:32 +0100 Subject: [PATCH 3/4] refactor: state the EReal inverse-multiplication lemma for every real MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalise EReal.coe_nnreal_inv_mul (r : ℝ≥0) to EReal.coe_inv_mul (x : ℝ), and rewrite with NNReal.coe_inv first at its use sites. Co-Authored-By: Claude Code --- LMLExplore/Data/EReal/Inv.lean | 21 ++++++++----------- .../Probability/LargeDeviations/Basic.lean | 8 +++---- 2 files changed, 13 insertions(+), 16 deletions(-) diff --git a/LMLExplore/Data/EReal/Inv.lean b/LMLExplore/Data/EReal/Inv.lean index 1adb9790..3d6f5323 100644 --- a/LMLExplore/Data/EReal/Inv.lean +++ b/LMLExplore/Data/EReal/Inv.lean @@ -8,26 +8,23 @@ module public import Mathlib.Data.EReal.Inv /-! -# Multiplying an extended real by the inverse of a nonnegative real +# Multiplying an extended real by the inverse of a real ## Main statements -* `EReal.coe_nnreal_inv_mul`: multiplying an extended real `a` by the inverse `r⁻¹` of a - nonnegative real, taken in `ℝ≥0` and cast to `EReal`, is dividing `a` by `r`. This holds also for - `r = 0`, where both sides vanish. It converts between the forms `ε * log μ` and `log μ / r` of - the bounds of a large deviation principle with speed `ε = r⁻¹`. +* `EReal.coe_inv_mul`: multiplying an extended real `a` by the inverse `x⁻¹` of a real, taken in + `ℝ` and cast to `EReal`, is dividing `a` by `x`. This holds also for `x = 0`, where both sides + vanish. It converts between the forms `ε * log μ` and `log μ / r` of the bounds of a large + deviation principle with speed `ε = r⁻¹`. -/ public section -open scoped NNReal - namespace EReal -/-- Multiplying an extended real `a` by `r⁻¹`, for `r : ℝ≥0`, is dividing `a` by `r`, also for -`r = 0`, where both sides vanish. -/ -lemma coe_nnreal_inv_mul (r : ℝ≥0) (a : EReal) : - (((r⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / ((r : ℝ) : EReal) := by - rw [NNReal.coe_inv, EReal.coe_inv, EReal.div_eq_inv_mul] +/-- Multiplying an extended real `a` by `x⁻¹`, for `x : ℝ`, is dividing `a` by `x`, also for +`x = 0`, where both sides vanish. -/ +lemma coe_inv_mul (x : ℝ) (a : EReal) : ((x⁻¹ : ℝ) : EReal) * a = a / (x : EReal) := by + rw [EReal.coe_inv, EReal.div_eq_inv_mul] end EReal diff --git a/LMLExplore/Probability/LargeDeviations/Basic.lean b/LMLExplore/Probability/LargeDeviations/Basic.lean index 3e2a1c55..13cce284 100644 --- a/LMLExplore/Probability/LargeDeviations/Basic.lean +++ b/LMLExplore/Probability/LargeDeviations/Basic.lean @@ -113,7 +113,7 @@ lemma limsup_inv_mul_log_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ ∀ᶠ n : ℕ in atTop, u n ≤ C * ENNReal.ofReal (Real.exp (-(n * r)))) : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal) := by - simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] + simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] rw [EReal.le_neg] refine EReal.ge_of_forall_gt_iff_ge.1 fun r hr ↦ ?_ rw [EReal.le_neg] @@ -134,7 +134,7 @@ lemma neg_le_liminf_inv_mul_log_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ (h : ∀ r : ℝ, (c : EReal) < r → ∃ C : ℝ≥0∞, C ≠ 0 ∧ ∀ᶠ n : ℕ in atTop, C * ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n) : -(c : EReal) ≤ liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop := by - simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] + simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] rw [EReal.neg_le] refine EReal.le_of_forall_lt_iff_le.1 fun r hr ↦ ?_ rw [EReal.neg_le] @@ -158,7 +158,7 @@ lemma eventually_le_exp_of_limsup_inv_mul_log_le {u : ℕ → ℝ≥0∞} {c : (h : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal)) {r : ℝ} (hr : (r : EReal) < c) : ∀ᶠ n : ℕ in atTop, u n ≤ ENNReal.ofReal (Real.exp (-(n * r))) := by - simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h + simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h have h' : limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop < ((-r : ℝ) : EReal) := by rw [EReal.coe_neg] exact h.trans_lt (EReal.neg_lt_neg_iff.2 hr) @@ -175,7 +175,7 @@ lemma eventually_exp_le_of_neg_le_liminf_inv_mul_log {u : ℕ → ℝ≥0∞} {c liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop) {r : ℝ} (hr : (c : EReal) < r) : ∀ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n := by - simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h + simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h have h' : ((-r : ℝ) : EReal) < liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop := by rw [EReal.coe_neg] exact (EReal.neg_lt_neg_iff.2 hr).trans_le h From de1fa536ec9c5b3551a7e857cfcdcea76499a900 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 00:05:41 +0100 Subject: [PATCH 4/4] refactor: name the speed `1 / n` conversion in one EReal lemma MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `EReal.coe_nnreal_inv_natCast_mul`, the case `x = n` of `EReal.coe_inv_mul` at HasLDP's speed `(n : ℝ≥0)⁻¹`, and use it in the four exponential-bound criteria instead of repeating a four-lemma chain. Co-Authored-By: Claude Code --- LMLExplore/Data/EReal/Inv.lean | 11 +++++++++++ LMLExplore/Probability/LargeDeviations/Basic.lean | 8 ++++---- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/LMLExplore/Data/EReal/Inv.lean b/LMLExplore/Data/EReal/Inv.lean index 3d6f5323..6564b80f 100644 --- a/LMLExplore/Data/EReal/Inv.lean +++ b/LMLExplore/Data/EReal/Inv.lean @@ -16,10 +16,14 @@ public import Mathlib.Data.EReal.Inv `ℝ` and cast to `EReal`, is dividing `a` by `x`. This holds also for `x = 0`, where both sides vanish. It converts between the forms `ε * log μ` and `log μ / r` of the bounds of a large deviation principle with speed `ε = r⁻¹`. +* `EReal.coe_nnreal_inv_natCast_mul`: the case of the speed `1 / n`, written `(n : ℝ≥0)⁻¹` as in + `TauCeti.Probability.HasLDP`: multiplying `a` by `(n : ℝ≥0)⁻¹` is dividing `a` by `n`. -/ public section +open scoped NNReal + namespace EReal /-- Multiplying an extended real `a` by `x⁻¹`, for `x : ℝ`, is dividing `a` by `x`, also for @@ -27,4 +31,11 @@ namespace EReal lemma coe_inv_mul (x : ℝ) (a : EReal) : ((x⁻¹ : ℝ) : EReal) * a = a / (x : EReal) := by rw [EReal.coe_inv, EReal.div_eq_inv_mul] +/-- Multiplying an extended real `a` by the speed `(n : ℝ≥0)⁻¹`, for `n : ℕ`, is dividing `a` +by `n`, also for `n = 0`, where both sides vanish. This is the form of the bounds of a large +deviation principle with speed `1 / n`. -/ +lemma coe_nnreal_inv_natCast_mul (n : ℕ) (a : EReal) : + (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / (n : EReal) := by + rw [NNReal.coe_inv, coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] + end EReal diff --git a/LMLExplore/Probability/LargeDeviations/Basic.lean b/LMLExplore/Probability/LargeDeviations/Basic.lean index 13cce284..0521e406 100644 --- a/LMLExplore/Probability/LargeDeviations/Basic.lean +++ b/LMLExplore/Probability/LargeDeviations/Basic.lean @@ -113,7 +113,7 @@ lemma limsup_inv_mul_log_le_neg_of_le_mul_exp {u : ℕ → ℝ≥0∞} {c : ℝ ∀ᶠ n : ℕ in atTop, u n ≤ C * ENNReal.ofReal (Real.exp (-(n * r)))) : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal) := by - simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] + simp_rw [EReal.coe_nnreal_inv_natCast_mul] rw [EReal.le_neg] refine EReal.ge_of_forall_gt_iff_ge.1 fun r hr ↦ ?_ rw [EReal.le_neg] @@ -134,7 +134,7 @@ lemma neg_le_liminf_inv_mul_log_of_mul_exp_le {u : ℕ → ℝ≥0∞} {c : ℝ (h : ∀ r : ℝ, (c : EReal) < r → ∃ C : ℝ≥0∞, C ≠ 0 ∧ ∀ᶠ n : ℕ in atTop, C * ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n) : -(c : EReal) ≤ liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop := by - simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] + simp_rw [EReal.coe_nnreal_inv_natCast_mul] rw [EReal.neg_le] refine EReal.le_of_forall_lt_iff_le.1 fun r hr ↦ ?_ rw [EReal.neg_le] @@ -158,7 +158,7 @@ lemma eventually_le_exp_of_limsup_inv_mul_log_le {u : ℕ → ℝ≥0∞} {c : (h : limsup (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop ≤ -(c : EReal)) {r : ℝ} (hr : (r : EReal) < c) : ∀ᶠ n : ℕ in atTop, u n ≤ ENNReal.ofReal (Real.exp (-(n * r))) := by - simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h + simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h have h' : limsup (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop < ((-r : ℝ) : EReal) := by rw [EReal.coe_neg] exact h.trans_lt (EReal.neg_lt_neg_iff.2 hr) @@ -175,7 +175,7 @@ lemma eventually_exp_le_of_neg_le_liminf_inv_mul_log {u : ℕ → ℝ≥0∞} {c liminf (fun n : ℕ ↦ (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * ENNReal.log (u n)) atTop) {r : ℝ} (hr : (c : EReal) < r) : ∀ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (-(n * r))) ≤ u n := by - simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] at h + simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h have h' : ((-r : ℝ) : EReal) < liminf (fun n : ℕ ↦ ENNReal.log (u n) / n) atTop := by rw [EReal.coe_neg] exact (EReal.neg_lt_neg_iff.2 hr).trans_le h