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.

Sphere integrals of a cylindrical function project to weighted ball integrals

Statement

Assume the Axiom of Countable Choice. Let $n \geq 1$ and $g \in C^{0} (R^{n})$ , and let $G (ξ, z) : = g (ξ)$ be the extension of $g$ to $R^{n + 1}$ independent of the last coordinate. For $r > 0$ and $x \in R^{n}$ , with $S_{r}^{n} (x) = {(ξ, z) \in R^{n + 1} : ∣ ξ - x ∣^{2} + z^{2} = r^{2}}$ the sphere of radius $r$ in $R^{n + 1}$ and $ω_{n} = ∣ S^{n} ∣$ its total polar measure (The polar surface set function on the unit sphere), $\int_{S_{r}^{n} (x)} G d S = 2 r \int_{B_{r}^{n} (x)} \frac{g (y)}{\sqrt{r^{2} - ∣ y - x ∣^{2}}} d y,$ and the spherical mean of $G$ over $S_{r}^{n} (x)$ equals $\frac{2}{ω_{n} r^{n - 1}} \int_{B_{r}^{n} (x)} \frac{g (y)}{\sqrt{r^{2} - ∣ y - x ∣^{2}}} d y$ . In particular, for even $n = 2 k$ , every $c > 0$ and $t > 0$ , with $W_{g}$ the weighted ball integral of Spherical means and the weighted ball integral of space-dependent data, $t^{n - 1} M_{G} ((x, 0), c t) = \frac{(n - 1)!!}{c^{n - 1}} W_{g} (x, c t),$ where $M_{G}$ is the $(n + 1)$ -dimensional spherical mean of $G$ with centre $(x, 0)$ . The connecting constant identity is $2 n!! V_{n} / ω_{n} = (n - 1)!!$ .

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $g \in C^{0} (R^{n})$ , the cylindrical extension $G (ξ, z) = g (ξ)$ , and $r > 0$ , $x \in R^{n}$ .

[F1]

Surface measure is chart-independent; in graph coordinates $(y, h (y))$ its density is $\sqrt{1 + ∣ D h (y) ∣^{2}}$ (Surface integration on compact C1 hypersurfaces, Chart and partition independence of surface measure). On spheres it agrees with polar measure and scales by the appropriate radius power (Agreement with the existing polar sphere measure).

[F2]

Under Countable Choice, $\int_{R^{n}} f d λ_{n} = \int_{0}^{\infty} \int_{S^{n - 1}} f (s θ) s^{n - 1} d σ (θ) d s$ for every Borel $f : R^{n} \to [0, \infty]$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F3]

$∣ \partial B_{r}^{m} ∣ = ω_{m - 1} r^{m - 1}$ and $∣ B_{r}^{m} ∣ = ω_{m - 1} r^{m} / m$ , so in particular $∣ S_{r}^{n} (x) ∣ = ω_{n} r^{n}$ for the sphere in $R^{n + 1}$ and $ω_{m} = (m + 1) V_{m + 1}$ for the unit sphere $S^{m}$ (Sphere and ball measures scale in Rn).

[F4]

$V_{m} = π^{m / 2} / Γ (m / 2 + 1)$ for every $m \geq 1$ (The closed form for the volume of the unit $n$ -ball).

[F5]

$Γ (s + 1) = s Γ (s)$ for $s > 0$ with $Γ (1) = 1$ (The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ ); $Γ (1 / 2) = \sqrt{π}$ ( $Γ (1 / 2) = \sqrt{π}$ from the Gaussian integral); $Γ (m + 1) = m!$ for every integer $m \geq 0$ (Gamma at the positive integers).

Proof

1.1F1algebra

Graph sheets. The upper and lower open hemispheres of $S_{r}^{n} (x)$ are the graphs $y \mapsto (y, \pm \sqrt{r^{2} - ∣ y - x ∣^{2}})$ over $B_{r}^{n} (x)$ . Their graph density is $\sqrt{1 + ∣ y - x ∣^{2} / (r^{2} - ∣ y - x ∣^{2})} = r / \sqrt{r^{2} - ∣ y - x ∣^{2}}$ by [F1]. The equator has zero surface measure: near each of its points choose a sphere graph omitting a nonzero one of the first $n$ coordinates. Its parameter set for the equator lies in the coordinate hyperplane $z = 0$ , which has Lebesgue measure zero (for $n = 1$ , it is a singleton, null because it lies in intervals of arbitrarily small length); Fubini's theorem for L^1 functions on a sigma-finite product applied to its indicator proves nullity, and the continuous graph density preserves it. A finite chart cover suffices by compactness of the sphere (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).

1.2F1F2algebra

Integrating the two sheets gives $\int_{S_{r}^{n} (x)} G d S = 2 r \int_{B_{r}^{n} (x)} g (y) (r^{2} - ∣ y - x ∣^{2})^{- 1 / 2} d y$ . These integrals are absolutely convergent: $g$ is bounded on the closed ball by A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, and [F2] reduces the weight integral to $ω_{n - 1} \int_{0}^{r} s^{n - 1} (r^{2} - s^{2})^{- 1 / 2} d s$ , bounded by $ω_{n - 1} r^{n - 1} \int_{0}^{r} (r^{2} - s^{2})^{- 1 / 2} d s = ω_{n - 1} r^{n - 1} π / 2$ . Thus the graph computation applies separately to positive and negative parts.

1.3F3algebra

The mean. By [F3], $∣ S_{r}^{n} (x) ∣ = ω_{n} r^{n}$ , so the spherical mean of $G$ over $S_{r}^{n} (x)$ is $ω_{n}^{- 1} r^{- n} \int_{S_{r}^{n} (x)} G d S = \frac{2}{ω_{n} r^{n - 1}} \int_{B_{r} (x)} \frac{g (y)}{\sqrt{r^{2} - ∣ y - x ∣^{2}}} d y$ .

1.4F3F4F5algebra

The even-dimensional form. Let $n = 2 k$ be even, $c > 0$ , $t > 0$ and $r = c t$ . Substituting $r = c t$ in the mean identity, $t^{n - 1} M_{G} ((x, 0), c t) = \frac{2}{ω_{n} c^{n - 1}} \int_{B_{c t} (x)} \frac{g (y)}{\sqrt{c^{2} t^{2} - ∣ y - x ∣^{2}}} d y = \frac{2 n!! V_{n}}{ω_{n} c^{n - 1}} W_{g} (x, c t)$ by the definition of $W_{g}$ . For the constant: $V_{n} = π^{n / 2} / Γ (k + 1) = π^{k} / k!$ by [F4]; the functional equation and $Γ (1 / 2) = \sqrt{π}$ give by induction $Γ (k + 1 / 2) = \frac{(2 k - 1) (2 k - 3) \dots 1}{2^{k}} \sqrt{π} = \frac{(2 k)! \sqrt{π}}{4^{k} k!}$ , so with $ω_{n} = ∣ S^{n} ∣ = (n + 1) V_{n + 1} = \frac{2 π^{k + 1 / 2}}{Γ (k + 1 / 2)} = \frac{2^{2 k + 1} π^{k} k!}{(2 k)!}$ one gets $2 n!! V_{n} = 2 \cdot 2^{k} k! \cdot π^{k} / k! = 2^{k + 1} π^{k}$ and $\frac{2 n!! V_{n}}{ω_{n}} = \frac{2^{k + 1} π^{k} (2 k)!}{2^{2 k + 1} π^{k} k!} = \frac{(2 k)!}{2^{k} k!} = (2 k - 1)!! = (n - 1)!!$ .

2.1algebra∎

Substituting the constant gives $t^{n - 1} M_{G} ((x, 0), c t) = \frac{(n - 1)!!}{c^{n - 1}} W_{g} (x, c t)$ , which together with the two integral identities proves all assertions.

Depends on

Used by

The dimension formulas attain the Cauchy data Lemma
Poisson's formula in two dimensions by descent Theorem
The even-dimensional wave formula by descent Theorem

Dependency tree · two levels

104 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

Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)