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.

Backward uniqueness for the heat equation on a bounded interval

Statement

Assume Countable Choice. Let $T > 0$ , $Q = (0, π) \times (0, T]$ , and say that a function $w : \overline{Q} \to R$ is of class $C^{4, 2} (\overline{Q})$ when it is continuous on $\overline{Q}$ and all ordered partial derivatives containing at most four $x$ derivatives and at most two $t$ derivatives exist on $Q$ and extend continuously to $\overline{Q}$ . Suppose $w \in C^{4, 2} (\overline{Q})$ satisfies $w_{t} = w_{x x} in Q, w (0, t) = w (π, t) = 0 (0 \leq t \leq T), w (x, T) = 0 (0 \leq x \leq π) .$ Then $w \equiv 0$ on $\overline{Q}$ . No hypothesis on the initial face $t = 0$ is imposed: the vanishing is forced by the lateral and terminal conditions alone. Consequently two solutions of the interval Dirichlet problem in this class with zero lateral data and the same terminal data coincide, and the terminal-to-initial map is well defined on the class of terminal data of such solutions.

Facts & Assumptions

Given: Countable Choice, $T > 0$ , $Q = (0, π) \times (0, T]$ , and $w \in C^{4, 2} (\overline{Q})$ with $w_{t} = w_{x x}$ in $Q$ , $w (0, t) = w (π, t) = 0$ for $0 \leq t \leq T$ and $w (x, T) = 0$ for $0 \leq x \leq π$ .

[A1]

Countable Choice is the ambient hypothesis (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

If $f$ satisfies the hypotheses of the differentiation-under-the-integral theorem, then $F (t) = \int f (x, t) d μ (x)$ is differentiable with $F^{'} = \int \partial_{t} f d μ$ (Differentiation under the integral sign).

[F2]

For $u, v$ differentiable on $[a, b]$ with integrable derivatives, $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ).

[F3]

A continuous function on $[a, b]$ is bounded and Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F4]

A bounded Riemann integrable function on $[a, b]$ is Lebesgue integrable with the same integral (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[F5]

$\int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ for $f, g \in L^{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ).

[F6]

A twice differentiable function on an open interval is convex exactly when its second derivative is nonnegative (A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative).

[F7]

Convexity is the convex-combination inequality (Convex, strictly convex, concave, strictly concave, and midpoint-convex real functions on an interval).

[F8]

$\log : (0, \infty) \to R$ is continuous, strictly increasing and onto $R$ , with $\log (x y) = \log x + \log y$ and $\log 1 = 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F9]

$\log^{'} (x) = 1 / x$ for $x > 0$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F10]

The rectangle $[0, π] \times [0, T]$ is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Open cover, subcover, compact metric space, and compact subset of a metric space), and a continuous real function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F11]

Dominated convergence (Dominated convergence).

[F12]

The product and quotient rules for derivatives, in particular $(f / g)^{'} = (f^{'} g - f g^{'}) / g^{2}$ where $g \neq 0$ (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$ ).

[F13]

A continuous function whose derivative is nonpositive is nonincreasing (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed); the derivative of $\log \circ E$ uses 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)$ .

Proof

Given: Countable Choice, $T > 0$ , $w \in C^{4, 2} (\overline{Q})$ with $w_{t} = w_{x x}$ in $Q$ , $w (0, t) = w (π, t) = 0$ for $0 \leq t \leq T$ , and $w (x, T) = 0$ for $0 \leq x \leq π$ .

1.1A1F3F4F10F11given

Define $E (t) : = \frac{1}{2} \int_{0}^{π} w (x, t)^{2} d x$ for $t \in [0, T]$ ; the integrand is continuous on the compact interval, hence Lebesgue integrable by [F3] and [F4]. If $t_{k} \to t$ in $[0, T]$ , then $w (x, t_{k})^{2} \to w (x, t)^{2}$ for every $x$ by continuity of $w$ on $\overline{Q}$ , and [F10] bounds $w$ by some $M < \infty$ , so the constant $4 M^{2}$ dominates all integrands and [F11] gives $E (t_{k}) \to E (t)$ ; thus $E$ is continuous on $[0, T]$ .

1.2F1F10given

For fixed $t \in (0, T)$ the map $x \mapsto w (x, t)^{2}$ is integrable, for every $x$ the map $s \mapsto w (x, s)^{2}$ is differentiable on $(0, T)$ with derivative $2 w (x, s) w_{t} (x, s)$ , and [F10] bounds $w$ and $w_{t}$ by constants $M, M_{1} < \infty$ , so $∣ 2 w w_{t} ∣ \leq 2 M M_{1}$ everywhere; [F1] therefore applies and gives $E^{'} (t) = \frac{1}{2} \int_{0}^{π} 2 w (x, t) w_{t} (x, t) d x = \int_{0}^{π} w (x, t) w_{t} (x, t) d x$ for every $t \in (0, T)$ .

2.1step 1.2F2F3F4given

On $(0, T)$ the equation $w_{t} = w_{x x}$ turns step 1.2 into $E^{'} (t) = \int_{0}^{π} w w_{x x} d x$ ; the functions $x \mapsto w (x, t)$ and $x \mapsto w_{x} (x, t)$ are continuously differentiable on $[0, π]$ with continuous, hence integrable derivatives by [F3], so [F2] gives $\int_{0}^{π} w w_{x x} d x = [w w_{x}]_{0}^{π} - \int_{0}^{π} w_{x}^{2} d x = - \int_{0}^{π} w_{x} (x, t)^{2} d x$ , the boundary term vanishing because $w (0, t) = w (π, t) = 0$ for all $t$ ; the Riemann integrals equal the Lebesgue integrals by [F4], so $E^{'} (t) = - \int_{0}^{π} w_{x} (x, t)^{2} d x \leq 0$ .

2.2step 1.2F1F2F3F4F10given

Applying [F1] to $x \mapsto w_{x} (x, t)^{2}$ , with $w_{x}$ and $w_{x t}$ bounded on the compact rectangle by [F10], gives $E^{''} (t) = - 2 \int_{0}^{π} w_{x} (x, t) w_{x t} (x, t) d x$ for $t \in (0, T)$ ; [F2] applied to $u = w_{x} (\cdot, t)$ and $v = w_{t} (\cdot, t)$ gives $\int_{0}^{π} w_{x} w_{x t} = [w_{x} w_{t}]_{0}^{π} - \int_{0}^{π} w_{x x} w_{t} = - \int_{0}^{π} w_{x x} w_{t} d x$ , since $w_{t} (0, t) = w_{t} (π, t) = 0$ by differentiating the boundary identities in $t$ : the continuous extensions of $w_{t}$ are those derivatives, since the interior identity $w (x, b) - w (x, a) = \int_{a}^{b} w_{t} (x, s) d s$ passes to $x = 0, π$ by uniform continuity on $[a, b]$ ; substituting $w_{x x} = w_{t}$ yields $E^{''} (t) = 2 \int_{0}^{π} w_{t} (x, t)^{2} d x \geq 0$ .

3.1step 1.2step 2.2F5F6F7F9F12F13given

By [F5] and steps 1.2 and 2.2, $E^{'} (t)^{2} = (\int_{0}^{π} w w_{t})^{2} \leq (\int_{0}^{π} w^{2}) (\int_{0}^{π} w_{t}^{2}) = E (t) E^{''} (t)$ for $t \in (0, T)$ ; hence on every interval on which $E > 0$ , the function $L : = \log \circ E$ is twice differentiable with $L^{'} = E^{'} / E$ and $L^{''} = E^{''} / E - (E^{'} / E)^{2} \geq 0$ by [F9] and [F12], so $L$ is convex there by [F6] and [F7].

4.1step 1.1step 2.1step 3.1F7F8F13given

If $E$ were positive somewhere, continuity and $E (T) = 0$ would give $t_{0} \in (0, T)$ with $E (t_{0}) > 0$ . By step 2.1 and [F13], $E$ is nonincreasing; fix $s \in (0, t_{0})$ , so $E (s) > 0$ . The nonempty closed set ${t \in [t_{0}, T] : E (t) = 0}$ has a least element $b > t_{0}$ , with $E > 0$ on $[s, b)$ and $E (b) = 0$ . For $t_{0} < t < b$ , convexity from step 3.1 yields $L (t_{0}) \leq \frac{t - t_{0}}{t - s} L (s) + \frac{t_{0} - s}{t - s} L (t)$ . As $t ↑ b$ , $L (t) \to - \infty$ by continuity of $E$ and [F8], its coefficient tends to $(t_{0} - s) / (b - s) > 0$ , and the other term is bounded. This contradicts the finite $L (t_{0})$ . Hence $E \equiv 0$ on $[0, T]$ .

5.1step 4.1given∎

Since $E \equiv 0$ and $E (t) = \frac{1}{2} \int_{0}^{π} w (x, t)^{2} d x$ with a nonnegative continuous integrand, $w (x, t) = 0$ for every $x \in [0, π]$ and every $t \in [0, T]$ : if $w (x_{0}, t) \neq 0$ , continuity in $x$ gives $w^{2} > 0$ on a nondegenerate interval, making $E (t) > 0$ . Thus $w \equiv 0$ on $\overline{Q}$ ; if $u_{1}, u_{2}$ are two $C^{4, 2}$ solutions with the same terminal data and zero lateral data, their difference satisfies the hypotheses, so $u_{1} = u_{2}$ and the terminal-to-initial map on the terminal data of such solutions is well defined.

Depends on

Used by

Dependency tree · two levels

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