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 d'Alembert expression attains both initial data

Statement

Let $c > 0$ , $u_{0} \in C^{2} (R)$ , $u_{1} \in C^{1} (R)$ and let $A$ be the d'Alembert expression of d'Alembert's formula and uniqueness in one dimension, $A (x, t) : = \frac{1}{2} (u_{0} (x - c t) + u_{0} (x + c t)) + \frac{1}{2 c} \int_{x - c t}^{x + c t} u_{1} (y) d y .$ Then $A \in C^{2} (R \times [0, \infty))$ , $A (x, 0) = u_{0} (x)$ for every $x$ , and $\partial_{t} A (x, t) = \frac{1}{2} (- c u_{0}^{'} (x - c t) + c u_{0}^{'} (x + c t)) + \frac{1}{2} (u_{1} (x + c t) + u_{1} (x - c t)),$ so $\partial_{t} A (x, 0) = u_{1} (x)$ . The orientation of the velocity integral is the $+$ sign in the second bracket: both ends of the characteristic base are traversed with speed $c$ , and the two endpoint contributions add.

Facts & Assumptions

Given: a speed $c > 0$ , data $u_{0} \in C^{2} (R)$ , $u_{1} \in C^{1} (R)$ , and the expression $A$ of the statement.

[F1]

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

[F2]

Sums, constant multiples of differentiable functions are differentiable with the usual rules (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$ ).

[F3]

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)$ ). 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).

Proof

1.1algebra

Displacement at $t = 0$ . At $t = 0$ the two displacement terms are both $u_{0} (x)$ and the integral has equal endpoints, so $A (x, 0) = \frac{1}{2} (u_{0} (x) + u_{0} (x)) + 0 = u_{0} (x)$ for every $x \in R$ .

1.2F1F2F3algebra

Velocity. For $t > 0$ , by [F1] applied to the integral term with $α (t) = x - c t$ , $β (t) = x + c t$ , $α^{'} (t) = - c$ , $β^{'} (t) = c$ and inner integrand $u_{1}$ , $\partial_{t} A (x, t) = \frac{1}{2} (- c u_{0}^{'} (x - c t) + c u_{0}^{'} (x + c t)) + \frac{1}{2 c} (c u_{1} (x + c t) + c u_{1} (x - c t)) = \frac{1}{2} (- c u_{0}^{'} (x - c t) + c u_{0}^{'} (x + c t)) + \frac{1}{2} (u_{1} (x + c t) + u_{1} (x - c t))$ ; the displacement term is differentiated by [F2] and [F3]. Continuity of the data and the $C^{2}$ regularity supplied by d'Alembert's formula and uniqueness in one dimension extend this derivative formula to $t = 0$ .

2.1F1algebra∎

Setting $t = 0$ in the velocity formula gives $\partial_{t} A (x, 0) = \frac{1}{2} (- c u_{0}^{'} (x) + c u_{0}^{'} (x)) + \frac{1}{2} (u_{1} (x) + u_{1} (x)) = u_{1} (x)$ ; the regularity $A \in C^{2} (R \times [0, \infty))$ is established in d'Alembert's formula and uniqueness in one dimension. Hence $A$ attains both initial data, and the two endpoint contributions of the velocity integral add with a $+$ sign as displayed.

Depends on

Used by

Dependency tree · two levels

31 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 #10: Introduction to the Wave Equation (Fall 2011) (standard reference, not scraped)