TheoremStatement: 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.

Energy uniqueness for the homogeneous heat equation

Statement

Assume ${A C}_{ω}$ . Let $n \geq 2$ , let $Ω \subseteq R^{n}$ be a bounded $C^{1}$ domain (or belong to the specified finite piecewise $C^{1}$ class) of Bounded C1 domains and their outward normals, let $T > 0$ , and let $u \in C^{2, 1} (\overline{Q})$ solve $u_{t} - Δ u = 0$ in $Q = Ω \times (0, T]$ with $u = 0$ on $\partial Ω \times [0, T]$ and $u (\cdot, 0) = 0$ on $Ω$ . Then $u \equiv 0$ on $\overline{Q}$ ; equivalently, the Dirichlet problem for the homogeneous heat equation is unique in this class by the energy method. No backward-in-time or terminal-data uniqueness is claimed here (the time-reversed function solves the backward heat equation, for which the energy is nondecreasing rather than nonincreasing).

Facts & Assumptions

Given: ${A C}_{ω}$ , $n \geq 2$ , a bounded $C^{1}$ domain $Ω$ in the Green-identity class, $T > 0$ , and $u \in C^{2, 1} (\overline{Q})$ with $u_{t} - Δ u = 0$ in $Q$ , $u = 0$ on $\partial Ω \times [0, T]$ and $u (\cdot, 0) = 0$ on $Ω$ .

[A1]

Countable Choice is the ambient hypothesis, carried by the Green identity supplier (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Differentiation under the integral sign with an integrable majorant (Differentiation under the integral sign).

[F2]

Green's first identity: for real $u \in C^{2} (\overline{Ω})$ and $v \in C^{1} (\overline{Ω})$ , $\int_{Ω} (v Δ u + D u \cdot D v) d x = \int_{\partial Ω} v \partial_{ν} u d S$ (First Green identity).

[F3]

If a differentiable function has nonpositive derivative on an interval, it is nonincreasing there (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).

[F4]

$Δ u = \sum_{i} \partial_{i} \partial_{i} u$ in the notation of The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, and the domain class and boundary conventions are those of Bounded C1 domains and their outward normals.

[F5]

The closed cylinder $\overline{Ω} \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 continuous functions on it are bounded and attain their extrema (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F6]

Dominated convergence (Dominated convergence).

[F7]

Every bounded open set has finite measure because it lies in a bounded box (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included). A nonnegative continuous function $g$ with zero integral on an open set vanishes everywhere: if $g (x_{0}) > 0$ , a small nondegenerate box $B$ inside that set has $g \geq g (x_{0}) / 2$ on $B$ , so $\int g \geq (g (x_{0}) / 2) λ_{n} (B) > 0$ , a contradiction by the same box-volume formula.

Proof

Given: ${A C}_{ω}$ , a bounded $C^{1}$ domain $Ω \subset R^{n}$ with $n \geq 2$ , $T > 0$ , and $u \in C^{2, 1} (\overline{Q})$ with $u_{t} - Δ u = 0$ in $Q$ , $u = 0$ on $\partial Ω \times [0, T]$ , $u (\cdot, 0) = 0$ on $Ω$ .

1.1A1F1F5F6given

Define $E (t) : = \frac{1}{2} \int_{Ω} u (x, t)^{2} d x$ for $t \in [0, T]$ . The maps $u$ and $u_{t}$ are continuous on the compact cylinder [F5], hence bounded by constants $M, M_{1} < \infty$ , so [F1] applies with the constant majorant $2 M M_{1}$ and gives $E^{'} (t) = \int_{Ω} u (x, t) u_{t} (x, t) d x$ for every $t \in (0, T)$ ; moreover $E$ is continuous on $[0, T]$ , since for $t_{k} \to t$ the integrands $u (\cdot, t_{k})^{2}$ converge pointwise to $u (\cdot, t)^{2}$ (continuity of $u$ on $\overline{Q}$ ) and are dominated by $4 M^{2}$ , so [F6] gives $E (t_{k}) \to E (t)$ .

2.1step 1.1F2F3F4given

Substituting $u_{t} = Δ u$ into step 1.1 gives $E^{'} (t) = \int_{Ω} u Δ u d x$ ; [F2] with $v = u$ reads $\int_{Ω} (u Δ u + ∣ D u ∣^{2}) d x = \int_{\partial Ω} u \partial_{ν} u d S$ , and the boundary term vanishes because $u = 0$ on $\partial Ω \times [0, T]$ , so $E^{'} (t) = - \int_{Ω} ∣ D u (x, t) ∣^{2} d x \leq 0$ ; hence $E$ is nonincreasing on $(0, T)$ by [F3], and since $E (0) = \frac{1}{2} \int_{Ω} u (x, 0)^{2} d x = 0$ by the zero initial datum, continuity from step 1.1 gives $E (t) \leq 0$ and hence $E \equiv 0$ on $[0, T]$ because $E \geq 0$ .

3.1step 2.1F7given

For every $t$ , $E (t) = 0$ is the integral of the nonnegative continuous function $u (\cdot, t)^{2}$ , so [F7] gives $u (x, t) = 0$ for every $x \in Ω$ ; by continuity of $u$ on $\overline{Q}$ this gives $u \equiv 0$ on $\overline{Q}$ .

4.1step 3.1given∎

If $u_{1}, u_{2}$ are two solutions in this class with the same zero initial and lateral data, their difference $w : = u_{1} - u_{2}$ again satisfies $w_{t} - Δ w = 0$ in $Q$ , $w = 0$ on $\partial Ω \times [0, T]$ and $w (\cdot, 0) = 0$ on $Ω$ , so step 3.1 gives $w \equiv 0$ ; the Dirichlet problem for the homogeneous heat equation is therefore unique in this class. This is exactly the forward-in-time direction: the argument uses $u (\cdot, 0) = 0$ and deduces vanishing for larger times, and no terminal data or backward uniqueness is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

91 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)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Universitext, Springer 2011) (standard reference, not scraped)