Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Smooth sphere data have a harmonic replacement

Statement

Let n2, aRn, R>0, and gC(BR(a)) be real. Write ωn1=Sn1. There is a unique hC(BR(a))C(BR(a)) harmonic inside and equal to g on the sphere. It is h(x)=BR(a)R2xa2Rωn1xyng(y)dS(y),xa<R. The kernel is positive and has integral one at each interior point.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

A C2 real function is harmonic when the sum of its pure second derivatives, its Laplacian, vanishes. (The Laplacian of a C2 function and of a C2 vector field).

[F2]

BR=ωn1Rn1 and ωn1 is finite and positive. (Sphere and ball measures scale in Rn).

[F3]

A classical harmonic function equals its sphere average on every compactly contained ball. (Spherical mean-value property for harmonic functions).

[F4]

Classical harmonic functions continuous on a bounded open set’s closure and sharing boundary data agree. (Uniqueness for the classical dirichlet problem).

[F5]

For measurable functions converging almost everywhere under a single integrable absolute majorant, dominated convergence permits passing their limit through the integral. (Dominated convergence).

Proof

technique · direct
1.1

Translate a to zero. Put q=xy, A=R2x2, and P(x,y)=Aqn/(Rωn1), where y=R. The sphere has finite positive measure ωn1Rn1. On compact interior sets q is bounded away from zero; all x-derivatives of the kernel times bounded g have a constant integrable majorant. The mean value theorem bounds their difference quotients likewise. Dominated convergence therefore permits differentiation of every order under the sphere integral and proves continuity of those derivatives.

F2F5given
2.1

Cartesian differentiation gives qn=n(xy)qn2, Δqn=2nqn2 and ΔA=2n. The product rule gives Δ(Aqn)=2nqn2(Aq2+2x(xy))=2nqn2(R2y2)=0. Thus both h and I(x)=P(x,y)dS(y) are smooth harmonic functions.

F1step 1.1algebra
3.1

Rotation invariance of surface measure and the kernel makes I constant on each sphere centered at zero. Its spherical mean equals I(0) by harmonic mean values; since it is already constant on that sphere, I(x)=I(0). At zero, P(0,y)=1/(ωn1Rn1), so I(0)=1. Also P>0 in the ball.

F2F3step 2.1algebra
4.1

Fix pBR. The mass identity gives h(x)g(p)=P(x,y)(g(y)g(p))dS(y). For a given ε>0, take δ>0 so that g(y)g(p)<ε when yp<δ. That part of the integral has absolute value at most ε. On the remaining sphere, if xp<δ/2, then xyδ/2, and P(x,y)(R2x2)/(Rωn1(δ/2)n) uniformly tends to zero. The remaining integral is bounded by this supremum times 2gBR. Thus h(x)g(p), proving continuity on the closed ball.

step 3.1algebra
5.1

Any two such harmonic replacements have identical boundary data on a bounded ball and are continuous on its closure, so classical Dirichlet uniqueness makes them equal. Translation restores the stated formula at a.

F4step 4.1

Depends on

Used by

Dependency tree · two levels

21 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