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-bandwidth Gaussian smoothing
Example
Let and For every fixed bandwidth , Thus the expected estimate is the centered Gaussian density with covariance , and at it is strictly smaller than .
Facts & Assumptions
Given: , , iid observations with density , and kernel .
The Axiom of Countable Choice, written (The Axiom of Countable Choice ()).
The KDE formula and density-based sample model (Density targets and the kernel density estimator).
Expectations are integrals against the sample law, which has density (Change of variables for expectation, Integrating against a density agrees with integrating the product).
The Lebesgue integral is linear on integrable functions (The Lebesgue integral is linear on ).
The nonnegative plane Gaussian integral is (The plane Gaussian integral equals by polar coordinates).
Tonelli permits factoring nonnegative product integrals (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).
Under , affine C substitutions obey the nonnegative change-of-variables formula (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).
Verification
Put . Tonelli [F5] and [F4] give , so . Scaling by with [F6] yields ; repeated Tonelli gives . Since , [F6] with gives .
By [F1] and [F2], expectation of one KDE summand is integration of its Gaussian kernel against . The summand is bounded for fixed , hence integrable. The integrand is nonnegative; using [F6] with changes variables to . All summands have this expectation, so linearity [F3] gives The integral is finite because both Gaussian densities are bounded and integrable.
In the integrand of step 2.1, combine exponents using The remaining translated Gaussian integral is by [F4], [F5], and affine scaling [F6]. Multiplying the normalizing constants gives the displayed formula.
At , because . Therefore a finite positive bandwidth has nonzero bias in this example.
Depends on
- Density targets and the kernel density estimator
- Each fixed-point KDE evaluation is a statistic
- Change of variables for expectation
- Integrating against a density agrees with integrating the product
- The Lebesgue integral is linear on $L^1(\mu)$
- The plane Gaussian integral equals $\pi$ by polar coordinates
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
70 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. 1–3 (standard reference, not scraped)
- Adrian Bowman and Ludger Evers, Nonparametric Smoothing, APTS 2013–14 course notes, §1.2.4, PDF p. 11 (standard reference, not scraped)