LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite-dimensional LAN convolution bound for differentiable functionals

Statement

Assume AC and let $d, k \geq 1$ be finite. Let ${P_{n, h} : h \in R^{d}}$ be LAN at $h = 0$ with positive-definite information matrix $K$ and central sequence $Δ_{n}$ . Let $ψ_{n, h} \in R^{k}$ be a local target such that for every fixed $h$ ,

$δ_{n} (h) : = \sqrt{n} (ψ_{n, h} - ψ_{n, 0}) ⟶ D h$

for a fixed matrix $D \in R^{k \times d}$ . Suppose $T_{n} = \sqrt{n} ({\hat{ψ}}_{n} - ψ_{n, 0})$ is regular for this target: under each fixed $P_{n, h}$ , $T_{n} - δ_{n} (h) \Rightarrow W$ for the same Borel law $W$ . Then there is a probability law $ν$ on $R^{k}$ such that

$L (W) = N_{k} (0, D K^{- 1} D^{T}) * ν .$

The Gaussian covariance may be singular. No finite-moment hypothesis on $W$ or $ν$ is needed.

Facts & Assumptions

Given: AC; the finite-dimensional LAN experiment, positive-definite $K$ , central sequence $Δ_{n}$ ; the local target derivative matrix $D$ ; and a regular estimator with common limit law $W$ .

[F1]

Local asymptotic normality for local experiments: for each fixed $h$ , a mean-one proxy has $\log L_{n, h} = h^{T} Δ_{n} - \frac{1}{2} h^{T} K h + o_{P_{n, 0}} (1)$ and is total-variation close to the actual local law.

[F2]

Regular estimator under local alternatives: for an identity target the centered statistic has a common limit under each fixed local displacement; the statement gives the corresponding target-shift condition explicitly.

[F3]

Le Cam's third lemma for a Gaussian likelihood-ratio limit: the joint limit tilted by the mean-one Gaussian likelihood ratio describes the statistic's limit under the proxy local law.

[F4]

Weakly convergent sequences are tight and Prokhorov tightness theorem on polish spaces: convergent marginal laws are tight, and under AC a tight sequence of joint Borel laws on Euclidean space has a weakly convergent subsequence.

[F5]

Identity theorem for holomorphic functions: two holomorphic functions on a connected complex domain that agree on a set with an interior accumulation point agree throughout the domain.

[F6]

Multivariate normal law, including singular covariance and Characteristic function of a multivariate normal law: $N_{d} (0, K)$ has characteristic function $u \mapsto e^{- u^{T} K u / 2}$ and finite exponential moments in every real direction.

[F7]

Continuous mapping theorem and Slutsky's theorem for real random variables: continuous projections preserve weak limits, and scalar $o_{P} (1)$ remainders preserve those limits.

[F8]

Uniqueness of a law from its characteristic function: real probability laws with equal characteristic functions are equal; the vector conclusion below is obtained from scalar projections using Cramer–Wold.

[F9]

Cramer wold device: under AC, equality or convergence of all real projections determines the Borel vector law.

[F10]

The product measure of two sigma-finite measure spaces, For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, and Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: sigma-finite products have the rectangle formula, and Tonelli evaluates nonnegative product integrals by iterated integration.

[F11]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: closed bounded subsets of finite-dimensional Euclidean space are compact.

[F12]

Finite and countable subadditivity of measures: the measure of a finite union is at most the sum of the measures of its members.

[F13]

Characteristic function of a real random variable: the characteristic function of a real random variable $X$ is $t \mapsto E [e^{i t X}]$ .

[F14]

Fubini's theorem for L^1 functions on a sigma-finite product: a bounded complex-valued function is integrable under a product probability, and Fubini factors the integral of a product of coordinate functions.

[A1]

The Axiom of Choice: AC is assumed by LAN, Prokhorov's theorem, and the finite-dimensional characteristic-function uniqueness and Cramer–Wold suppliers.

Proof

Given: The local experiment, target, estimator, and hypotheses above.

1.1A1F1F2F4F11F12givenchoose

Under $P_{n, 0}$ , $T_{n} \Rightarrow W$ by regularity at $h = 0$ and $Δ_{n} \Rightarrow N_{d} (0, K)$ by LAN. Marginal tightness gives compact sets with outside probabilities below $ε / 2$ ; enlarge them to closed balls. Their product is closed and bounded in $R^{k + d}$ and hence compact by [F11]. By [F12] the joint outside probability is at most $ε$ , so the joint laws of $(T_{n}, Δ_{n})$ are tight.

2.1A1F1F4F7F9step 1.1given

By [F4], choose a subsequence along which $(T_{n}, Δ_{n}) \Rightarrow (T, Δ)$ . Its marginals have laws $W$ and $N_{d} (0, K)$ . Fix $h \in R^{d}$ . By [F1], $P_{n, 0} (L_{n, h} = 0) \to 0$ ; define $ℓ_{n, h} = \log L_{n, h}$ when $L_{n, h} > 0$ and $ℓ_{n, h} = 0$ otherwise. This replacement changes a variable only on an event of probability $o (1)$ . For any $a \in R^{k}$ and $b \in R$ , the projection of $(T_{n}, ℓ_{n, h})$ differs by $o_{P} (1)$ from $a^{T} T_{n} + b h^{T} Δ_{n} - \frac{1}{2} b h^{T} K h$ . The latter converges by [F7]; applying scalar Slutsky and [F9] to every projection gives $(T_{n}, ℓ_{n, h}) \Rightarrow (T, h^{T} Δ - \frac{1}{2} h^{T} K h)$ .

3.1F1F2F3F7F9step 2.1given

By the continuous mapping theorem [F7], $(T_{n}, e^{ℓ_{n, h}}) \Rightarrow (T, e^{h^{T} Δ - \frac{1}{2} h^{T} K h})$ . Since $e^{ℓ_{n, h}} = L_{n, h}$ off the event $L_{n, h} = 0$ , whose probability tends to zero by [F1], the same joint limit holds with $L_{n, h}$ . Apply [F3] to this mean-one proxy; [F1] transfers its limit under the proxy law to the actual $P_{n, h}$ law. Regularity and $δ_{n} (h) \to D h$ imply that under this same actual law $T_{n} \Rightarrow W + D h$ : apply [F7] to each real projection and then [F9]. Therefore for every real $h$ and $t \in R^{k}$ , $E [e^{i t^{T} T + h^{T} Δ - \frac{1}{2} h^{T} K h}] = e^{i t^{T} D h} φ_{W} (t),$ where $φ_{W} (t) = E [e^{i t^{T} W}]$ .

4.1F5F6step 3.1given

Rearranging step 3.1 gives $F_{t} (h) : = E [e^{i t^{T} T + h^{T} Δ}] = e^{\frac{1}{2} h^{T} K h + i t^{T} D h} φ_{W} (t)$ for every real $h$ . For complex $z \in C^{d}$ , define $F_{t} (z) = E [e^{i t^{T} T + z^{T} Δ}]$ . On every compact set of $z$ , its coordinate power series and derivatives are dominated by $e^{R ∥ Δ ∥_{1}}$ for some finite $R$ , whose expectation is finite because $Δ$ is Gaussian. Thus $F_{t}$ is entire in each coordinate, as is the right-hand side. Apply [F5] one coordinate at a time, holding the remaining coordinates real and then extending them successively; the equality holds for every complex $z$ .

5.1F6F13step 4.1givenalgebra

Put $z = i u$ in step 4.1. By [F13], the resulting characteristic functions satisfy, for all real $t, u$ , $E [e^{i t^{T} T + i u^{T} Δ}] = φ_{W} (t) e^{- t^{T} D u - u^{T} K u / 2}$ . Set $R = T - D K^{- 1} Δ$ and replace $u$ by $u - K^{- 1} D^{T} t$ . Direct expansion gives $E [e^{i t^{T} R + i u^{T} Δ}] = (φ_{W} (t) e^{t^{T} D K^{- 1} D^{T} t / 2}) e^{- u^{T} K u / 2}$ . At $u = 0$ the first factor is the characteristic function of $R$ ; the second is the characteristic function of $Δ$ . The joint characteristic function therefore factors as the product of the marginal characteristic functions.

6.1A1F6F8F9F10F13F14step 5.1algebra∎

Let $ρ = L (R) \otimes N_{d} (0, K)$ , whose product law exists by [F10]. For each $t \in R^{k}$ and $u \in R^{d}$ , the function $(r, z) \mapsto e^{i t^{T} r} e^{i u^{T} z}$ is bounded and hence integrable under $ρ$ ; [F14] factors its integral into the marginal characteristic functions. By [F13] and step 5.1, this product equals the characteristic function of $(R, Δ)$ . Scalar uniqueness [F8] and [F9] give $L (R, Δ) = ρ$ , so $R$ and $Δ$ are independent. Since $D K^{- 1} Δ \sim N_{k} (0, D K^{- 1} D^{T})$ and $T = D K^{- 1} Δ + R$ , the law of $T$ , which is $W$ , is the stated convolution. The argument allows singular $D K^{- 1} D^{T}$ and uses no inverse of that matrix.

Depends on

Used by

Convolution bound for general regular estimators Theorem

Dependency tree · two levels

119 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. W. van der Vaart, Semiparametric Statistics, Lecture Notes in Mathematics 1781, Lecture 4, §4.2, Theorem 4.12 (Springer, 2002) (standard reference, not scraped)
John Duchi, A few notes on contiguity, asymptotics, and local asymptotic normality, §2 (2021) (standard reference, not scraped)