LemmaStatement: 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 Euler–Poisson–Darboux equation for spherical means

Statement

Assume the Axiom of Countable Choice, let $n \geq 1$ , let $f \in C^{2} (R^{n})$ and let $M = M_{f}$ be the spherical mean of Spherical means and the weighted ball integral of space-dependent data. Then for every $x \in R^{n}$ and $r > 0$ $Δ_{x} M (x, r) = M_{r r} (x, r) + \frac{n - 1}{r} M_{r} (x, r) .$ The right-hand side extends continuously to $r = 0$ with value $Δ f (x)$ : with $M (x, 0) : = f (x)$ one has $M_{r} (x, r) \to 0$ and $(M_{r r} + \frac{n - 1}{r} M_{r}) (x, r) \to Δ f (x)$ as $r ↓ 0$ . If $u \in C^{2} (R^{n} \times I)$ is a classical solution of $□_{c} u = 0$ on an interval $I$ , then its space-time mean $(x, r, t) \mapsto M_{u} (x, r, t) : = ω_{n - 1}^{- 1} \int_{S^{n - 1}} u (x + r ω, t) d σ (ω)$ satisfies $\partial_{t}^{2} M_{u} = c^{2} (M_{r r} + \frac{n - 1}{r} M_{r})$ . No equation for $f$ is needed for the identity itself.

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $f \in C^{2} (R^{n})$ , the spherical mean $M = M_{f}$ with $M (x, 0) = f (x)$ , and, when stated, a $C^{2}$ solution $u$ of $□_{c} u = 0$ on $R^{n} \times I$ .

[F1]

For $k \geq 1$ and $h \in C^{k} (R^{n})$ , $(x, r) \mapsto M_{h} (x, r)$ is $C^{k}$ on $R^{n} \times (0, \infty)$ with all derivatives obtained by differentiating $h$ under the sphere integral; it extends continuously to $r = 0$ with $M_{h} (x, 0) = h (x)$ , and its radial derivative tends to $0$ uniformly on compacta (Smoothness, parity and zero-radius limits of spherical means).

[F2]

If $g \in C^{2} (R^{n})$ and $r > 0$ , then $\partial_{r} M_{g} (x, r) = \frac{r}{n} A_{Δ g} (x, r)$ , where $A_{Δ g} (x, r) = ∣ B_{r} (x) ∣^{- 1} \int_{B_{r} (x)} Δ g$ is the ball average (Radial derivative of a spherical average, The average of a locally integrable function over a Euclidean ball).

[F3]

For $h \in C^{0} (R^{n})$ one has $M_{h} (x, r) = A_{h} (x, r) + \frac{r}{n} \partial_{r} A_{h} (x, r)$ for all $r > 0$ (Ball means and sphere means are related by a radial derivative).

[F4]

A continuous real function on a nonempty compact metric space is bounded; Euclidean closed balls are compact (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).

Proof

1.1F1algebra

The spatial Laplacian passes under the sphere integral: by [F1] the map $(x, r) \mapsto M (x, r)$ is $C^{2}$ , and differentiating the defining integral twice in $x$ , $Δ_{x} M (x, r) = ω_{n - 1}^{- 1} \int_{S^{n - 1}} Δ f (x + r ω) d σ (ω) = M_{Δ f} (x, r)$ for every $r > 0$ .

1.2F2F3algebra

Radial identities. Put $A (x, r) : = A_{Δ f} (x, r)$ . Applying [F2] only to $f$ gives $M_{r} (x, r) = \frac{r}{n} A (x, r)$ . Since $Δ f$ is continuous, [F3] applied to $Δ f$ gives $M_{Δ f} (x, r) = A (x, r) + \frac{r}{n} \partial_{r} A (x, r)$ . Differentiating the first identity in $r$ gives $M_{r r} (x, r) = \frac{1}{n} A (x, r) + \frac{r}{n} \partial_{r} A (x, r)$ ; therefore $M_{r r} + \frac{n - 1}{r} M_{r} = \frac{1}{n} A + \frac{r}{n} \partial_{r} A + \frac{n - 1}{n} A = A + \frac{r}{n} \partial_{r} A = M_{Δ f} (x, r) = Δ_{x} M (x, r)$ . The radial-derivative formula is used only with the $C^{2}$ function $f$ ; no differentiability of $Δ f$ is assumed.

1.3F4algebra

The limits at $r ↓ 0$ . For $0 < r \leq 1$ the bound $∣ A_{Δ f} (x, r) ∣ \leq \sup_{B_{1} (x)} ∣ Δ f ∣ < \infty$ holds, the supremum being finite by [F4]; hence $M_{r} (x, r) = \frac{r}{n} A_{Δ f} (x, r) \to 0$ . Moreover the identity just proved gives $M_{r r} (x, r) + \frac{n - 1}{r} M_{r} (x, r) = M_{Δ f} (x, r) = Δ_{x} M (x, r)$ . Since $Δ f$ is continuous at $x$ , $∣ M_{Δ f} (x, r) - Δ f (x) ∣ \leq \sup_{ω \in S^{n - 1}} ∣ Δ f (x + r ω) - Δ f (x) ∣ \to 0$ as $r ↓ 0$ .

1.4F1algebra

The space-time version. If $u \in C^{2}$ solves $□_{c} u = 0$ , applying the differentiation-under-the-sphere-integral computation of [F1] to the $C^{2}$ function $(x, t) \mapsto u (x, t)$ yields $Δ_{x} M_{u} (x, r, t) = M_{Δ_{x} u} (x, r, t)$ and $\partial_{t}^{2} M_{u} (x, r, t) = M_{u_{t t}} (x, r, t)$ for all $r > 0$ and $t \in I$ . Since $u_{t t} = c^{2} Δ u$ , this gives $\partial_{t}^{2} M_{u} = c^{2} M_{Δ u} = c^{2} Δ_{x} M_{u}$ ; and the identity of the first two steps applied to the $C^{2}$ spatial function $u (\cdot, t)$ gives $Δ_{x} M_{u} (x, r, t) = M_{r r} (x, r, t) + \frac{n - 1}{r} M_{r} (x, r, t)$ . Substituting, $\partial_{t}^{2} M_{u} = c^{2} (M_{r r} + \frac{n - 1}{r} M_{r})$ .

2.1given∎

Collecting: the Euler–Poisson–Darboux identity holds for every $C^{2}$ datum, its right-hand side has the stated continuous extension at $r = 0$ with value $Δ f (x)$ , and the space-time means of solutions satisfy the same radial equation with two time derivatives on the left.

Depends on

Used by

Dependency tree · two levels

65 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)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)