ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Gaussian-kernel moments and pointwise constants

Example

For $d \geq 1$ , take the standard Gaussian kernel $K_{d} (u) = (2 π)^{- d / 2} e^{- ∥ u ∥^{2} / 2} .$ Its second-moment matrix is $μ_{j k} = δ_{j k}$ and $∥ K_{d} ∥_{2}^{2} = (4 π)^{- d / 2}$ , where $δ_{j k}$ is $1$ for $j = k$ and $0$ otherwise. Thus, under the pointwise theorem hypotheses, $E {\hat{f}}_{h} (x) - f (x) = \frac{1}{2} h^{2} Δ f (x) + o (h^{2}), Var ({\hat{f}}_{h} (x)) = \frac{f (x)}{n h^{d}} (4 π)^{- d / 2} + o ((n h^{d})^{- 1}) .$ Here $Δ f = \sum_{j = 1}^{d} \partial_{j j} f$ .

Facts & Assumptions

Given: $d \geq 1$ , the kernel $K_{d}$ above, and a density/sample satisfying the hypotheses of Pointwise second-order bias of the KDE and Pointwise variance of the KDE.

[A1]

The Axiom of Countable Choice, written ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The nonnegative plane Gaussian integral is $\int_{R^{2}} e^{- (x^{2} + y^{2})} d (x, y) = π$ (The plane Gaussian integral equals $π$ by polar coordinates).

[F2]

Tonelli factors nonnegative integrals of products on Euclidean product spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F3]

Under ${A C}_{ω}$ , nonnegative C $^{1}$ substitutions obey change of variables (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F4]

Fubini factors absolutely integrable products on sigma-finite product spaces (Fubini's theorem for L^1 functions on a sigma-finite product).

[F5]

The chain rule and $(\exp)^{'} = \exp$ give derivatives of $ϕ$ (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[F6]

Integration by parts and the second fundamental theorem evaluate $\int u v^{'}$ on a compact interval when the derivatives are integrable (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F7]

The exponential dominates each fixed polynomial at infinity (The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

[F8]

The pointwise bias and variance expansions hold with their stated regularity and bandwidth conditions (Pointwise second-order bias of the KDE, Pointwise variance of the KDE).

[F9]

Integrals of nonnegative functions pass to increasing-domain limits (Monotone convergence for the integral).

Verification

1.1givenA1F1F2F3F5F6F7F9

Put $I = \int_{R} e^{- t^{2}} d t$ . Tonelli [F2] and [F1] give $I^{2} = \int_{R^{2}} e^{- (x^{2} + y^{2})} d (x, y) = π$ . Since $I \geq 0$ , $I = \sqrt{π}$ . Let $ϕ (t) = (2 π)^{- 1 / 2} e^{- t^{2} / 2}$ . The substitution $s = t / \sqrt{2}$ in [F3] then gives $\int ϕ = 1$ . By [F5], $ϕ^{'} (t) = - t ϕ (t)$ . Integration by parts [F6] gives $\int_{0}^{R} t ϕ (t) d t = ϕ (0) - ϕ (R)$ . By [F7], $ϕ (R) \to 0$ and $R ϕ (R) \to 0$ , so $\int ∣ t ∣ ϕ (t) d t = 2 ϕ (0) < \infty$ . Oddness then gives $\int t ϕ (t) d t = 0$ . Integration by parts [F6] on $[- R, R]$ also yields $\int_{- R}^{R} t^{2} ϕ (t) d t = \int_{- R}^{R} ϕ (t) d t - [t ϕ (t)]_{- R}^{R} .$ As $R \to \infty$ , $R ϕ (R) \to 0$ by [F7] (put $s = R^{2} / 4$ and use $R \leq 2 s$ for $R \geq 2$ ), and the right side tends to $1$ , so $\int t^{2} ϕ (t) d t = 1$ by [F9].

2.1step 1.1F1F2F4algebra

Since $K_{d} (u) = \prod_{j = 1}^{d} ϕ (u_{j})$ , repeated use of Tonelli [F2] shows $\int K_{d} = 1$ . Fubini [F4], the one-dimensional moments from step 1.1, and absolute integrability give $μ_{j j} = 1$ and $μ_{j k} = 0$ for $j \neq k$ . Also $\int K_{d} (u)^{2} d u = (2 π)^{- d} \prod_{j = 1}^{d} \int_{R} e^{- u_{j}^{2}} d u_{j} = (2 π)^{- d} π^{d / 2} = (4 π)^{- d / 2} .$

3.1step 2.1F8algebra∎

Substituting $μ_{j k} = δ_{j k}$ and $∥ K_{d} ∥_{2}^{2} = (4 π)^{- d / 2}$ into [F8] yields the two displayed leading terms. The Gaussian kernel is nonnegative and integrates to one by step 2.1, so A nonnegative normalized kernel estimate integrates to one also confirms that each finite estimate is a density.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

114 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

Whitney K. Newey, Nonparametric and Semiparametric Estimation, MIT OpenCourseWare 14.385, Fall 2007, PDF pp. 2–4 and 6 (standard reference, not scraped)
Ryan Tibshirani, Nonparametric Regression: Nearest Neighbors and Kernels, Advanced Topics in Statistical Learning, Spring 2024, §3, PDF p. 5 (standard reference, not scraped)