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.

Duhamel's principle for the wave equation

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ , $n \geq 2$ , $T > 0$ and let $f : R^{n} \times [0, T] \to R$ be continuous, compactly supported in $x$ for each fixed $s$ , with all spatial derivatives $D_{x}^{α} f$ through order $q : = ⌊ n / 2 ⌋ + 1$ existing and jointly continuous on $R^{n} \times [0, T]$ . Thus every slice is in the velocity-data class, and the additional derivatives needed to differentiate the launched solution twice are jointly continuous. No time derivative of $f$ is required. For an admissible velocity datum $g$ let $W [g] (x, τ)$ be the homogeneous solution constructed from the formulas above with zero displacement and velocity datum $g$ , so that, by The dimension formulas attain the Cauchy data, $W [g] (x, 0) = 0$ and $\partial_{τ} W [g] (x, 0) = g (x)$ . Then $u (x, t) : = \int_{0}^{t} W [f (\cdot, s)] (x, t - s) d s (0 \leq t \leq T)$ is a $C^{2}$ function with $u (\cdot, 0) = u_{t} (\cdot, 0) = 0$ and $u_{t t} = c^{2} Δ u + f$ on $R^{n} \times (0, T)$ .

Facts & Assumptions

Given: Countable Choice, $c > 0$ , $n \geq 2$ , a source $f$ of the stated class, and for each admissible $g$ the launched solution $W [g]$ with $W [g] (x, 0) = 0$ , $\partial_{τ} W [g] (x, 0) = g (x)$ .

[F1]

The formulas of the page define $C^{2}$ solutions of the homogeneous equation on $R^{n} \times (0, \infty)$ for admissible data, and the data are attained in the limit sense (The dimension formulas attain the Cauchy data).

[F2]

Let $α, β \in C^{1} (I)$ with $α < β$ and let $F$ be continuous on $I \times J$ with continuous $\partial_{t} F$ , where $J$ contains the closure of the union of the intervals $[α (t), β (t)]$ . Then $G (t) = \int_{α (t)}^{β (t)} F (t, y) d y$ is $C^{1}$ with $G^{'} (t) = F (t, β (t)) β^{'} (t) - F (t, α (t)) α^{'} (t) + \int_{α (t)}^{β (t)} \partial_{t} F (t, y) d y$ (Differentiating an integral with moving endpoints).

[F3]

In odd dimension $n = 2 k + 1$ , a zero-displacement launch is $W [g] (x, τ) = a^{- 1} \sum_{j = 0}^{k - 1} α_{k, j} τ^{j + 1} \partial_{τ}^{j} M_{g} (x, c τ)$ , $a = (2 k - 1)!!$ , by Radial-derivative expansion of the Euler–Poisson–Darboux transform and its zero-radius limit. The signed-radius mean is $C^{k + 1}$ (Smoothness, parity and zero-radius limits of spherical means). Differentiating this finite sum through total order two involves at most $k + 1$ spatial derivatives of $g$ and nonnegative powers of $τ$ . For $g = f (\cdot, s)$ , the uniform integral estimate in the smoothness lemma applies also with the continuous parameter $s$ : the assumed joint continuity on compact spatial-time sets makes $W$ and its first two $(x, τ)$ derivatives jointly continuous, including at $τ = 0$ . In even dimension use the cylindrical launch in dimension $n + 1$ from The even-dimensional wave formula by descent, with the same derivative order $q = k + 1$ .

Proof

1.1F1F2F3

First derivative. The launched solutions vanish at $τ = 0$ and have velocity $g$ there by [F1]: $W [g] (x, 0) = 0$ and $\partial_{τ} W [g] (x, 0) = g (x)$ . Applying [F2] to the moving-endpoint integral $u (x, t) = \int_{0}^{t} W [f (\cdot, s)] (x, t - s) d s$ in the form $G (t) = \int_{0}^{t} F (t, s) d s$ with $F (t, s) = W [f (\cdot, s)] (x, t - s)$ — defined also for negative $t - s$ by the signed-radius finite sum in [F3]; extend the source slices constantly for $s < 0$ and $s > T$ . Then $F$ and its first two $t$ -derivatives are continuous on a rectangular neighbourhood of the integration region by [F3] — gives $u_{t} (x, t) = \int_{0}^{t} \partial_{t} W [f (\cdot, s)] (x, t - s) d s + W [f (\cdot, t)] (x, 0) = \int_{0}^{t} \partial_{t} W [f (\cdot, s)] (x, t - s) d s$ , since $W [\cdot] (x, 0) = 0$ ; in particular $u (\cdot, 0) = 0$ and $u_{t} (\cdot, 0) = 0$ .

1.2F1F2F3algebra

Second derivative. Differentiating once more with [F2], $u_{t t} (x, t) = \partial_{t} W [f (\cdot, t)] (x, 0) + \int_{0}^{t} \partial_{t}^{2} W [f (\cdot, s)] (x, t - s) d s = f (x, t) + \int_{0}^{t} c^{2} Δ_{x} W [f (\cdot, s)] (x, t - s) d s = f (x, t) + c^{2} Δ_{x} u (x, t)$ , where the last equality uses $\partial_{τ} W [f (\cdot, t)] (x, 0) = f (x, t)$ and the homogeneous equation for every launched solution from [F1]. To justify moving $Δ_{x}$ through the integral, fix any compact set of $x$ -values and a compact time interval $[0, T_{0}] \subseteq [0, T]$ . By [F3], the integrand and its first two $x$ -derivatives are jointly continuous on the resulting compact $(x, s, t - s)$ parameter set; applying [F2] twice with the fixed $s$ -interval endpoints therefore permits differentiating under the $s$ -integral locally in $x$ . The mixed derivative $u_{t x}$ is obtained similarly from the integral formula for $u_{t}$ . These derivative integrals and their boundary terms are continuous; their bounds on local compact sets give continuous one-sided derivatives also at $t = 0, T$ . No common compact support of all source slices is needed.

2.1given∎

Hence $u$ is $C^{2}$ with zero Cauchy data and $u_{t t} - c^{2} Δ u = f$ on $R^{n} \times (0, T)$ ; the constructed $u$ is a classical solution of the forced problem.

Depends on

Used by

The forced three-dimensional version as a retarded potential Theorem

Dependency tree · two levels

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