PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Classical solutions are distributional weak solutions, and conversely

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the injectivity interface below. Let $n \geq 1$ , $T > 0$ , $f \in C^{1} (R; R^{n})$ and $u_{0} \in L^{\infty} (R^{n}) \cap L_{l o c}^{1} (R^{n})$ .

(i) If $u \in C^{1} (Π_{T}) \cap C^{0} ([0, T]; L_{l o c}^{1} (R^{n})) \cap L^{\infty} (Π_{T})$ satisfies $u_{t} + {div}_{x} f (u) = 0$ pointwise in $Π_{T}$ and has initial trace $u (\cdot, t) \to u_{0}$ in $L_{l o c}^{1}$ as $t ↓ 0$ , then $u$ is a distributional weak solution in the sense of Distributional weak solutions of the Cauchy problem.

(ii) Conversely, if $u$ is a bounded distributional weak solution, $u \in C^{1} (Π_{T})$ , and $u (\cdot, t)$ has an $L_{l o c}^{1}$ -continuous trace ${\overset{ˉ}{u}}_{0}$ as $t ↓ 0$ , then $u_{t} + {div}_{x} f (u) = 0$ pointwise in $Π_{T}$ and ${\overset{ˉ}{u}}_{0} = u_{0}$ as $L_{l o c}^{1}$ equivalence classes.

The initial-trace conclusion is an almost-everywhere class equality; no pointwise representative on $t = 0$ is asserted (Scalar conservation laws, fluxes and Cauchy data).

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $T > 0$ , $f \in C^{1} (R; R^{n})$ , $u_{0} \in L^{\infty} \cap L_{l o c}^{1}$ , a classical solution $u \in C^{1} (Π_{T})$ satisfying $u_{t} + {div}_{x} f (u) = 0$ pointwise with an $L_{l o c}^{1}$ initial trace (i), and, in (ii), a bounded distributional weak solution $u \in C^{1} (Π_{T})$ with an $L_{l o c}^{1}$ -continuous initial trace ${\overset{ˉ}{u}}_{0}$ .

[F1]

For a $C^{1}$ function $u$ the composition $f (u)$ is $C^{1}$ with ${div}_{x} f (u) = f^{'} (u) \cdot \nabla_{x} u$ , by the chain rule and the algebra of derivatives; the Laplacian-free flux is locally integrable on compact space--time boxes (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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$ , Scalar conservation laws, fluxes and Cauchy data).

[F2]

Integration by parts on a box follows coordinatewise from The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ and Fubini's theorem for L^1 functions on a sigma-finite product applied to the $C^{1}$ products $u φ$ and $f_{i} (u) φ$ . Compact support kills spatial and terminal faces. No surface divergence theorem is used.

[F3]

A continuous function on an open set whose integral against every compactly supported smooth test function vanishes is identically zero there; testing against a translate of a fixed nonzero smooth compactly supported bump gives a nonzero pairing where the function does not vanish (Explicit compactly supported smooth cutoffs).

[F4]

Under Countable Choice, two locally integrable functions with equal pairings against every smooth compactly supported test represent the same almost-everywhere class (Locally integrable functions embed in distributions).

Proof

technique · direct

1.1F1F2

Fix $φ \in C_{c}^{\infty} (R^{n} \times (- \infty, T))$ and choose $Q_{R} = (- R, R)^{n}$ and $τ$ with $supp φ \subset Q_{R} \times (- \infty, τ)$ , $τ < T$ . Multiplying the pointwise equation by $φ$ and integrating over $Q_{R} \times (δ, τ)$ , $0 < δ < τ$ , [F2] gives $0 = \int_{Q_{R}} u φ ∣_{δ}^{τ} d x - \int_{δ}^{τ} ⁣ ⁣ \int_{Q_{R}} u φ_{t} - \int_{δ}^{τ} ⁣ ⁣ \int_{Q_{R}} f (u) \cdot \nabla_{x} φ$ , since $φ$ vanishes on the lateral and terminal faces.

1.2F1F3given

For (ii), test the weak identity with $φ \in C_{c}^{\infty} (Π_{T})$ (so $φ = 0$ near $t = 0$ ): integration by parts over the support of $φ$ gives $0 = \int_{Π_{T}} (u φ_{t} + f (u) \cdot \nabla_{x} φ) = - ⟨ u_{t} + {div}_{x} f (u), φ ⟩$ , where the residual $R : = u_{t} + {div}_{x} f (u)$ is continuous by [F1]. By [F3] applied on the open set $Π_{T}$ , $R \equiv 0$ , so the equation holds pointwise.

2.1F2givenstep 1.1

In step 1.1 the terminal term vanishes and $φ (\cdot, δ) \to φ (\cdot, 0)$ uniformly on the compact spatial support while $u (\cdot, δ) \to u_{0}$ in $L_{l o c}^{1}$ ; letting $δ ↓ 0$ gives $\int_{Π_{T}} (u φ_{t} + f (u) \cdot \nabla_{x} φ) d x d t + \int_{R^{n}} u_{0} φ (\cdot, 0) d x = 0$ , which is the weak formulation for this test function. As $φ$ was arbitrary, (i) holds.

3.1F2F4givenstep 1.2step 2.1∎

Identification of the trace. Fix $ψ \in C_{c}^{\infty} (R^{n})$ and $β \in C_{c}^{\infty} ((- \infty, T))$ with $β (0) = 1$ . The pointwise equation from step 1.2, integrated on a box times $(δ, τ)$ containing the positive-time support of $ψ β$ , gives the calculation of steps 1.1 and 2.1 with trace ${\overset{ˉ}{u}}_{0}$ . Hence $\int_{Π_{T}} (u φ_{t} + f (u) \cdot \nabla φ) + \int {\overset{ˉ}{u}}_{0} ψ = 0$ for $φ = ψ β$ . Subtract the given weak identity, whose bottom term is $\int u_{0} ψ$ , to get $\int ({\overset{ˉ}{u}}_{0} - u_{0}) ψ = 0$ . By [F4], ${\overset{ˉ}{u}}_{0} = u_{0}$ almost everywhere.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

G. A. Chechkin and A. Yu. Goritsky (translated by B. Andreianov), “S. N. Kruzhkov’s lectures on first-order quasilinear PDEs,” in Analytical and Numerical Aspects of PDEs, de Gruyter 2009, complete lecture-notes text (standard reference, not scraped)
S. N. Kruzhkov, “First order quasilinear equations in several independent variables,” Mat. USSR-Sbornik 10 (1970), 217–243, complete English translation (standard reference, not scraped)