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 iterated radial-derivative identity behind the odd-dimensional reduction

Statement

Let $k \geq 1$ and let $D_{r} : = r^{- 1} \partial_{r}$ be the radial derivative on $(0, \infty)$ . For every $f \in C^{k + 1} ((0, \infty))$ , $\frac{\partial^{2}}{\partial r^{2}} D_{r}^{k - 1} (r^{2 k - 1} f (r)) = D_{r}^{k - 1} [r^{2 k - 1} \frac{1}{r^{2 k}} \frac{\partial}{\partial r} (r^{2 k} \partial_{r} f (r))]$ on $(0, \infty)$ . Both sides are finite combinations of derivatives of $f$ computed by the product and quotient rules; no integral and no differential equation for $f$ is used.

Facts & Assumptions

Given: an integer $k \geq 1$ , a function $f \in C^{k + 1} ((0, \infty))$ , and the operator $D_{r} = r^{- 1} \partial_{r}$ acting on functions on $(0, \infty)$ .

[F1]

Sums, products, quotients of differentiable functions are differentiable, with the usual sum, product, quotient rules; nonnegative integer powers are differentiated by repeated product rules, and reciprocals by the quotient rule on nonzero 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$ ).

Proof

1.1F1given

Put $g : = r^{2 k - 1} f$ , so that $g \in C^{k + 1} ((0, \infty))$ and $f = r^{1 - 2 k} g$ . The left-hand side is $\partial_{r}^{2} D_{r}^{k - 1} g$ , and for the right-hand side the product rule gives $r^{2 k} \partial_{r} f = (1 - 2 k) g + r g^{'}$ , hence $r^{- 1} \partial_{r} (r^{2 k} \partial_{r} f) = g^{''} + (2 - 2 k) r^{- 1} g^{'}$ ; since $r^{2 k - 1} r^{- 2 k} = r^{- 1}$ , the right-hand side is $D_{r}^{k - 1} (g^{''} + (2 - 2 k) r^{- 1} g^{'})$ . It therefore suffices to prove $\partial_{r}^{2} D_{r}^{k - 1} g = D_{r}^{k - 1} (g^{''} + (2 - 2 k) r^{- 1} g^{'})$ for every $g \in C^{k + 1} ((0, \infty))$ , which is what the following steps do.

1.2F1algebra

On $(0, \infty)$ the operators satisfy $\partial_{r} = r D_{r}$ , hence $\partial_{r}^{2} = \partial_{r} (r D_{r}) = D_{r} + r^{2} D_{r}^{2}$ ; and for every $j \geq 1$ and every $v \in C^{j} ((0, \infty))$ one has $D_{r}^{j} (r^{2} v) = r^{2} D_{r}^{j} v + 2 j D_{r}^{j - 1} v$ . The last identity is proved by induction on $j$ : for $j = 1$ , $D_{r} (r^{2} v) = r^{- 1} (2 r v + r^{2} v^{'}) = 2 v + r^{2} D_{r} v$ ; and if it holds for $j$ , then $D_{r}^{j + 1} (r^{2} v) = D_{r} (r^{2} D_{r}^{j} v + 2 j D_{r}^{j - 1} v) = r^{2} D_{r}^{j + 1} v + 2 D_{r}^{j} v + 2 j D_{r}^{j} v = r^{2} D_{r}^{j + 1} v + 2 (j + 1) D_{r}^{j} v$ .

1.3F1algebra

Fix $g \in C^{k + 1} ((0, \infty))$ . If $k = 1$ , then $D_{r}^{k - 1} (r^{2} D_{r}^{2} g) = r^{2} D_{r}^{2} g = r^{2} D_{r}^{k + 1} g + 2 (k - 1) D_{r}^{k} g$ directly; if $k \geq 2$ , the second identity of the previous step with $j = k - 1$ and $v = D_{r}^{2} g$ gives the same equality. Also $g^{''} = \partial_{r}^{2} g = D_{r} g + r^{2} D_{r}^{2} g$ by the first identity of the previous step, so $D_{r}^{k - 1} g^{''} = D_{r}^{k} g + D_{r}^{k - 1} (r^{2} D_{r}^{2} g) = r^{2} D_{r}^{k + 1} g + (2 k - 1) D_{r}^{k} g$ . Moreover $r^{- 1} g^{'} = D_{r} g$ , so $D_{r}^{k - 1} ((2 - 2 k) r^{- 1} g^{'}) = (2 - 2 k) D_{r}^{k} g$ .

2.1F1algebra∎

Adding the two pieces of the previous step gives $D_{r}^{k - 1} (g^{''} + (2 - 2 k) r^{- 1} g^{'}) = r^{2} D_{r}^{k + 1} g + (2 k - 1 + 2 - 2 k) D_{r}^{k} g = r^{2} D_{r}^{k + 1} g + D_{r}^{k} g$ , and by the first identity of the second step this last quantity is $\partial_{r}^{2} D_{r}^{k - 1} g$ . This proves the equivalent identity for $g$ and hence, by the substitution of the first step, the identity of the statement.

Depends on

Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$

Used by

The odd-dimensional wave formula by iterated spherical means Theorem

Dependency tree · two levels

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