From 8014c15e9db7d2b7f05122255d9c948912a620b3 Mon Sep 17 00:00:00 2001 From: Sebastien Gouezel Date: Sat, 27 Dec 2025 17:36:19 +0100 Subject: [PATCH 1/2] use innerSL --- Clt/Inversion.lean | 12 ++++++------ Clt/MomentGenerating.lean | 24 ++---------------------- lake-manifest.json | 4 ++-- 3 files changed, 10 insertions(+), 30 deletions(-) diff --git a/Clt/Inversion.lean b/Clt/Inversion.lean index f6a2f52..da7344d 100644 --- a/Clt/Inversion.lean +++ b/Clt/Inversion.lean @@ -52,12 +52,12 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] lemma MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun (h : ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t))) {g : E →ᵇ ℂ} - (hg : g ∈ charPoly continuous_probChar (L := bilinFormOfRealInner) continuous_inner) : + (hg : g ∈ charPoly continuous_probChar (L := innerₗ E) continuous_inner) : Tendsto (fun n ↦ ∫ x, g x ∂(μ n)) atTop (𝓝 (∫ x, g x ∂μ₀)) := by rw [mem_charPoly] at hg obtain ⟨w, hw⟩ := hg have h_eq (μ : Measure E) (hμ : IsProbabilityMeasure μ) : - ∫ x, g x ∂μ = ∑ a ∈ w.support, w a * ∫ x, (probChar (bilinFormOfRealInner x a) : ℂ) ∂μ := by + ∫ x, g x ∂μ = ∑ a ∈ w.support, w a * ∫ x, (probChar (innerₗ E x a) : ℂ) ∂μ := by simp_rw [hw] rw [integral_finset_sum] · congr with y @@ -68,18 +68,18 @@ lemma MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun exact BoundedContinuousFunction.integrable μ _ simp_rw [h_eq (μ _), h_eq μ₀] refine tendsto_finset_sum _ fun y hy ↦ Tendsto.const_mul _ ?_ - simp only [bilinFormOfRealInner_apply_apply] + simp only [innerₗ_apply_apply] simp_rw [← charFun_eq_integral_probChar] exact h y lemma MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun - [CompleteSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] + [FiniteDimensional ℝ E] (h : ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t))) : Tendsto μ atTop (𝓝 μ₀) := by have h_tight : IsTightMeasureSet (𝓧 := E) {μ n | n} := isTightMeasureSet_of_tendsto_charFun (by fun_prop) (by fun_prop) h refine tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ) - (A := charPoly continuous_probChar (L := bilinFormOfRealInner) continuous_inner) ?_ ?_ + (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_ · refine separatesPoints_charPoly continuous_probChar probChar_ne_one _ ?_ exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩ · exact fun g ↦ tendsto_charPoly_of_tendsto_charFun h @@ -98,7 +98,7 @@ The => direction is much harder: -/ theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun - [CompleteSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] : + [FiniteDimensional ℝ E] : Tendsto μ atTop (𝓝 μ₀) ↔ ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t)) := by refine ⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩ diff --git a/Clt/MomentGenerating.lean b/Clt/MomentGenerating.lean index b1ea905..685a47c 100644 --- a/Clt/MomentGenerating.lean +++ b/Clt/MomentGenerating.lean @@ -67,25 +67,6 @@ section InnerProductSpace variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] -/-! -The `n`th derivative of `charFun μ`. -The proof uses results on iterated derivatives of the Fourier transform. --/ - -/-- The scalar product as a continuous bilinear map. -TODO: this is already in Mathlib, as `innerSL ℝ`. Use that instead. -/ -noncomputable -def continuousBilinFormOfInner : E →L[ℝ] E →L[ℝ] ℝ := - (isBoundedBilinearMap_inner (𝕜 := ℝ)).toContinuousLinearMap - -@[simp] -lemma continuousBilinFormOfInner_apply {x y : E} : continuousBilinFormOfInner x y = ⟪x, y⟫ := rfl - -@[simp] -lemma toLinearMap₂_continuousBilinFormOfInner : - ContinuousLinearMap.toLinearMap₁₂ (continuousBilinFormOfInner : E →L[ℝ] E →L[ℝ] ℝ) - = bilinFormOfRealInner := rfl - variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsProbabilityMeasure μ] @@ -98,8 +79,7 @@ theorem contDiff_charFun rw [Nat.cast_le] at hk exact integrable_norm_pow_antitone μ aestronglyMeasurable_id hk hint simp_rw [funext charFun_eq_fourierIntegral'] - rw [← toLinearMap₂_continuousBilinFormOfInner] - refine (VectorFourier.contDiff_fourierIntegral (L := continuousBilinFormOfInner) hint').comp ?_ + refine (VectorFourier.contDiff_fourierIntegral (L := innerSL ℝ) hint').comp ?_ exact contDiff_const_smul _ @[fun_prop] @@ -116,7 +96,7 @@ variable {μ : Measure ℝ} [IsProbabilityMeasure μ] 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 : bilinFormOfRealInner = (ContinuousLinearMap.mul ℝ ℝ).toLinearMap₁₂ := by ext; rfl + 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 diff --git a/lake-manifest.json b/lake-manifest.json index 0669309..228dfe7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "26440c825575eea64509c91cf9e1ab3ede95de9b", + "rev": "a36c84ab8236a4869899268a42a44af07daa21ed", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dff865b7ee7011518d59abfc101c368293173150", + "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 203e468f781513dfc046db15b475b3011aef48ec Mon Sep 17 00:00:00 2001 From: Sebastien Gouezel Date: Sat, 27 Dec 2025 17:39:28 +0100 Subject: [PATCH 2/2] oops --- Clt/MomentGenerating.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Clt/MomentGenerating.lean b/Clt/MomentGenerating.lean index 685a47c..0685b0c 100644 --- a/Clt/MomentGenerating.lean +++ b/Clt/MomentGenerating.lean @@ -65,9 +65,14 @@ end ForMathlib section InnerProductSpace -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] +/-! +The `n`th derivative of `charFun μ`. +The proof uses results on iterated derivatives of the Fourier transform. +-/ -variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsProbabilityMeasure μ] @[fun_prop]