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.

The odd-dimensional wave formula by iterated spherical means

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n = 2 k + 1 \geq 3$ be odd, $c > 0$ , $u_{0} \in C^{k + 2} (R^{n})$ , $u_{1} \in C^{k + 1} (R^{n})$ , put $D_{t} : = t^{- 1} \partial_{t}$ , and let $M$ be the spherical mean of Spherical means and the weighted ball integral of space-dependent data. Then $u (x, t) : = \frac{1}{(n - 2)!!} [\frac{\partial}{\partial t} D_{t}^{k - 1} (t^{n - 2} M_{u_{0}} (x, c t)) + D_{t}^{k - 1} (t^{n - 2} M_{u_{1}} (x, c t))]$ defines a $C^{2}$ function on $R^{n} \times (0, \infty)$ solving $u_{t t} = c^{2} Δ u$ ; each $D_{t}^{j}$ is applied to the $t$ -dependent function $t \mapsto t^{n - 2} M_{f} (x, c t)$ . For $n = 3$ ( $k = 1$ ) this is exactly Kirchhoff's formula Kirchhoff's formula in three dimensions, and the displayed constant $(n - 2)!!$ is the one required by the leading coefficient of Radial-derivative expansion of the Euler–Poisson–Darboux transform and its zero-radius limit.

Facts & Assumptions

Given: Countable Choice, $n = 2 k + 1 \geq 3$ , $c > 0$ , $u_{0} \in C^{k + 2} (R^{n})$ , $u_{1} \in C^{k + 1} (R^{n})$ , and the spherical means $H_{f} (x, r) : = M_{f} (x, r)$ .

[F1]

For $j \geq 1$ and every $φ \in C^{j + 1} ((0, \infty))$ , $\partial_{r}^{2} D_{r}^{j - 1} (r^{2 j - 1} φ (r)) = D_{r}^{j - 1} [r^{2 j - 1} r^{- 2 j} \partial_{r} (r^{2 j} \partial_{r} φ (r))]$ on $(0, \infty)$ , where $D_{r} = r^{- 1} \partial_{r}$ (The iterated radial-derivative identity behind the odd-dimensional reduction).

[F2]

For $m \geq 1$ and $h \in C^{m} (R^{n})$ , $(x, r) \mapsto M_{h} (x, r)$ is $C^{m}$ on $R^{n} \times (0, \infty)$ with all derivatives obtained by differentiating $h$ under the sphere integral (Smoothness, parity and zero-radius limits of spherical means).

[F3]

For $h \in C^{2} (R^{n})$ the Euler–Poisson–Darboux identity $Δ_{x} M_{h} (x, r) = M_{r r} (x, r) + \frac{n - 1}{r} M_{r} (x, r)$ holds for every $r > 0$ (The Euler–Poisson–Darboux equation for spherical means).

[F4]

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)$ ); sums, products and quotients of differentiable functions are differentiable with the usual rules on their domains (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$ ). 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).

[F5]

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

Proof

1.1F1F2

Fix $f \in C^{k + 1} (R^{n})$ and put $W (x, t) : = D_{t}^{k - 1} (t^{n - 2} H_{f} (x, c t))$ , where $n - 2 = 2 k - 1$ . Applying [F1] with $j = k$ and $φ (t) : = H_{f} (x, c t)$ — admissible for each fixed $x$ because $H_{f} (x, \cdot) \in C^{k + 1}$ by [F2] — gives $\partial_{t}^{2} D_{t}^{k - 1} (t^{2 k - 1} H_{f} (x, c t)) = D_{t}^{k - 1} [t^{2 k - 1} t^{- 2 k} \partial_{t} (t^{2 k} \partial_{t} H_{f} (x, c t))]$ .

1.2F3F4algebra

The inner expression. By [F4], $\partial_{t} H_{f} (x, c t) = c (H_{f})_{r} (x, c t)$ and $\partial_{t}^{2} H_{f} (x, c t) = c^{2} (H_{f})_{r r} (x, c t)$ , so with $r = c t$ and $2 k = n - 1$ , $t^{- 1} \partial_{t} (t^{2 k} \partial_{t} H_{f} (x, c t)) = t^{- 1} \partial_{t} (t^{n - 1} c (H_{f})_{r} (x, c t)) = c t^{n - 3} [(n - 1) (H_{f})_{r} (x, c t) + c t (H_{f})_{r r} (x, c t)] = c t^{n - 3} [(n - 1) (H_{f})_{r} (x, r) + r (H_{f})_{r r} (x, r)] = c^{2} t^{n - 2} Δ_{x} H_{f} (x, c t)$ , the last equality because $r ((H_{f})_{r r} + \frac{n - 1}{r} (H_{f})_{r}) = r Δ_{x} H_{f}$ by [F3].

1.3F5algebra

Hence $\partial_{t}^{2} W (x, t) = c^{2} D_{t}^{k - 1} (t^{n - 2} Δ_{x} H_{f} (x, c t))$ . The operator $Δ_{x}$ acts only on the $x$ -variables while $D_{t}^{k - 1}$ and multiplication by $t^{n - 2}$ act only on $t$ , and the mixed partials involved commute by [F5] since $H_{f}$ is $C^{k + 1}$ ; therefore $D_{t}^{k - 1} (t^{n - 2} Δ_{x} H_{f} (x, c t)) = Δ_{x} D_{t}^{k - 1} (t^{n - 2} H_{f} (x, c t)) = Δ_{x} W (x, t)$ , that is $\partial_{t}^{2} W = c^{2} Δ_{x} W$ on $R^{n} \times (0, \infty)$ .

1.4F2algebra

Regularity and superposition. For $f = u_{0} \in C^{k + 2} (R^{n})$ the function $t \mapsto t^{n - 2} H_{u_{0}} (x, c t)$ is $C^{k + 2}$ by [F2], so $W_{u_{0}} = D_{t}^{k - 1} (\cdot)$ is $C^{3}$ ; for $f = u_{1} \in C^{k + 1} (R^{n})$ similarly $W_{u_{1}}$ is $C^{2}$ . Hence $u = (n - 2)!!^{- 1} [\partial_{t} W_{u_{0}} + W_{u_{1}}]$ is $C^{2}$ on $R^{n} \times (0, \infty)$ and $u_{t t} = (n - 2)!!^{- 1} [\partial_{t} \partial_{t}^{2} W_{u_{0}} + \partial_{t}^{2} W_{u_{1}}] = (n - 2)!!^{- 1} [\partial_{t} (c^{2} Δ_{x} W_{u_{0}}) + c^{2} Δ_{x} W_{u_{1}}] = c^{2} Δ_{x} u$ .

2.1given∎

For $k = 1$ , that is $n = 3$ , the formula reads $\partial_{t} [t M_{u_{0}} (x, c t)] + t M_{u_{1}} (x, c t)$ with $(n - 2)!! = 1$ , which is Kirchhoff's expression of Kirchhoff's formula in three dimensions. The prefactor $(n - 2)!!$ is the leading coefficient of $D_{r}^{k - 1} (r^{2 k - 1} φ)$ by Radial-derivative expansion of the Euler–Poisson–Darboux transform and its zero-radius limit: with $r = c t$ and with the evenness of the means, which kills the first-order term, that expansion makes the normalised combination the data-carrying normalisation; the precise attainment of $u_{0}$ and $u_{1}$ is proved by the data-attainment lemma below.

Depends on

Used by

Dependency tree · two levels

63 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)