ExampleConstruction: Literature-sourcedVerification: 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.

Heat comparison preserves an interval of values

Example

Assume Countable Choice. Let $Q = Ω \times (0, T]$ be a parabolic cylinder with $Ω$ bounded, let $a \leq b$ be real constants, and let $u \in C^{2, 1} (\overline{Q})$ solve $u_{t} - Δ u = 0$ in $Q$ with $a \leq u \leq b$ on the parabolic boundary $\partial_{p} Q$ . Then $a \leq u \leq b$ on all of $\overline{Q}$ . On the whole space the analogous statement is that $a \leq u_{0} \leq b$ almost everywhere implies $a \leq H_{t} u_{0} \leq b$ almost everywhere for every $t > 0$ .

Facts & Assumptions

Given: Countable Choice, a bounded parabolic cylinder $Q = Ω \times (0, T]$ , constants $a \leq b$ , a solution $u \in C^{2, 1} (\overline{Q})$ with $a \leq u \leq b$ on $\partial_{p} Q$ , and, for the whole-space clause, $t > 0$ and $u_{0} \in L^{p} (R^{n})$ with $a \leq u_{0} \leq b$ almost everywhere.

[A1]

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

[F1]

Comparison: if $U, V \in C^{2, 1} (\overline{Q})$ with $U_{t} - Δ U \leq V_{t} - Δ V$ in $Q$ and $U \leq V$ on $\partial_{p} Q$ , then $U \leq V$ on $\overline{Q}$ (Comparison and uniqueness for the bounded-cylinder heat problem); the parabolic boundary is that of Parabolic cylinder and parabolic boundary, and a constant function has $c_{t} = 0 = Δ c$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[F2]

Heat evolution on $L^{p}$ : for $t > 0$ , $H_{t} f$ is the $L^{p}$ class of $x \mapsto \int_{R^{n}} Γ (x - y, t) f (y) d y$ , defined for almost every $x$ , and each $H_{t}$ is linear (The heat evolution $H_{t}$ of initial data); the kernel has unit mass $∥ Γ_{t} ∥_{1} = 1$ for every $t > 0$ (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

[F3]

Order preservation and positivity: if $f, g \in L^{p} (R^{n})$ satisfy $f \leq g$ almost everywhere, then $H_{t} f \leq H_{t} g$ almost everywhere for every $t > 0$ ; and if $f \geq 0$ almost everywhere then $H_{t} f \geq 0$ almost everywhere (Monotonicity and $L^{p}$ contractivity of the heat flow, Mass conservation and positivity of the heat flow).

[F4]

The Lebesgue integral is linear on $L^{1}$ and monotone for nonnegative functions: $\int (α f + β g) = α \int f + β \int g$ for $f, g \in L^{1}$ , and $f \leq g$ implies $\int f \leq \int g$ for measurable $f, g \geq 0$ (The Lebesgue integral is linear on $L^{1} (μ)$ , Monotonicity and nonnegative homogeneity of the nonnegative integral).

Verification

Given: Countable Choice, the bounded cylinder $Q$ , the constants $a \leq b$ , a solution $u \in C^{2, 1} (\overline{Q})$ with $a \leq u \leq b$ on $\partial_{p} Q$ , and the whole-space data $t > 0$ and $u_{0} \in L^{p} (R^{n})$ with $a \leq u_{0} \leq b$ almost everywhere.

1.1A1F1given

On the bounded cylinder, apply [F1] to the pair $(U, V) = (a, u)$ : both lie in $C^{2, 1} (\overline{Q})$ , $a_{t} - Δ a = 0 = u_{t} - Δ u$ in $Q$ by [F1], and $a \leq u$ on $\partial_{p} Q$ by hypothesis, so $a \leq u$ on $\overline{Q}$ ; applying [F1] to $(U, V) = (u, b)$ in the same way gives $u \leq b$ on $\overline{Q}$ . Hence $a \leq u \leq b$ on all of $\overline{Q}$ .

2.1step 1.1F2F3given

The analogous whole-space statement in the bounded-data case $u_{0} \in L^{\infty} (R^{n})$ : the constant functions $a$ and $b$ lie in $L^{\infty}$ , and $H_{t} a = a$ , $H_{t} b = b$ almost everywhere because the constant $c$ convolves to $c \int Γ (x - y, t) d y = c$ for almost every $x$ by the unit mass of [F2]; since $a \leq u_{0} \leq b$ almost everywhere, [F3] applied to the pairs $(a, u_{0})$ and $(u_{0}, b)$ gives $a = H_{t} a \leq H_{t} u_{0} \leq H_{t} b = b$ almost everywhere.

3.1step 2.1F2F3F4given∎

For general $u_{0} \in L^{p} (R^{n})$ , $1 \leq p \leq \infty$ , the same conclusion follows from the kernel representation: at every $x$ where the defining integral of [F2] converges, $b - H_{t} u_{0} (x) = \int_{R^{n}} Γ (x - y, t) (b - u_{0} (y)) d y$ by linearity of the integral [F4] and $b = \int_{R^{n}} Γ (x - y, t) b d y$ by the unit mass of [F2], while the integrand $Γ (x - y, t) (b - u_{0} (y))$ is nonnegative almost everywhere in $y$ ; its integral is therefore nonnegative by the monotonicity clause of [F4], so $H_{t} u_{0} (x) \leq b$ at each such $x$ , and $H_{t} u_{0} \leq b$ almost everywhere because the defining integral converges almost everywhere [F2]; the inequality $H_{t} u_{0} \geq a$ follows the same way from $u_{0} - a \geq 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Universitext, Springer 2011) (standard reference, not scraped)