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.

Submean inequality for heat subsolutions on heat balls

Statement

Assume Countable Choice. Let $u$ be of class $C^{2, 1}$ on a neighbourhood of the closed heat ball $E_{r} (t, x)$ of Heat balls and their time slices and suppose $u_{t} - Δ u \leq 0$ there. Then $u (x, t) \leq \frac{1}{2 r^{n}} \int_{t - r^{2} / 4 π}^{t} \frac{ρ_{n} (t - s)}{t - s} \int_{∣ y - x ∣ = ρ_{n} (t - s)} u (y, s) d S (y) d s .$ In particular, if $u \leq M$ on $E_{r} (t, x)$ then $u (x, t) \leq M$ .

Facts & Assumptions

Given: Countable Choice, a $C^{2, 1}$ function $u$ on a neighbourhood of the closed heat ball $E_{r} (t, x)$ with $u_{t} - Δ u \leq 0$ there.

[A1]

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

[F1]

On the heat ball below its top point, the defining inequality gives $Γ (x - y, t - s) - r^{- n} \geq 0$ ; the single top point is irrelevant to the volume integral. The slice radius is $ρ_{n} (τ) = \sqrt{2 n τ \log \frac{r^{2}}{4 π τ}} > 0$ for $0 < τ < r^{2} / (4 π)$ (Heat balls and their time slices).

[F2]

Representation formula: for $u$ of class $C^{2, 1}$ near $E_{r} (t, x)$ and $f = u_{t} - Δ u$ , $u (x, t) = \iint_{E} (Γ (x - y, t - s) - r^{- n}) f (y, s) d y d s + \frac{1}{2 r^{n}} \int_{t - r^{2} / 4 π}^{t} \frac{ρ_{n} (t - s)}{t - s} \int_{∣ y - x ∣ = ρ_{n} (t - s)} u (y, s) d S (y) d s,$ all integrals absolutely convergent (Heat-ball representation formula).

Proof

Given: Countable Choice, $u$ of class $C^{2, 1}$ near the closed heat ball $E_{r} (t, x)$ with $u_{t} - Δ u \leq 0$ there, and a constant $M$ with $u \leq M$ on $E_{r} (t, x)$ .

1.1A1F1F2given

Put $f : = u_{t} - Δ u$ ; by hypothesis $f \leq 0$ on $E_{r} (t, x)$ , while [F1] gives $Γ (x - y, t - s) - r^{- n} \geq 0$ there, so its integrand is nonpositive almost everywhere and the double integral in the representation formula of [F2] is $\leq 0$ .

2.1step 1.1F2given

Applying [F2] and discarding the nonpositive double integral by step 1.1 gives $u (x, t) \leq \frac{1}{2 r^{n}} \int_{t - r^{2} / 4 π}^{t} \frac{ρ_{n} (t - s)}{t - s} \int_{∣ y - x ∣ = ρ_{n} (t - s)} u (y, s) d S (y) d s$ , which is the submean inequality.

3.1step 2.1F1F2given∎

If in addition $u \leq M$ on $E_{r} (t, x)$ , then the averaging kernel $\frac{ρ_{n} (t - s)}{2 r^{n} (t - s)}$ is nonnegative by [F1] and the sphere integrals of the constant $M$ satisfy $\frac{1}{2 r^{n}} \int_{t - r^{2} / 4 π}^{t} \frac{ρ_{n} (t - s)}{t - s} \int_{∣ y - x ∣ = ρ_{n} (t - s)} M d S (y) d s = M$ , because the representation formula [F2] applied to the constant function $u \equiv M$ (whose forcing vanishes) reduces to that identity; hence step 2.1 gives $u (x, t) \leq M$ .

Depends on

Used by

Strong parabolic maximum principle Theorem

Dependency tree · two levels

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