LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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 moving jump is a weak solution exactly under Rankine–Hugoniot

Statement

For a conservation system as in Strictly hyperbolic conservation systems and characteristic families, constant states $u_{L}, u_{R} \in G$ , and a constant speed $s$ , define $u (t, x) = u_{L}$ for $x < s t$ and $u (t, x) = u_{R}$ for $x > s t$ , and let $u_{0} (x) = u_{L}$ for $x < 0$ and $u_{0} (x) = u_{R}$ for $x > 0$ (values on the jump lines are immaterial). Then $u$ is a distributional weak solution with initial datum $u_{0}$ in the sense of Strictly hyperbolic conservation systems and characteristic families if and only if $f (u_{R}) - f (u_{L}) = s (u_{R} - u_{L}) .$

Facts & Assumptions

Given: A system as in Strictly hyperbolic conservation systems and characteristic families, states $u_{L}, u_{R} \in G$ , and the jump at speed $s$ .

[F1]

Rankine–Hugoniot jumps and Lax shocks: a Rankine–Hugoniot jump is exactly the algebraic equality $[f] = s [u]$ .

[F2]

Strictly hyperbolic conservation systems and characteristic families: a distributional weak solution with initial data satisfies the vector test-function identity for the PDE and converges to that datum in $L_{l o c}^{1}$ as $t ↓ 0$ .

Proof

1.1givenF2algebra

Write $u = u_{L} + [u] H (x - s t)$ and $f (u) = f (u_{L}) + [f] H (x - s t)$ , where $H$ is the unit step and $[u] = u_{R} - u_{L}$ , $[f] = f (u_{R}) - f (u_{L})$ . Testing against a smooth compactly supported function and integrating by parts on the two sides of the line $x = s t$ gives $\partial_{t} u = - s [u] δ_{x = s t}$ and $\partial_{x} f = [f] δ_{x = s t}$ .

1.2givenF2algebra

For every compact $K \subset R$ , the functions $u (t, \cdot)$ and $u_{0}$ agree almost everywhere outside the interval with endpoints $0$ and $s t$ . Hence $∥ u (t, \cdot) - u_{0} ∥_{L^{1} (K)} \leq ∣ s ∣ t ∥ u_{R} - u_{L} ∥_{2} ⟶ 0$ as $t ↓ 0$ . Thus the required local $L^{1}$ initial trace holds.

2.1step 1.1step 1.2F1F2algebra∎

By step 1.1 the distributional PDE identity holds exactly when $[f] = s [u]$ , which is [F1]. Step 1.2 supplies the initial trace in either case, so the definition of weak solution gives both implications.

Depends on

Used by

Dependency tree · two levels

4 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

Randall J. LeVeque, Numerical Methods for Conservation Laws (standard reference, not scraped)