From a56f0b3d63d42c8ee2514493bd11bffb86fe2da6 Mon Sep 17 00:00:00 2001 From: Etienne Marion Date: Wed, 4 Mar 2026 10:36:19 +0000 Subject: [PATCH 1/2] bump --- Clt.lean | 2 - Clt/CLT.lean | 50 +++-------- Clt/CharFun.lean | 44 --------- Clt/Inversion.lean | 3 +- Clt/MomentGenerating.lean | 185 -------------------------------------- Clt/Tight.lean | 122 +------------------------ lake-manifest.json | 4 +- 7 files changed, 18 insertions(+), 392 deletions(-) delete mode 100644 Clt/CharFun.lean delete mode 100644 Clt/MomentGenerating.lean diff --git a/Clt.lean b/Clt.lean index cb02ab5..1bde9e4 100644 --- a/Clt.lean +++ b/Clt.lean @@ -1,7 +1,5 @@ import Clt.CLT -import Clt.CharFun import Clt.Inversion -import Clt.MomentGenerating import Clt.MultivariateGaussian import Clt.Prokhorov import Clt.Tight diff --git a/Clt/CLT.lean b/Clt/CLT.lean index d90dc92..48c33fe 100644 --- a/Clt/CLT.lean +++ b/Clt/CLT.lean @@ -6,7 +6,7 @@ Authors: Thomas Zhu, Rémy Degenne import Mathlib.Probability.Distributions.Gaussian.Real import Mathlib.Probability.IdentDistrib import Clt.Inversion -import Clt.MomentGenerating +import Mathlib.Probability.Independence.CharacteristicFunction /-! The Central Limit Theorem @@ -79,47 +79,21 @@ lemma charFun_invSqrtMulSum (hX : ∀ n, Measurable (X n)) {P : Measure Ω} [IsP (indep_fin n) have map_eq (n : ℕ) := (hident n).map_eq -- use existing results to rewrite the charFun - simp_rw [map_invSqrtMulSum P hX, charFun_map_mul, pi_fin, map_eq, charFun_map_sum_pi_const] - -lemma taylor_charFun_two' {X : Ω → ℝ} (hX : Measurable X) {P : Measure Ω} [IsProbabilityMeasure P] - (hint : Integrable (|·| ^ 2) (P.map X)) : - (fun t ↦ charFun (P.map X) t - (1 + P[X] * t * I - P[X ^ 2] * t ^ 2 / 2)) - =o[𝓝 0] fun t ↦ t ^ 2 := by - -- Apply Taylor's theorem to `charFun` - have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX.aemeasurable - have h := taylor_charFun hint - -- simplify the Taylor expansion - simp only [Nat.reduceAdd, ofReal_inv, ofReal_natCast, mul_pow, Finset.sum_range_succ, - Finset.range_one, Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, - mul_one, integral_const, probReal_univ, smul_eq_mul, ofReal_one, Nat.factorial_one, - pow_one, one_mul, Nat.factorial_two, Nat.cast_ofNat, I_sq, mul_neg, neg_mul] at h - have h1 : ∫ x, x ∂P.map X = P[X] := by - rw [integral_map hX.aemeasurable] - exact aestronglyMeasurable_id - have h2 : ∫ x, x ^ 2 ∂P.map X = P[X ^ 2] := by - rw [integral_map hX.aemeasurable] - · simp - · exact aestronglyMeasurable_id.pow 2 - simp only [h1, h2, Pi.pow_apply, ← sub_eq_add_neg] at h - simp only [integral_complex_ofReal, Pi.pow_apply, ← ofReal_pow] - simp only [ofReal_pow] - convert h using 4 with t - · ring - · ring + have := P.isProbabilityMeasure_map (hX 0).aemeasurable + simp_rw [map_invSqrtMulSum P hX, charFun_map_mul, pi_fin, map_eq, charFun_map_sum_pi_eq_prod] + simp lemma taylor_charFun_two {X : Ω → ℝ} (hX : Measurable X) {P : Measure Ω} [IsProbabilityMeasure P] (h0 : P[X] = 0) (h1 : P[X ^ 2] = 1) : (fun t ↦ charFun (P.map X) t - (1 - t ^ 2 / 2)) =o[𝓝 0] fun t ↦ t ^ 2 := by - have hint : Integrable (|·| ^ 2) (P.map X) := by - simp_rw [_root_.sq_abs] - apply Integrable.of_integral_ne_zero - erw [← integral_map hX.aemeasurable (aestronglyMeasurable_id.pow 2)] at h1 - simp only [Pi.pow_apply, id_eq] at h1 - simp [h1] - convert taylor_charFun_two' hX hint with t - · simp [integral_complex_ofReal, h0] - · simp only [Pi.pow_apply] at h1 - simp [← ofReal_pow, integral_complex_ofReal, h1] + simp_rw [← taylorWithinEval_charFun_two_zero' (by fun_prop) h0 h1] + convert taylor_isLittleO_univ ?_ + · simp + · refine contDiff_charFun ?_ + refine (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_) + rw [integral_map] + any_goals fun_prop + simp_all theorem central_limit (hX : ∀ n, Measurable (X n)) {P : ProbabilityMeasure Ω} (h0 : P[X 0] = 0) (h1 : P[X 0 ^ 2] = 1) diff --git a/Clt/CharFun.lean b/Clt/CharFun.lean deleted file mode 100644 index 0f63076..0000000 --- a/Clt/CharFun.lean +++ /dev/null @@ -1,44 +0,0 @@ -/- -Copyright (c) 2023 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne, Thomas Zhu --/ -import Mathlib.MeasureTheory.Measure.CharacteristicFunction - -/-! -# Characteristic function of a measure - --/ - -open MeasureTheory - -namespace ProbabilityTheory - -variable {E : Type*} [MeasurableSpace E] {μ ν : Measure E} {t : E} - [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] - -/-- -The characteristic function of the sum of `n` i.i.d. variables with characteristic function `f` is -`f ^ n`. - -We express this in terms of the pushforward of $P^{\otimes n}$ by summation. - -(A more general version not assuming identical distribution is possible) - -(Should I express this using pushforward of `iIndepFun` etc?) --/ -lemma charFun_map_sum_pi_const (μ : Measure E) [IsFiniteMeasure μ] (n : ℕ) (t : E) : - charFun ((Measure.pi fun (_ : Fin n) ↦ μ).map fun x ↦ ∑ i, x i) t = charFun μ t ^ n := by - induction n with - | zero => simp [Measure.map_const, charFun_apply] - | succ n ih => - rw [pow_succ', ← ih, ← charFun_conv] - congr 1 - have h := (measurePreserving_piFinSuccAbove (fun (_ : Fin (n + 1)) ↦ μ) 0).map_eq - nth_rw 2 [← μ.map_id] - rw [Measure.conv, Measure.map_prod_map, ← h, Measure.map_map, Measure.map_map] - · congr 1 with x - apply Fin.sum_univ_succ - all_goals { fun_prop } - -end ProbabilityTheory diff --git a/Clt/Inversion.lean b/Clt/Inversion.lean index 946be58..9a3f057 100644 --- a/Clt/Inversion.lean +++ b/Clt/Inversion.lean @@ -3,10 +3,11 @@ Copyright (c) 2024 Thomas Zhu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Zhu, Rémy Degenne -/ -import Clt.MomentGenerating +-- import Clt.MomentGenerating import Clt.Prokhorov import Clt.Tight import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric +import Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion /-! Inverting the characteristic function diff --git a/Clt/MomentGenerating.lean b/Clt/MomentGenerating.lean deleted file mode 100644 index 729e5d3..0000000 --- a/Clt/MomentGenerating.lean +++ /dev/null @@ -1,185 +0,0 @@ -/- -Copyright (c) 2024 Thomas Zhu. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Zhu, Rémy Degenne --/ -import Mathlib.Analysis.Calculus.Taylor -import Mathlib.Analysis.Fourier.FourierTransformDeriv -import Clt.CharFun - -/-! -The characteristic function is moment generating. - -Still depends on: Peano form of Taylor's theorem (TODO: is there code for X) --/ - -section Taylor - -open Set -open scoped Topology - -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] - -theorem taylor_isLittleO_univ {f : ℝ → E} {x₀ : ℝ} {n : ℕ} (hf : ContDiff ℝ n f) : - (fun x ↦ f x - taylorWithinEval f n univ x₀ x) =o[𝓝 x₀] fun x ↦ (x - x₀) ^ n := by - suffices (fun x ↦ f x - taylorWithinEval f n univ x₀ x) =o[𝓝[univ] x₀] fun x ↦ (x - x₀) ^ n by - simpa - refine taylor_isLittleO (s := univ) convex_univ (mem_univ _) ?_ - simpa [contDiffOn_univ] using hf - -end Taylor - -open MeasureTheory ProbabilityTheory Complex -open scoped Nat Real NNReal ENNReal Topology RealInnerProductSpace - -section ForMathlib - -lemma integrable_norm_rpow_antitone {α} [MeasurableSpace α] - (μ : Measure α) [IsFiniteMeasure μ] - {E} [NormedAddCommGroup E] {f : α → E} (hf : AEStronglyMeasurable f μ) - {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p ≤ q) - (hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ) : - Integrable (fun x ↦ ‖f x‖ ^ p) μ := by - rcases hp.eq_or_lt with (rfl | hp) - · simp - rcases hq.eq_or_lt with (rfl | hq) - · exact (hp.not_ge hpq).elim - revert hint - convert fun h ↦ MemLp.mono_exponent h (ENNReal.ofReal_le_ofReal hpq) using 1 - · rw [← integrable_norm_rpow_iff hf, ENNReal.toReal_ofReal hq.le] <;> simp_all - · rw [← integrable_norm_rpow_iff hf, ENNReal.toReal_ofReal hp.le] <;> simp_all - · infer_instance - -lemma integrable_norm_pow_antitone {α} [MeasurableSpace α] - (μ : Measure α) [IsFiniteMeasure μ] - {E} [NormedAddCommGroup E] {f : α → E} (hf : AEStronglyMeasurable f μ) - {p q : ℕ} (hpq : p ≤ q) - (hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ) : - Integrable (fun x ↦ ‖f x‖ ^ p) μ := by - revert hint - replace hpq : (p : ℝ) ≤ q := by simpa - convert integrable_norm_rpow_antitone μ hf - p.cast_nonneg q.cast_nonneg hpq <;> rw [Real.rpow_natCast] - -end ForMathlib - -section InnerProductSpace - -/-! -The `n`th derivative of `charFun μ`. -The proof uses results on iterated derivatives of the Fourier transform. --/ - - -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] - [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] - {μ : Measure E} [IsProbabilityMeasure μ] - -set_option backward.isDefEq.respectTransparency false -@[fun_prop] -theorem contDiff_charFun - {n : ℕ} (hint : Integrable (‖·‖ ^ n) μ) : - ContDiff ℝ n (charFun μ) := by - have hint' (k : ℕ) (hk : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ ‖x‖ ^ k * ‖(1 : E → ℂ) x‖) μ := by - simp only [Pi.one_apply, norm_one, mul_one] - rw [Nat.cast_le] at hk - exact integrable_norm_pow_antitone μ aestronglyMeasurable_id hk hint - simp_rw [funext charFun_eq_fourierIntegral'] - refine (VectorFourier.contDiff_fourierIntegral (L := innerSL ℝ) hint').comp ?_ - exact contDiff_const_smul _ - -@[fun_prop] -lemma continuous_charFun : Continuous (charFun μ) := by - rw [← contDiff_zero (𝕜 := ℝ)] - refine contDiff_charFun ?_ - suffices Integrable (fun _ ↦ (1 : ℝ)) μ by convert this - fun_prop - -end InnerProductSpace - -variable {μ : Measure ℝ} [IsProbabilityMeasure μ] - -set_option backward.isDefEq.respectTransparency false -open VectorFourier in -theorem iteratedDeriv_charFun {n : ℕ} {t : ℝ} (hint : Integrable (|·| ^ n) μ) : - iteratedDeriv n (charFun μ) t = I ^ n * ∫ x, x ^ n * exp (t * x * I) ∂μ := by - have h : innerₗ ℝ = (ContinuousLinearMap.mul ℝ ℝ).toLinearMap₁₂ := by ext; rfl - have hint' (k : ℕ) (hk : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ ‖x‖ ^ k * ‖(1 : ℝ → ℂ) x‖) μ := by - simp only [Pi.one_apply, norm_one, mul_one] - rw [Nat.cast_le] at hk - exact integrable_norm_pow_antitone μ aestronglyMeasurable_id hk hint - simp_rw [funext charFun_eq_fourierIntegral', smul_eq_mul] - rw [iteratedDeriv_comp_const_smul] - · dsimp only - simp only [mul_inv_rev, neg_mul] - rw [h, iteratedDeriv, iteratedFDeriv_fourierIntegral _ hint'] - · rw [fourierIntegral_continuousMultilinearMap_apply] - · unfold fourierIntegral Real.fourierChar Circle.exp - simp only [ContinuousMap.coe_mk, ofReal_mul, ofReal_ofNat, - ContinuousLinearMap.toLinearMap₁₂_apply, ContinuousLinearMap.mul_apply', mul_neg, neg_neg, - AddChar.coe_mk, ofReal_inv, fourierPowSMulRight_apply, mul_one, Finset.prod_const, - Finset.card_univ, Fintype.card_fin, Pi.one_apply, real_smul, ofReal_pow, smul_eq_mul, - Circle.smul_def, ofReal_neg] - simp_rw [mul_left_comm (exp _), integral_const_mul] - calc (-((↑π)⁻¹ * 2⁻¹)) ^ n - * ((-(2 * ↑π * I)) ^ n * ∫ a, cexp (2 * ↑π * (↑a * ((↑π)⁻¹ * 2⁻¹ * ↑t)) * I) * ↑a ^ n ∂μ) - _ = I ^ n * ∫ a, cexp (2 * ↑π * (↑a * ((↑π)⁻¹ * 2⁻¹ * ↑t)) * I) * ↑a ^ n ∂μ := by - rw [← mul_assoc] - congr - rw [← mul_pow] - ring_nf - -- `⊢ ↑π ^ n * (↑π)⁻¹ ^ n * I ^ n = I ^ n` - rw [inv_pow, mul_inv_cancel₀, one_mul] - norm_cast - positivity - _ = I ^ n * ∫ x, ↑x ^ n * cexp (↑t * ↑x * I) ∂μ := by - simp_rw [mul_comm ((_ : ℂ) ^ n)] - congr with x - congr 2 - ring_nf - congr 2 - -- `⊢ ↑π * ↑x * (↑π)⁻¹ = ↑x` - rw [mul_comm, ← mul_assoc, inv_mul_cancel₀, one_mul] - norm_cast - positivity - · exact Real.continuous_fourierChar - · apply integrable_fourierPowSMulRight - · simpa - · exact aestronglyMeasurable_one - · exact aestronglyMeasurable_one - · rfl - · rw [h] - exact contDiff_fourierIntegral _ hint' - -theorem iteratedDeriv_charFun_zero {n : ℕ} (hint : Integrable (|·| ^ n) μ) : - iteratedDeriv n (charFun μ) 0 = I ^ n * ∫ x, x ^ n ∂μ := by - simp only [iteratedDeriv_charFun hint, ofReal_zero, zero_mul, exp_zero, mul_one, - mul_eq_mul_left_iff, pow_eq_zero_iff', I_ne_zero, ne_eq, false_and, or_false] - norm_cast - -- maybe this should have been done by norm_cast? - exact integral_ofReal - -lemma taylorWithinEval_charFun_zero {n : ℕ} (hint : Integrable (|·| ^ n) μ) (t : ℝ): - taylorWithinEval (charFun μ) n Set.univ 0 t - = ∑ k ∈ Finset.range (n + 1), (k ! : ℂ)⁻¹ * (t * I) ^ k * ∫ x, x ^ k ∂μ := by - simp_rw [taylor_within_apply, sub_zero, RCLike.real_smul_eq_coe_mul] - refine Finset.sum_congr rfl fun k hkn ↦ ?_ - push_cast - have hint' : Integrable (fun x ↦ |x| ^ k) μ := - integrable_norm_pow_antitone μ aestronglyMeasurable_id (Finset.mem_range_succ_iff.mp hkn) hint - rw [iteratedDerivWithin, - iteratedFDerivWithin_eq_iteratedFDeriv uniqueDiffOn_univ _ (Set.mem_univ _), - ← iteratedDeriv, iteratedDeriv_charFun_zero hint'] - · simp [mul_pow, mul_comm, mul_assoc, mul_left_comm] - · exact (contDiff_charFun hint').contDiffAt - -theorem taylor_charFun {n : ℕ} (hint : Integrable (|·| ^ n) μ) : - (fun t ↦ charFun μ t - ∑ k ∈ Finset.range (n + 1), (k ! : ℝ)⁻¹ * (t * I) ^ k * ∫ x, x ^ k ∂μ) - =o[𝓝 0] fun t ↦ t ^ n := by - have : (fun x ↦ charFun μ x - taylorWithinEval (charFun μ) n Set.univ 0 x) - =o[𝓝 0] fun x ↦ x ^ n :=by - convert taylor_isLittleO_univ (contDiff_charFun hint) - simp_rw [sub_zero] - convert this with t - push_cast - exact (taylorWithinEval_charFun_zero hint t).symm diff --git a/Clt/Tight.lean b/Clt/Tight.lean index 8c4cc7c..d862327 100644 --- a/Clt/Tight.lean +++ b/Clt/Tight.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne -/ import Mathlib.MeasureTheory.Measure.IntegralCharFun import Mathlib.MeasureTheory.Measure.TightNormed -import Clt.CharFun /-! # Tightness and characteristic functions @@ -15,140 +14,23 @@ import Clt.CharFun open MeasureTheory ProbabilityTheory Filter open scoped ENNReal NNReal Topology RealInnerProductSpace -lemma tendsto_iSup_of_tendsto_limsup {u : ℕ → ℝ → ℝ≥0∞} - (h_all : ∀ n, Tendsto (u n) atTop (𝓝 0)) - (h_tendsto : Tendsto (fun r : ℝ ↦ limsup (fun n ↦ u n r) atTop) atTop (𝓝 0)) - (h_anti : ∀ n, Antitone (u n)) : - Tendsto (fun r : ℝ ↦ ⨆ n, u n r) atTop (𝓝 0) := by - simp_rw [ENNReal.tendsto_atTop_zero] at h_tendsto h_all ⊢ - intro ε hε - by_cases hε_top : ε = ∞ - · refine ⟨0, fun _ _ ↦ by simp [hε_top]⟩ - simp only [gt_iff_lt, ge_iff_le] at h_tendsto h_all hε - obtain ⟨r, h⟩ := h_tendsto (ε / 2) (ENNReal.half_pos hε.ne') - have h' x (hx : r ≤ x) y (hy : ε / 2 < y) : ∀ᶠ n in atTop, u n x < y := by - specialize h x hx - rw [limsup_le_iff] at h - exact h y hy - replace h' : ∀ x, r ≤ x → ∀ᶠ n in atTop, u n x < ε := - fun x hx ↦ h' x hx ε (ENNReal.half_lt_self hε.ne' hε_top) - simp only [eventually_atTop, ge_iff_le] at h' - obtain ⟨N, h⟩ := h' r le_rfl - replace h_all : ∀ ε > 0, ∀ n, ∃ N, ∀ n_1 ≥ N, u n n_1 ≤ ε := fun ε hε n ↦ h_all n ε hε - choose rs hrs using h_all ε hε - refine ⟨r ⊔ ⨆ n : Finset.range N, rs n, fun v hv ↦ ?_⟩ - simp only [iSup_le_iff] - intro n - by_cases hn : n < N - · refine hrs n v ?_ - calc rs n - _ = rs (⟨n, by simp [hn]⟩ : Finset.range N) := rfl - _ ≤ ⨆ n : Finset.range N, rs n := by - refine le_ciSup (f := fun (x : Finset.range N) ↦ rs x) ?_ (⟨n, by simp [hn]⟩ : Finset.range N) - exact Finite.bddAbove_range _ - _ ≤ r ⊔ ⨆ n : Finset.range N, rs n := le_max_right _ _ - _ ≤ v := hv - · have hn_le : N ≤ n := not_lt.mp hn - specialize h n hn_le - refine (h_anti n ?_).trans h.le - calc r - _ ≤ r ⊔ ⨆ n : Finset.range N, rs n := le_max_left _ _ - _ ≤ v := hv - variable {E : Type*} {mE : MeasurableSpace E} [NormedAddCommGroup E] section FiniteDimensional variable [BorelSpace E] {μ : ℕ → Measure E} [∀ i, IsFiniteMeasure (μ i)] -section NormedSpace - -variable [NormedSpace ℝ E] [FiniteDimensional ℝ E] - -lemma isTightMeasureSet_of_tendsto_limsup_measure_norm_gt - (h : Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop) atTop (𝓝 0)) : - IsTightMeasureSet (Set.range μ) := by - refine isTightMeasureSet_of_tendsto_measure_norm_gt ?_ - simp_rw [iSup_range] - refine tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) h fun n u v huv ↦ ?_ - · have h_tight : IsTightMeasureSet {μ n} := isTightMeasureSet_singleton - rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h_tight - simpa using h_tight - · refine measure_mono fun x hx ↦ ?_ - simp only [Set.mem_setOf_eq] at hx ⊢ - exact huv.trans_lt hx - -lemma isTightMeasureSet_iff_tendsto_limsup_measure_norm_gt : - IsTightMeasureSet (Set.range μ) - ↔ Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop) atTop (𝓝 0) := by - refine ⟨fun h ↦ ?_, isTightMeasureSet_of_tendsto_limsup_measure_norm_gt⟩ - have h_sup := tendsto_measure_norm_gt_of_isTightMeasureSet h - refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h_sup (fun _ ↦ zero_le _) ?_ - intro r - simp_rw [iSup_range] - exact limsup_le_iSup - -end NormedSpace - section InnerProductSpace variable [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] -lemma isTightMeasureSet_of_tendsto_limsup_inner - (h : ∀ z, Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | r < |⟪z, x⟫|}) atTop) atTop (𝓝 0)) : - IsTightMeasureSet (Set.range μ) := by - refine isTightMeasureSet_of_inner_tendsto (𝕜 := ℝ) fun z ↦ ?_ - simp_rw [iSup_range] - refine tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) (h z) fun n u v huv ↦ ?_ - · have h_tight : IsTightMeasureSet {(μ n).map (fun x ↦ ⟪z, x⟫)} := isTightMeasureSet_singleton - rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h_tight - have h_map r : (μ n).map (fun x ↦ ⟪z, x⟫) {x | r < |x|} = μ n {x | r < |⟪z, x⟫|} := by - rw [Measure.map_apply (by fun_prop)] - · simp - · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop) - simpa [h_map] using h_tight - · exact measure_mono fun x hx ↦ huv.trans_lt hx - -lemma isTightMeasureSet_iff_tendsto_limsup_inner : - IsTightMeasureSet (Set.range μ) - ↔ ∀ z, Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | r < |⟪z, x⟫|}) atTop) atTop (𝓝 0) := by - refine ⟨fun h z ↦ ?_, isTightMeasureSet_of_tendsto_limsup_inner⟩ - rw [isTightMeasureSet_iff_inner_tendsto ℝ] at h - refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h z) - (fun _ ↦ zero_le _) fun r ↦ ?_ - simp_rw [iSup_range] - exact limsup_le_iSup - -lemma isTightMeasureSet_of_tendsto_limsup_inner_of_norm_eq_one - (h : ∀ z, ‖z‖ = 1 - → Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | r < |⟪z, x⟫|}) atTop) atTop (𝓝 0)) : - IsTightMeasureSet (Set.range μ) := by - have : ProperSpace E := FiniteDimensional.proper ℝ E - refine isTightMeasureSet_of_tendsto_limsup_inner fun y ↦ ?_ - by_cases hy : y = 0 - · simp only [hy, inner_zero_left, abs_zero] - refine (tendsto_congr' ?_).mpr tendsto_const_nhds - filter_upwards [eventually_ge_atTop 0] with r hr - simp [not_lt.mpr hr] - have h' : Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | ‖y‖⁻¹ * r < |⟪‖y‖⁻¹ • y, x⟫|}) atTop) - atTop (𝓝 0) := by - specialize h (‖y‖⁻¹ • y) ?_ - · simp only [norm_smul, norm_inv, norm_norm] - rw [inv_mul_cancel₀ (by positivity)] - exact h.comp <| (tendsto_const_mul_atTop_of_pos (by positivity)).mpr tendsto_id - convert h' using 7 with r n x - rw [inner_smul_left] - simp only [map_inv₀, conj_trivial, abs_mul, abs_inv, abs_norm] - rw [mul_lt_mul_iff_right₀] - positivity - /-- If the characteristic functions converge pointwise to a function which is continuous at 0, then `{μ n | n}` is tight. -/ lemma isTightMeasureSet_of_tendsto_charFun {μ : ℕ → Measure E} [∀ i, IsProbabilityMeasure (μ i)] {f : E → ℂ} (hf : ContinuousAt f 0) (hf_meas : Measurable f) (h : ∀ t, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))) : IsTightMeasureSet (Set.range μ) := by - refine isTightMeasureSet_of_tendsto_limsup_inner_of_norm_eq_one fun z hz ↦ ?_ + refine isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one ℝ fun z hz ↦ ?_ suffices Tendsto (fun r : ℝ ↦ limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop) atTop (𝓝 0) by have h_ofReal r : limsup (fun n ↦ μ n {x | r < |⟪z, x⟫|}) atTop = ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop) := by @@ -158,7 +40,7 @@ lemma isTightMeasureSet_of_tendsto_charFun {μ : ℕ → Measure E} [∀ i, IsPr refine ne_top_of_le_ne_top (by simp : 1 ≠ ∞) ?_ refine limsup_le_of_le ?_ (.of_forall fun _ ↦ prob_le_one) exact IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ zero_le _ - simp_rw [h_ofReal] + simp_rw [Real.norm_eq_abs, h_ofReal] rw [← ENNReal.ofReal_zero] exact ENNReal.tendsto_ofReal this have h_le_4 n r (hr : 0 < r) : diff --git a/lake-manifest.json b/lake-manifest.json index 7cf0a3e..d4d601c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c71e03699b96d33cf3847760172921163748a1d4", + "rev": "bf8875c7dc7162b23cdb881f33cc97caab1c688a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed250d06b33e67aa5dc5f2cc349a5a35e8b6b390", + "rev": "8b4f32c03c788181a4ee3f00130c130e6317ccc9", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 853f6bc24472e91592d083cf1fb49026279f3466 Mon Sep 17 00:00:00 2001 From: Etienne Marion Date: Wed, 4 Mar 2026 10:37:03 +0000 Subject: [PATCH 2/2] detail --- Clt/Inversion.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Clt/Inversion.lean b/Clt/Inversion.lean index 9a3f057..d08aebd 100644 --- a/Clt/Inversion.lean +++ b/Clt/Inversion.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Thomas Zhu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Zhu, Rémy Degenne -/ --- import Clt.MomentGenerating import Clt.Prokhorov import Clt.Tight import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric