From d2c58d15a007c71b864bded6e9b3577ecef7b418 Mon Sep 17 00:00:00 2001
From: Komyyy <pol_tta@outlook.jp>
Date: Sun, 11 Jan 2026 21:33:36 +0900
Subject: [PATCH 1/2] feat: prove theorem 6.7

---
 Clt/Inversion.lean            | 32 ++++++++++++++++++++++++++++----
 blueprint/lean_decls          |  1 +
 blueprint/src/chapter/clt.tex |  2 ++
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/Clt/Inversion.lean b/Clt/Inversion.lean
index da7344d..e148181 100644
--- a/Clt/Inversion.lean
+++ b/Clt/Inversion.lean
@@ -1,7 +1,7 @@
 /-
 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
+Authors: Thomas Zhu, Rémy Degenne, Miyahara Kō
 -/
 import Clt.MomentGenerating
 import Clt.Prokhorov
@@ -14,9 +14,22 @@ Inverting the characteristic function
 
 noncomputable section
 
-open Filter MeasureTheory ProbabilityTheory BoundedContinuousFunction Real RCLike
+open Function Filter MeasureTheory ProbabilityMeasure ProbabilityTheory BoundedContinuousFunction
+  Real RCLike
 open scoped Topology RealInnerProductSpace
 
+section ForMathlib
+
+lemma MeasureTheory.charFun_map_inner_right
+    {E : Type*} {mE : MeasurableSpace E} {μ : Measure E}
+    [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E]
+    (r : ℝ) (t : E) :
+    charFun (μ.map (fun (x : E) => ⟪x, t⟫)) r = charFun μ (r • t) := by
+  rw [charFun_apply_real, charFun_apply, integral_map (by fun_prop) (by fun_prop)]
+  simp [real_inner_smul_right]
+
+end ForMathlib
+
 variable (𝕜 : Type*) [RCLike 𝕜]
 
 lemma MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints
@@ -42,7 +55,7 @@ lemma MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints
   specialize heq g hg
   suffices Tendsto (fun n ↦ ∫ x, g x ∂(μ (ns (φ n)))) atTop (𝓝 (∫ x, g x ∂μ')) from
     tendsto_nhds_unique this <| heq.comp (hns.comp hφ_mono.tendsto_atTop)
-  rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto 𝕜] at hφ_tendsto
+  rw [tendsto_iff_forall_integral_rclike_tendsto 𝕜] at hφ_tendsto
   exact hφ_tendsto g
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
@@ -102,6 +115,17 @@ theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun
     Tendsto μ atTop (𝓝 μ₀) ↔
       ∀ t : E, Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (charFun μ₀ t)) := by
   refine ⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩
-  rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ] at h
+  rw [tendsto_iff_forall_integral_rclike_tendsto ℂ] at h
   simp_rw [charFun_eq_integral_innerProbChar]
   exact h (innerProbChar t)
+
+lemma ProbabilityTheory.tendsto_iff_forall_tendto_inner_right
+    {E : Type*} {mE : MeasurableSpace E}
+    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
+    {P : ℕ → ProbabilityMeasure E} {P₀ : ProbabilityMeasure E} :
+    Tendsto P atTop (𝓝 P₀) ↔
+      ∀ a, Tendsto (fun n => (P n).map (f := fun x => ⟪x, a⟫) (by fun_prop))
+        atTop (𝓝 (P₀.map (f := fun x => ⟪x, a⟫) (by fun_prop))) := by
+  simp_rw [tendsto_iff_tendsto_charFun, toMeasure_map, charFun_map_inner_right]
+  rw [forall_comm, ← Prod.forall',
+    (show Surjective (fun p : ℝ × E => p.1 • p.2) by intro a; use (1, a); simp).forall]
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 4fb071d..751115b 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -42,4 +42,5 @@ taylor_isLittleO
 ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
 taylor_charFun
 tendsto_pow_exp_of_isLittleO
+ProbabilityTheory.tendsto_iff_forall_tendto_inner_right
 ProbabilityTheory.central_limit
\ No newline at end of file
diff --git a/blueprint/src/chapter/clt.tex b/blueprint/src/chapter/clt.tex
index b6ea7f3..add3d7d 100644
--- a/blueprint/src/chapter/clt.tex
+++ b/blueprint/src/chapter/clt.tex
@@ -87,6 +87,8 @@ \section{The central limit theorem for random variables in $\mathbb{R}^d$}
 
 \begin{theorem}[Cramér-Wold]\label{thm:cramer_wold}
     \uses{def:cvg_distribution}
+    \leanok
+    \lean{ProbabilityTheory.tendsto_iff_forall_tendto_inner_right}
 Let $X, X_1, X_2, \ldots$ be random variables in $\mathbb{R}^d$.
 Then $X_n \xrightarrow{d} X$ iff for every $a \in \mathbb{R}^d$, $\langle a, X_n \rangle \xrightarrow{d} \langle a, X \rangle$.
 \end{theorem}

From f769fb26214cb967a1c2936876b5cf6cd2ec42a2 Mon Sep 17 00:00:00 2001
From: Komyyy <pol_tta@outlook.jp>
Date: Sun, 11 Jan 2026 23:26:59 +0900
Subject: [PATCH 2/2] chore: sort `lean_decls

---
 blueprint/lean_decls | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 751115b..d45b33b 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -42,5 +42,5 @@ taylor_isLittleO
 ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
 taylor_charFun
 tendsto_pow_exp_of_isLittleO
-ProbabilityTheory.tendsto_iff_forall_tendto_inner_right
-ProbabilityTheory.central_limit
\ No newline at end of file
+ProbabilityTheory.central_limit
+ProbabilityTheory.tendsto_iff_forall_tendto_inner_right
\ No newline at end of file