TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Kirchhoff's formula in three dimensions

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ , $u_{0} \in C^{3} (R^{3})$ , $u_{1} \in C^{2} (R^{3})$ and let $M$ be the spherical mean of Spherical means and the weighted ball integral of space-dependent data. Then $u (x, t) : = \frac{\partial}{\partial t} [t M_{u_{0}} (x, c t)] + t M_{u_{1}} (x, c t)$ defines a $C^{2}$ function on $R^{3} \times (0, \infty)$ solving $u_{t t} = c^{2} Δ u$ . Equivalently, for $t > 0$ , $u (x, t) = \frac{1}{4 π c^{2} t^{2}} \int_{\partial B_{c t} (x)} (u_{0} (y) + \nabla u_{0} (y) \cdot (y - x) + t u_{1} (y)) d S (y),$ the sphere integral being the unnormalised form of the mean because $ω_{2} = 4 π$ (Sphere and ball measures scale in Rn). The formula uses the values of $u_{0}, u_{1}$ and the normal derivative of $u_{0}$ on $\partial B_{c t} (x)$ ; pointwise agreement of the two data only on that sphere need not give the same solution value.

Facts & Assumptions

Given: Countable Choice, $c > 0$ , $u_{0} \in C^{3} (R^{3})$ , $u_{1} \in C^{2} (R^{3})$ , and the means $A (x, r) : = M_{u_{0}} (x, r)$ , $B (x, r) : = M_{u_{1}} (x, r)$ .

[F1]

For $k \geq 1$ and $h \in C^{k} (R^{3})$ , the spherical mean $M_{h}$ is $C^{k}$ on $R^{3} \times (0, \infty)$ , every derivative being obtained by differentiating $h$ under the sphere integral (Smoothness, parity and zero-radius limits of spherical means).

[F2]

For $h \in C^{2} (R^{3})$ one has $Δ_{x} M_{h} (x, r) = M_{r r} (x, r) + \frac{2}{r} M_{r} (x, r)$ for $r > 0$ (The Euler–Poisson–Darboux equation for spherical means).

[F3]

If $f$ is totally differentiable at $a$ and $g$ at $f (a)$ , then $g \circ f$ is totally differentiable at $a$ with $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ). The required total differentiability follows from continuous coordinate partial derivatives (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[F4]

Sums, products, constant multiples of differentiable functions are differentiable with the usual rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F5]

If $h$ is $C^{2}$ on an open set of $R^{m}$ , then $\partial_{i} \partial_{j} h = \partial_{j} \partial_{i} h$ (Clairaut--Schwarz theorem for continuous second partial derivatives).

[F6]

$∣ \partial B_{r}^{3} ∣ = ω_{2} r^{2}$ with $ω_{2} = 3 V_{3}$ , and the map $ω \mapsto a + R ω$ multiplies surface measure by $R^{2}$ : $\int_{S^{2}} h (ω) d σ (ω) = R^{- 2} \int_{\partial B_{R} (a)} h ((y - a) / R) d S (y)$ (Sphere and ball measures scale in Rn, Agreement with the existing polar sphere measure).

[F7]

$V_{3} = π^{3 / 2} / Γ (5 / 2) = 4 π / 3$ , so $ω_{2} = 3 V_{3} = 4 π$ (The closed form for the volume of the unit $n$ -ball, The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ , $Γ (1 / 2) = \sqrt{π}$ from the Gaussian integral).

Proof

1.1F1F3F4algebra

Time derivatives of the candidate. Write $r = c t$ . By [F1] the means $A, B$ are $C^{3}$ respectively $C^{2}$ on $R^{3} \times (0, \infty)$ , so [F3] and [F4] give $u = A + c t A_{r} + t B$ , $\partial_{t} u = 2 c A_{r} + c^{2} t A_{r r} + B + c t B_{r}$ and $\partial_{t}^{2} u = 3 c^{2} A_{r r} + c^{3} t A_{r r r} + 2 c B_{r} + c^{2} t B_{r r}$ on $R^{3} \times (0, \infty)$ , all derivatives being evaluated at $(x, c t)$ .

1.2F2F5F4algebra

Spatial derivatives. By [F2] applied to $u_{0}$ and to $u_{1}$ , $Δ_{x} A = A_{r r} + \frac{2}{r} A_{r}$ and $Δ_{x} B = B_{r r} + \frac{2}{r} B_{r}$ ; since $A$ is $C^{3}$ and $\partial_{r}$ commutes with the $x$ -derivatives by [F5], $Δ_{x} A_{r} = \partial_{r} (Δ_{x} A) = A_{r r r} + \frac{2}{r} A_{r r} - \frac{2}{r^{2}} A_{r}$ . Hence $Δ u = Δ_{x} A + c t Δ_{x} A_{r} + t Δ_{x} B = (A_{r r} + \frac{2}{r} A_{r}) + c t (A_{r r r} + \frac{2}{r} A_{r r} - \frac{2}{r^{2}} A_{r}) + t (B_{r r} + \frac{2}{r} B_{r})$ at $(x, c t)$ .

1.3F1F3F6F7algebra

The unnormalised form. Since $∣ S^{2} ∣ = ω_{2} = 4 π$ by [F6] and [F7], $M_{u_{0}} (x, r) = \frac{1}{4 π} \int_{S^{2}} u_{0} (x + r ω) d σ (ω) = \frac{1}{4 π r^{2}} \int_{\partial B_{r} (x)} u_{0} d S$ , and likewise for $u_{1}$ ; also $\partial_{r} M_{u_{0}} (x, r) = \frac{1}{4 π} \int_{S^{2}} \nabla u_{0} (x + r ω) \cdot ω d σ (ω) = \frac{1}{4 π r^{2}} \int_{\partial B_{r} (x)} \nabla u_{0} (y) \cdot \frac{y - x}{r} d S (y)$ by [F1], [F3] and the scaling in [F6]. Substituting $r = c t$ into $u = A + c t A_{r} + t B$ and collecting the common factor $\frac{1}{4 π c^{2} t^{2}}$ gives $u (x, t) = \frac{1}{4 π c^{2} t^{2}} \int_{\partial B_{c t} (x)} (u_{0} (y) + \nabla u_{0} (y) \cdot (y - x) + t u_{1} (y)) d S (y)$ .

2.1F4step 1.1step 1.2algebra

Comparison. Multiplying step 1.2 by $c^{2}$ and substituting $r = c t$ gives $c^{2} Δ u = c^{2} A_{r r} + (2 c / t) A_{r} + c^{3} t A_{r r r} + 2 c^{2} A_{r r} - (2 c / t) A_{r} + c^{2} t B_{r r} + 2 c B_{r} = 3 c^{2} A_{r r} + c^{3} t A_{r r r} + c^{2} t B_{r r} + 2 c B_{r}$ . This equals $u_{t t}$ from step 1.1, proving the equation. The $C^{3}$ and $C^{2}$ regularity of $A$ and $B$ gives $u \in C^{2}$ .

3.1step 2.1step 1.3∎

Both displays define the same $C^{2}$ solution. The unnormalised display uses the data values and the normal derivative of $u_{0}$ on the sphere, or equivalently the data on an open neighbourhood of that sphere.

Depends on

Used by

Dependency tree · two levels

75 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #12: Kirchhoff's Formula and Minkowskian Geometry (Fall 2011) (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A (UC Berkeley, 19 March 2024) (standard reference, not scraped)