TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge 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.

The causal heat kernel is the fundamental solution of the heat operator

Statement

Assume Countable Choice and let $n \geq 1$ , and let $Γ$ be the causal extension of the heat kernel. Then $Γ \in L_{l o c}^{1} (R^{n + 1})$ , and its regular distribution $u_{Γ} \in D^{'} (R^{n + 1})$ satisfies $(\partial_{t} - Δ) u_{Γ} = δ_{(0, 0)}$ , that is, $⟨ (\partial_{t} - Δ) u_{Γ}, φ ⟩ = φ (0, 0) for every φ \in C_{c}^{\infty} (R^{n + 1}),$ so the causal extension is a fundamental solution of $\partial_{t} - Δ$ . Moreover $Γ (\cdot, t) \to δ_{0}$ in $D^{'} (R^{n})$ as $t ↓ 0^{+}$ , that is, $\int_{R^{n}} Γ (x, t) φ (x) d x \to φ (0)$ for every $φ \in C_{c}^{\infty} (R^{n})$ . The derivative $\partial_{t}$ is the distributional derivative in the last space-time coordinate.

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , a test function $φ \in C_{c}^{\infty} (R^{n + 1})$ , a real $R > 0$ with $supp φ$ contained in the open box $B_{R} \times (- R, R) \subseteq R^{n + 1}$ , and $0 < ε < R$ .

[A1]

Countable Choice is the hypothesis carried by the integration and embedding suppliers below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The causal extension of the heat kernel is $Γ (x, t)$ for $t > 0$ and $Γ (x, t) = 0$ for $t \leq 0$ , with $Γ (x, t) = (4 π t)^{- n / 2} \exp (- ∣ x ∣^{2} / (4 t))$ positive and $C^{\infty}$ on $R^{n} \times (0, \infty)$ (The heat kernel on $R^{n}$ and its causal extension).

[F2]

For every $t > 0$ , $\int_{R^{n}} Γ (x, t) d x = 1$ , $\partial_{t} Γ = Δ_{x} Γ$ on $R^{n} \times (0, \infty)$ , and $(Γ (\cdot, t))_{t > 0}$ is an $L^{1}$ approximate identity on $R^{n}$ (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

[F3]

For $f \in L_{l o c}^{1} (Ω)$ the regular functional $⟨ u_{f}, φ ⟩ = \int_{Ω} f φ$ is well-defined and depends only on the almost-everywhere class of $f$ (Regular distribution from a locally integrable function).

[F4]

The distributional derivative is $⟨ \partial^{α} u, φ ⟩ = (- 1)^{∣ α ∣} ⟨ u, \partial^{α} φ ⟩$ (Distributional derivative); thus a first time derivative contributes a sign $- 1$ and a second spatial derivative a sign $+ 1$ .

[F5]

Assuming Countable Choice, $f \mapsto u_{f}$ is an injection from $L_{l o c}^{1} (Ω)$ modulo almost-everywhere equality into $D^{'} (Ω)$ , and local $L^{1}$ convergence implies strong distribution convergence (Locally integrable functions embed in distributions).

[F6]

The Dirac distribution satisfies $δ_{a} (φ) = φ (a)$ and $⟨ \partial^{α} δ_{a}, φ ⟩ = (- 1)^{∣ α ∣} \partial^{α} φ (a)$ (Dirac delta and its derivatives).

[F7]

If $F, G$ are continuous on $[a, b]$ and differentiable on $(a, b)$ with $F^{'} = f$ , $G^{'} = g$ Riemann integrable there, then $\int_{a}^{b} F g + \int_{a}^{b} f G = F (b) G (b) - F (a) G (a)$ (Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives).

[F8]

On completed sigma-finite product measure spaces, Tonelli's theorem holds for nonnegative measurable functions and Fubini's theorem for $L^{1}$ functions (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability); under $R^{m + n} = R^{m} \times R^{n}$ , $λ_{m + n}$ is that completed product measure (The Euclidean Lebesgue measure is the completion of the product of the factor Lebesgue measures).

[F9]

If $(K_{ε})$ is an $L^{1}$ approximate identity and $f$ is bounded and continuous, then $(f * K_{ε}) (x) \to f (x)$ uniformly for $x$ in every compact set ( $L^{1}$ approximate identities converge uniformly on compacta for bounded continuous functions).

[F10]

For continuous $f$ on $[a, b]$ , differentiable on $(a, b)$ , there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ (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)$ ).

Proof

technique · direct

1.1A1F1F2F3F5F8given

Local integrability: let $K \subseteq R^{n + 1}$ be compact and choose $R > 0$ with $K \subseteq B_{R} \times [- R, R]$ . By Tonelli's theorem [F8] over the completed product measure, $\int_{K} ∣ Γ ∣ \leq \int_{0}^{R} \int_{R^{n}} Γ (x, t) d x d t = \int_{0}^{R} 1 d t = R < \infty$ using unit mass from [F2] and $Γ = 0$ for $t \leq 0$ from [F1]; hence $Γ \in L_{l o c}^{1} (R^{n + 1})$ and its regular functional $u_{Γ}$ of [F3] is a distribution by [F5].

1.2F1F2F6F9givenalgebra

Dirac limit at time zero: fix a spatial test function $ψ \in C_{c}^{\infty} (R^{n})$ . For every $t > 0$ , $\int_{R^{n}} Γ (x, t) ψ (x) d x = (ψ * Γ_{t}) (0)$ because $Γ$ is spatially even, and by [F9] applied on a compact set containing $0$ and $supp ψ$ this converges to $ψ (0)$ as $t ↓ 0^{+}$ , so $Γ (\cdot, t) \to δ_{0}$ in $D^{'} (R^{n})$ by the definition of $δ_{0}$ in [F6].

2.1step 1.1F3F4given

Pairing: fix $φ$ with support in $B_{R} \times (- R, R)$ . The definitions of the regular functional and of the distributional derivative give $⟨ (\partial_{t} - Δ_{x}) u_{Γ}, φ ⟩ = - \int_{R^{n + 1}} Γ \partial_{t} φ - \int_{R^{n + 1}} Γ Δ_{x} φ = - \int_{R^{n + 1}} Γ (\partial_{t} φ + Δ_{x} φ)$ , the two integrals being absolutely convergent by step 1.1 and the compact support of $φ$ , with the signs as in [F4].

2.2step 1.1F1F2F7F8given

Truncated integration by parts: for $0 < ε < R$ , choose $T > R$ with $supp φ \subseteq R^{n} \times (- T, T)$ . Fubini [F8] on the strip $ε \leq t \leq T$ , the scalar integration by parts [F7] in the time variable at each fixed $x$ , and [F7] twice in each spatial coordinate at each fixed $t$ (the boundary terms vanish because $φ$ and all its derivatives are supported in the open box $B_{R} \times (- R, R)$ ) give $\int_{ε}^{\infty} \int_{R^{n}} Γ \partial_{t} φ d x d t = - \int_{R^{n}} Γ (x, ε) φ (x, ε) d x - \int_{ε}^{\infty} \int_{R^{n}} \partial_{t} Γ φ d x d t$ and $\int_{ε}^{\infty} \int_{R^{n}} Γ Δ_{x} φ d x d t = \int_{ε}^{\infty} \int_{R^{n}} Δ_{x} Γ φ d x d t$ ; adding the two identities and substituting the heat equation $\partial_{t} Γ = Δ_{x} Γ$ of [F2] cancels the interior terms and yields $\int_{ε}^{\infty} \int_{R^{n}} Γ (\partial_{t} φ + Δ_{x} φ) d x d t = - \int_{R^{n}} Γ (x, ε) φ (x, ε) d x$ .

3.1step 2.1step 2.2F1F2F9F10givenalgebra

Limit as $ε ↓ 0$ : by step 2.2 and step 2.1, $⟨ (\partial_{t} - Δ_{x}) u_{Γ}, φ ⟩ = \lim_{ε ↓ 0} \int_{R^{n}} Γ (x, ε) φ (x, ε) d x$ . Write the last integral as $\int_{R^{n}} Γ (x, ε) φ (x, 0) d x + \int_{R^{n}} Γ (x, ε) (φ (x, ε) - φ (x, 0)) d x$ . The first term equals $(φ (\cdot, 0) * Γ_{ε}) (0)$ because $Γ$ is even in its spatial variable, and it tends to $φ (0, 0)$ by the approximate-identity corollary [F9] applied to the bounded continuous compactly supported function $x \mapsto φ (x, 0)$ on a compact set containing $0$ ; the second term is bounded in modulus by $\sup_{x} ∣ φ (x, ε) - φ (x, 0) ∣ \cdot ∥ Γ (\cdot, ε) ∥_{1} \leq ε \sup ∣ \partial_{t} φ ∣$ by the mean value theorem [F10] in the time variable and unit mass from [F2], hence tends to $0$ .

4.1step 1.1step 3.1step 1.2F6given∎

Step 3.1 gives $⟨ (\partial_{t} - Δ_{x}) u_{Γ}, φ ⟩ = φ (0, 0) = ⟨ δ_{(0, 0)}, φ ⟩$ for every $φ \in C_{c}^{\infty} (R^{n + 1})$ by [F6], that is, $(\partial_{t} - Δ_{x}) u_{Γ} = δ_{(0, 0)}$ ; step 1.2 gives the weak Dirac limit at time zero; step 1.1 gives local integrability, so the causal extension is a fundamental solution of $\partial_{t} - Δ_{x}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

68 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

Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #5: The Fundamental Solution for the Heat Equation (Fall 2011) (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)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)