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.

Strict-subsolution perturbation for the heat operator

Statement

Let $Q = Ω \times (0, T]$ be a parabolic cylinder (Parabolic cylinder and parabolic boundary) with $Ω$ bounded, and let $u \in C^{2, 1} (\overline{Q})$ satisfy $u_{t} - Δ u \leq 0$ in $Q$ . Then:

(i) for every $ε > 0$ the function $v : = u + ε ∣ x ∣^{2}$ is in $C^{2, 1} (\overline{Q})$ and satisfies $v_{t} - Δ v \leq - 2 n ε < 0 in Q;$

(ii) if $w \in C^{2, 1} (\overline{Q})$ satisfies $w_{t} - Δ w < 0$ in $Q$ , then $\max_{\overline{Q}} w = \max_{\partial_{p} Q} w$ .

Facts & Assumptions

Given: A parabolic cylinder $Q = Ω \times (0, T]$ with $Ω$ bounded, $u \in C^{2, 1} (\overline{Q})$ with $u_{t} - Δ u \leq 0$ in $Q$ , and $w \in C^{2, 1} (\overline{Q})$ with $w_{t} - Δ w < 0$ in $Q$ .

[F1]

On the open cylinder, $C^{2, 1} (\overline{Q})$ means continuous on $\overline{Q}$ with $C^{2}$ spatial and $C^{1}$ time derivatives on $Q$ extending continuously, and $\overline{Q}$ is compact while $\partial_{p} Q$ is closed (Parabolic cylinder and parabolic boundary).

[F2]

$Δ = \sum_{i} \partial_{i} \partial_{i}$ and the partial derivatives are those of Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F3]

The chain and product rules give $\partial_{i} ∣ x ∣^{2} = 2 x_{i}$ and $\partial_{i} \partial_{i} ∣ x ∣^{2} = 2$ (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$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F4]

At an interior local maximum of a $C^{2}$ function the Hessian is negative semidefinite, so the Laplacian is $\leq 0$ (The Hessian is negative semidefinite at an interior local maximum).

[F5]

At an interior local extremum of a differentiable one-variable function the derivative vanishes (Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ ), and the mean value theorem identifies a difference quotient with a derivative at an interior point (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F6]

A continuous real function on the nonempty compact set $\overline{Q}$ attains its maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, 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).

Proof

Given: A bounded parabolic cylinder $Q$ , $u \in C^{2, 1} (\overline{Q})$ with $u_{t} - Δ u \leq 0$ in $Q$ , and $w \in C^{2, 1} (\overline{Q})$ with $w_{t} - Δ w < 0$ in $Q$ .

1.1F2F3given

For $∣ x ∣^{2} = ⟨ x, x ⟩$ the chain rule and product rule give $\partial_{i} ∣ x ∣^{2} = 2 x_{i}$ and hence $\partial_{i} \partial_{i} ∣ x ∣^{2} = 2$ by [F3], so [F2] gives $Δ ∣ x ∣^{2} = \sum_{i} 2 = 2 n$ ; therefore for $v = u + ε ∣ x ∣^{2}$ one has $v_{t} = u_{t}$ and $Δ v = Δ u + 2 n ε$ , hence $v_{t} - Δ v = (u_{t} - Δ u) - 2 n ε \leq - 2 n ε < 0$ on $Q$ .

1.2F1F4F6given

By [F6] the function $w$ attains its maximum on $\overline{Q}$ ; suppose it is attained at a point $P = (x_{0}, t_{0}) \notin \partial_{p} Q$ . Then $t_{0} \neq 0$ and $x_{0} \notin \partial Ω$ by the definition of $\partial_{p} Q$ , so $x_{0}$ is an interior point of $Ω$ and $0 < t_{0} \leq T$ ; since $x_{0}$ is an unconstrained local maximum of the spatial function $x \mapsto w (x, t_{0})$ , [F4] gives $Δ w (P) \leq 0$ .

2.1step 1.2F5given

If $t_{0} < T$ , then $t_{0}$ is an interior point of $(0, T)$ at which the one-variable function $t \mapsto w (x_{0}, t)$ has a local maximum, so [F5] gives $w_{t} (P) = 0$ ; with step 1.2 this yields $(w_{t} - Δ w) (P) \geq 0 - 0 = 0$ , contradicting $w_{t} - Δ w < 0$ in $Q$ .

2.2step 1.2F1F5given

If $t_{0} = T$ , then for every $0 < h < T$ the difference quotient $(w (x_{0}, T) - w (x_{0}, T - h)) / h$ is $\geq 0$ because $T$ maximises $t \mapsto w (x_{0}, t)$ ; [F5] gives an interior point $c_{h} \in (T - h, T)$ with $w_{t} (x_{0}, c_{h})$ equal to that quotient, and continuity of $w_{t}$ up to the top face (the class of [F1]) gives $w_{t} (x_{0}, T) = \lim_{h ↓ 0} w_{t} (x_{0}, c_{h}) \geq 0$ ; with $Δ w (x_{0}, T) \leq 0$ from step 1.2 this again contradicts $w_{t} - Δ w < 0$ .

3.1step 1.1step 2.1step 2.2given∎

Steps 1.1, 2.1 and 2.2 show (i) and that the maximum of any strict subsolution $w$ is attained on $\partial_{p} Q$ , which is (ii).

Depends on

Used by

Weak parabolic maximum principle Theorem

Dependency tree · two levels

86 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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Universitext, Springer 2011) (standard reference, not scraped)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)