Alphabeta Math
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 population bias of local-linear regression

Statement

Assume AC for the chosen regression version Regression target and chosen version. Let X have density f, with f(x)>0 at a fixed interior point x, and let f,m be C2 near x. Let K be a finite-valued Borel, nonnegative symmetric kernel with ∫K=1, 0<μ2=∫u2K(u) du<∞ and ∫K2<∞. Assume either compact kernel support, or that f,m and their first two derivatives are bounded and continuous on R. A further localization alternative, including the Gaussian kernel, is that E[Y2]<∞, K is bounded, and lim⁡A→∞sup⁡∣u∣≥A∣u∣3K(u)=0. Under this rapid-tail alternative only the stated local smoothness of f,m is needed; no global boundedness of m or of its derivatives is assumed. Set Sj(h)=∫K(u)ujf(x−hu) du,Tj(h)=∫K(u)ujf(x−hu)m(x−hu) du. For sufficiently small h, Dh=S0S2−S12>0 and the population local-linear intercept, in the coordinates of Local-polynomial estimator, is mLL,h(x)=S2T0−S1T1Dh. Then mLL,h(x)−m(x)=h2μ22m′′(x)+o(h2). This requires no fourth kernel moment.

Facts & Assumptions

Given: The density, selected version, kernel moments and localization or global domination hypotheses in the statement.

[F1]

The local-polynomial fit returns the intercept of the weighted normal equations on a nonsingular design. Local-polynomial estimator.

[F2]

The selected regression function is a Borel conditional-mean version. Regression target and chosen version.

[F3]

A density supplies its integration law f dλ. The measure with density f relative to μ.

[F4]

For PX-almost every t, m(t)=∫y Q(t,dy), and conditional integration gives ∫∣m(t)∣f(t) dt≤E∣Y∣<∞ by the triangle inequality. Conditional expectation as a measurable function of the conditioning variable

Proof

1.1givenF2F3F4algebra

Write rh(u)=m(x−hu)−m(x)+hum′(x). Taylor's integral formula bounds ∣rh(u)∣≤Ch2u2 and gives rh(u)/h2→12m′′(x)u2 pointwise. It also gives ∣rh(u)∣≤Ch∣u∣ and rh(u)/(h∣u∣)→0 for each nonzero u. These bounds hold on compact kernel support for small h, or globally under the alternative assumptions. With Rj=∫K(u)ujf(x−hu)rh(u) du, splitting at a fixed ∣u∣≤A and controlling the tails by ∫∣u∣>Au2K(u) du proves R0=12h2m′′(x)f(x)μ2+o(h2) and R1=o(h). The same split yields S0→f(x), S2→f(x)μ2; symmetry and the first-order expansion of f give S1=−hf′(x)μ2+o(h)=O(h). In the rapid-tail alternative [F4] gives ∫∣m∣f<∞. Write z=x−hu and split at ∣z−x∣=δ. The far parts of S0,S1,S2 are respectively o(h2),o(h),o(1), since K((x−z)/h)≤ϵhh3/∣x−z∣3 and ∫f=1. The far parts of R0,R1 are o(h2),o(h): expand r=m(z)−m(x)−m′(x)(z−x) and use ∫∣m∣f<∞ with ∣z−x∣≥δ. On the near region the preceding local bounds and the integrable u2K apply; letting δ→0 after h→0 gives the same remainder limits. These estimates also make every stated integral finite.

2.1givenF1step 1.1algebra∎

The determinant tends to f(x)2μ2>0. Since Tj=m(x)Sj−hm′(x)Sj+1+Rj for j=0,1, the affine terms in the intercept cancel exactly and mLL,h(x)−m(x)=(S2R0−S1R1)/Dh. Step 1.1 makes S1R1=o(h2) and gives the asserted coefficient after division by the positive limiting determinant.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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