LemmaStatement: Literature-sourcedProof: AI-generatedprecheck pass

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.

A transport equation restricts to a linear ODE along each characteristic

Statement

Let $u \in C^{1} (Ω)$ satisfy

$u_{t} + a \cdot \nabla_{x} u + c u = f,$

and let $X$ be a characteristic solving $X^{'} (s) = a (X (s), s)$ . Then

$\frac{d}{d s} u (X (s), s) + c (X (s), s) u (X (s), s) = f (X (s), s) .$

Facts & Assumptions

Given: A $C^{1}$ solution $u$ of the transport equation and a characteristic $X$ .

[L1]

A linear transport equation and its characteristics are defined by the displayed PDE and ODE (Linear transport equations and their characteristic flow).

[L2]

The total-derivative chain rule differentiates a composite by the gradient of the outer function applied to the derivative of the inner function (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L3]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: continuous first partial derivatives on an open set imply total differentiability, with the Jacobian as derivative. Thus the stated $C^{1}$ function $u$ is totally differentiable at each point of its domain.

Proof

technique · direct

1.1L2L3

By [L3], $u$ is totally differentiable. The differentiable characteristic has the first-order expansion $X (s + h) = X (s) + h X^{'} (s) + o (h)$ coordinatewise, so its space-time curve is totally differentiable with derivative $(X^{'} (s), 1)$ . Apply [L2] to the map $s \mapsto u (X (s), s)$ ; since the space-time velocity of the characteristic is $(X^{'} (s), 1)$ , this gives $\frac{d}{d s} u (X (s), s) = u_{t} (X (s), s) + \nabla_{x} u (X (s), s) \cdot X^{'} (s)$ .

2.1L1step 1.1∎

By [L1], the characteristic ODE gives $X^{'} (s) = a (X (s), s)$ , so substituting into step 1.1 and then using the PDE yields $\frac{d}{d s} u (X (s), s) = f (X (s), s) - c (X (s), s) u (X (s), s)$ , which is the claimed scalar linear ODE along the characteristic.

Depends on

Used by

Dependency tree · two levels

16 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 (standard reference, not scraped)