Alphabeta Math
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.

Finite-bandwidth Gaussian smoothing

Example

Let τ>0 and fτ(x)=(2πτ2)−d/2exp⁡ ⁣(−∥x∥22τ2),Kd(u)=(2π)−d/2e−∥u∥2/2. For every fixed bandwidth h>0, Ef^h(x)=(2π(τ2+h2))−d/2exp⁡ ⁣(−∥x∥22(τ2+h2)). Thus the expected estimate is the centered Gaussian density with covariance (τ2+h2)Id, and at x=0 it is strictly smaller than f(0).

Facts & Assumptions

Given: d,n≥1, τ,h>0, iid observations with density fτ, and kernel Kd.

[A1]

The Axiom of Countable Choice, written ACω (The Axiom of Countable Choice (ACω)).

[F1]

The KDE formula and density-based sample model (Density targets and the kernel density estimator).

[F2]

Expectations are integrals against the sample law, which has density f (Change of variables for expectation, Integrating against a density agrees with integrating the product).

[F3]

The Lebesgue integral is linear on integrable functions (The Lebesgue integral is linear on L1(μ)).

[F4]

The nonnegative plane Gaussian integral is ∫R2e−(x2+y2)d(x,y)=π (The plane Gaussian integral equals π by polar coordinates).

[F5]

Tonelli permits factoring nonnegative product integrals (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F6]

Under ACω, affine C1 substitutions obey the nonnegative change-of-variables formula (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

Verification

1.1givenA1F4F5F6algebra

Put I=∫Re−t2dt. Tonelli [F5] and [F4] give I2=π, so I=π. Scaling by s=t/2 with [F6] yields ∫(2π)−1/2e−t2/2dt=1; repeated Tonelli gives ∫Kd=1. Since fτ(x)=τ−dKd(x/τ), [F6] with x=τu gives ∫fτ=1.

2.1givenA1F1F2F3F6step 1.1

By [F1] and [F2], expectation of one KDE summand is integration of its Gaussian kernel against fτ. The summand is bounded for fixed h, hence integrable. The integrand is nonnegative; using [F6] with T(u)=x−hu changes variables to ∫Kd(u)fτ(x−hu)du. All summands have this expectation, so linearity [F3] gives Ef^h(x)=∫RdKd(u)fτ(x−hu)du. The integral is finite because both Gaussian densities are bounded and integrable.

3.1step 1.1A1F4F5F6algebrastep 2.1

In the integrand of step 2.1, combine exponents using ∥u∥2+τ−2∥x−hu∥2=τ2+h2τ2∥u−hxτ2+h2∥2+∥x∥2τ2+h2. The remaining translated Gaussian integral is (2πτ2/(τ2+h2))d/2 by [F4], [F5], and affine scaling [F6]. Multiplying the normalizing constants gives the displayed formula.

4.1step 3.1algebra∎

At x=0, Ef^h(0)=(2π(τ2+h2))−d/2<(2πτ2)−d/2=f(0), because h>0. Therefore a finite positive bandwidth has nonzero bias in this example.

Depends on

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