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.

Energy identity for the forced Dirichlet heat equation

Statement

Assume Countable Choice. Let $n \geq 2$ and let $Ω \subset R^{n}$ be a bounded $C^{1}$ domain in the class of the first Green identity (Bounded C1 domains and their outward normals), let $T > 0$ , and let real $u \in C^{2, 1} (\overline{Ω} \times [0, T])$ solve $u_{t} - Δ u = f$ in $Ω \times (0, T]$ with $f \in C (\overline{Ω} \times [0, T])$ and $u = 0$ on the lateral boundary $\partial Ω \times [0, T]$ . Then for $0 < t < T$ , $\frac{1}{2} \frac{d}{d t} \int_{Ω} u (x, t)^{2} d x + \int_{Ω} ∣ D u (x, t) ∣^{2} d x = \int_{Ω} f (x, t) u (x, t) d x,$ and integrating in $t$ gives the energy balance $\frac{1}{2} \int_{Ω} u (x, t_{2})^{2} d x - \frac{1}{2} \int_{Ω} u (x, t_{1})^{2} d x + \int_{t_{1}}^{t_{2}} ⁣ \int_{Ω} ∣ D u ∣^{2} d x d t = \int_{t_{1}}^{t_{2}} ⁣ \int_{Ω} f u d x d t$ for $0 < t_{1} < t_{2} < T$ . The identity carries exactly the Countable Choice assumption of the Green identity supplier.

Facts & Assumptions

Given: Countable Choice, $n \geq 2$ , a bounded $C^{1}$ domain $Ω$ , $T > 0$ , $u \in C^{2, 1} (\overline{Ω} \times [0, T])$ with $u_{t} - Δ u = f$ in $Ω \times (0, T]$ , $f$ continuous, and $u = 0$ on $\partial Ω \times [0, T]$ .

[A1]

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

[F1]

Differentiation under the integral sign: under the domination and measurability hypotheses of the theorem, $F (t) = \int f (x, t) d μ (x)$ is differentiable with $F^{'} = \int \partial_{t} f d μ$ (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 $G$ is differentiable on $[a, b]$ with integrable derivative $G^{'}$ , then $\int_{a}^{b} G^{'} = G (b) - G (a)$ (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)$ ).

[F4]

The closed cylinder $\overline{Ω} \times [0, T]$ is a closed and bounded subset of $R^{n + 1}$ , hence 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 every continuous real function on it is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F5]

The domain class, the outward normal $ν$ , the surface element $d S$ and the conventions $C^{1} (\overline{Ω})$ , $C^{2} (\overline{Ω})$ are those of Bounded C1 domains and their outward normals.

Proof

Given: Countable Choice, $n \geq 2$ , a bounded $C^{1}$ domain $Ω$ in the Green-identity class, $T > 0$ , real $u \in C^{2, 1} (\overline{Ω} \times [0, T])$ with $u_{t} - Δ u = f$ in $Ω \times (0, T]$ for continuous $f$ , and $u = 0$ on $\partial Ω \times [0, T]$ .

1.1A1F1F4given

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 by [F4], hence bounded there by constants $M, M_{1} < \infty$ ; the bounded domain has finite measure since 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); therefore $x \mapsto u (x, t)^{2}$ is integrable on $Ω$ for every $t$ , the derivative $\partial_{t} u (x, t)^{2} = 2 u (x, t) u_{t} (x, t)$ is bounded by $2 M M_{1}$ , and [F1] applies with the constant majorant, giving that $E$ is differentiable on $(0, T)$ with $E^{'} (t) = \frac{1}{2} \int_{Ω} 2 u (x, t) u_{t} (x, t) d x = \int_{Ω} u (x, t) u_{t} (x, t) d x$ .

2.1step 1.1F2F5given

Substituting the equation $u_{t} = Δ u + f$ from the hypothesis into step 1.1 gives $E^{'} (t) = \int_{Ω} u Δ u d x + \int_{Ω} f 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 $\int_{Ω} u Δ u d x = - \int_{Ω} ∣ D u (x, t) ∣^{2} d x$ ; hence $\frac{1}{2} \frac{d}{d t} \int_{Ω} u^{2} + \int_{Ω} ∣ D u ∣^{2} = \int_{Ω} f u$ for every $t \in (0, T)$ .

3.1step 2.1F3F4given∎

The three functions of $t$ in the identity of step 2.1 are continuous on $(0, T)$ : $E^{'}$ is given there by the integral of the continuous function $u Δ u + f u$ , while $t \mapsto \int_{Ω} ∣ D u ∣^{2} d x$ and $t \mapsto \int_{Ω} f u d x$ are integrals of continuous functions on the compact cylinder [F4], and dominated convergence (Dominated convergence) with these uniform bounds proves their continuity; integrating the identity from $t_{1}$ to $t_{2}$ and applying [F3] to the energy term yields the balance $\frac{1}{2} \int_{Ω} u (x, t_{2})^{2} d x - \frac{1}{2} \int_{Ω} u (x, t_{1})^{2} d x + \int_{t_{1}}^{t_{2}} \int_{Ω} ∣ D u ∣^{2} d x d t = \int_{t_{1}}^{t_{2}} \int_{Ω} f u d x d t$ for $0 < t_{1} < t_{2} < T$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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