TheoremStatement: Literature-sourcedProof: 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.

Pointwise variance of the KDE

Statement

Assume ${A C}_{ω}$ . Let $X_{1}, \dots, X_{n}$ be iid with bounded continuous Borel density version $f$ on $R^{d}$ . Let $K : R^{d} \to R$ be Borel, $K \in L^{1} \cap L^{2}$ , and $\int K (u) d u = 1$ . For fixed $x \in R^{d}$ , along bandwidths $h = h_{n} > 0$ with $h_{n} \to 0$ and $n h_{n}^{d} \to \infty$ , $Var ({\hat{f}}_{h_{n}} (x)) = \frac{f (x) ∥ K ∥_{2}^{2}}{n h_{n}^{d}} + o ((n h_{n}^{d})^{- 1}) .$

Facts & Assumptions

Given: ${A C}_{ω}$ , iid $X_{1}, \dots, X_{n}$ with bounded continuous density version $f$ , a Borel kernel $K \in L^{1} \cap L^{2}$ with unit integral, a fixed $x$ , and $h_{n} \to 0$ , $n h_{n}^{d} \to \infty$ .

[A1]

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

[F1]

The fixed-point estimate is ${\hat{f}}_{h} (x) = (n h^{d})^{- 1} \sum_{i} K ((x - X_{i}) / h)$ (Density targets and the kernel density estimator).

[F2]

Its fixed-point evaluations are measurable (Each fixed-point KDE evaluation is a statistic).

[F3]

The $X_{i}$ are independent and identically distributed random elements (Identical distribution and IID families).

[F4]

Measurable functions of independent random elements remain independent (Measurable coordinatewise functions preserve independence).

[F5]

Expectations of integrable products of independent real random variables factor (Expectations factor over finite products of independent random variables).

[F6]

For a square-integrable real random variable, $Var (Z) = E [(Z - E Z)^{2}]$ (Moments, variance, and covariance on a probability space).

[F7]

Expectation is integration against the law, and a density law satisfies $\int g d (f λ_{d}) = \int g f d λ_{d}$ for nonnegative measurable $g$ (Change of variables for expectation, Integrating against a density agrees with integrating the product).

[F8]

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

[F9]

Under ${A C}_{ω}$ , a C $^{1}$ diffeomorphism obeys the change-of-variables formula for integrable functions (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F10]

Dominated convergence applies under the integrable majorant $∥ f ∥_{\infty} K^{2}$ (Dominated convergence).

[F11]

Expectation is linear for finite sums of integrable variables (The Lebesgue integral is linear on $L^{1} (μ)$ ).

Proof

1.1givenA1F1F2F3F4F7F8

Put $Z_{i} = K ((x - X_{i}) / h)$ . By [F2] and [F7], and using the nonnegative substitution $u \mapsto x - h u$ from [F8], $E [Z_{i}^{2}] = h^{d} \int K (u)^{2} f (x - h u) d u \leq h^{d} ∥ f ∥_{\infty} ∥ K ∥_{2}^{2} < \infty .$ Likewise $E ∣ Z_{i} ∣ \leq h^{d} ∥ f ∥_{\infty} ∥ K ∥_{1} < \infty$ , so each $Z_{i}$ is integrable and square-integrable. The maps $z \mapsto K ((x - z) / h)$ preserve independence by [F4]; identical laws of $X_{i}$ give identical laws of $Z_{i}$ .

2.1step 1.1F3F5F6F11algebra

Let $W_{i} = Z_{i} - E Z_{i}$ . For $i \neq j$ , [F5] applied to the independent integrable variables $W_{i}, W_{j}$ gives $E [W_{i} W_{j}] = E [W_{i}] E [W_{j}] = 0$ . Expanding the finite square and using expectation linearity [F11] therefore gives $Var ({\hat{f}}_{h} (x)) = \frac{1}{n h^{2 d}} (E [Z_{1}^{2}] - (E Z_{1})^{2}) .$

3.1step 1.1step 2.1F7F9F10F11algebra∎

Step 1.1 shows that $t \mapsto K ((x - t) / h) f (t)$ is integrable. Put $g (t) = K ((x - t) / h)$ and decompose $g = g^{+} - g^{-}$ into its nonnegative parts. The density integrals of both parts are finite because $\int ∣ g ∣ f < \infty$ by step 1.1. Apply the nonnegative density identity [F7] to each part and subtract using [F11], obtaining $E Z_{1} = \int g f$ . Applying the signed substitution [F9] to this integrable product gives $E Z_{1} = h^{d} \int K (u) f (x - h u) d u$ , so $∣ E Z_{1} ∣ \leq h^{d} ∥ f ∥_{\infty} ∥ K ∥_{1}$ . Along any sequence $h_{n} \to 0$ , [F10] gives $\int K (u)^{2} f (x - h_{n} u) d u ⟶ f (x) ∥ K ∥_{2}^{2} .$ Thus the first term in step 2.1 is $f (x) ∥ K ∥_{2}^{2} / (n h_{n}^{d}) + o ((n h_{n}^{d})^{- 1})$ . The subtracted mean-square term is $O (n^{- 1}) = o ((n h_{n}^{d})^{- 1})$ because $h_{n}^{d} \to 0$ . The additional $n h_{n}^{d} \to \infty$ condition places the expansion in the vanishing-variance regime. This proves the formula.

Depends on

Used by

Gaussian-kernel moments and pointwise constants Example

Dependency tree · two levels

63 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, Proposition 2, PDF p. 4 (standard reference, not scraped)
Adrian Bowman and Ludger Evers, Nonparametric Smoothing, APTS 2013–14 course notes, §1.2.1, PDF p. 8 (standard reference, not scraped)