Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck pass
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 heat kernel semigroup identity Γt∗Γs=Γt+s

Statement

Assume Countable Choice and let n≥1. For all s,t>0 the convolution Γ(⋅,t)∗Γ(⋅,s) converges absolutely at every x∈Rn and equals Γ(x,t+s); that is, Γt∗Γs=Γt+s as functions on Rn.

Facts & Assumptions

Given: Countable Choice, n≥1, s,t>0, and x∈Rn.

[A1]

Countable Choice is the hypothesis carried by the integration and change-of-variables suppliers below (The Axiom of Countable Choice (ACω)).

[F1]

For t>0 the heat kernel is Γ(y,t)=(4πt)−n/2exp⁡(−∣y∣2/(4t)), positive and integrable (The heat kernel on Rn and its causal extension); the convolution f∗g of Convolution of two functions on Rn is defined at x when y↦f(x−y)g(y) is measurable and integrable.

[F2]

For real u,v the exponential satisfies exp⁡(u)exp⁡(v)=exp⁡(u+v) (The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y)).

[F3]

∫−∞∞e−u2 du=π (The Gaussian integral ∫−∞∞e−x2 dx=π).

[F4]

Under Rm+n=Rm×Rn the Lebesgue measure λm+n is the completion of the product measure λm×λn (The Euclidean Lebesgue measure is the completion of the product of the factor Lebesgue measures).

[F5]

On completed sigma-finite product measure spaces, a nonnegative completed-product-measurable f has measurable sections outside measurable null sets. Set the inner integrals to zero on those exceptional sets; the resulting measurable functions have integrals equal to ∫f dμ×ν‾ (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability). For the continuous Euclidean Gaussian integrands used here, every section is measurable, so the ordinary iterated integrals give the same value.

[F6]

For a C1 diffeomorphism T:U→V of open sets and every nonnegative Lebesgue measurable f:V→[0,∞], ∫Vf(y) dy=∫Uf(T(x))∣det⁡DT(x)∣ dx (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions); a translation of Rn has ∣det⁡DT∣=1 (Integral invariance under measure-preserving maps).

[F7]

For every t>0 the kernel satisfies Γ(λz,λ2t)=λ−nΓ(z,t) for every λ>0 and z∈Rn (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

Proof

technique · direct
1.1A1F1F2F7given

Work under [A1] and fix s,t>0 and x∈Rn. By the product form [F1] and the addition formula [F2], the convolution integrand is Γ(x−y,t)Γ(y,s)=(4πt)−n/2(4πs)−n/2exp⁡(−∣x−y∣2/(4t)−∣y∣2/(4s)), a measurable function of y that is strictly positive everywhere.

1.2F3F4F5F6givenalgebra

Gaussian evaluation: for A>0, ∫Rne−A∣z∣2 dz=(π/A)n/2. Indeed, by the identification [F4] and Tonelli's theorem [F5] the integral factorises over the coordinates, each one-dimensional factor is ∫Re−Au2du=A−1/2π by the substitution u=A−1/2v of [F6] and the Gaussian integral [F3], and the product is (π/A)n/2.

2.1step 1.1givenalgebra

Completing the square in the exponent: with A:=(t+s)/(4ts) and b:=xs/(t+s), the algebraic identity −∣x−y∣2/(4t)−∣y∣2/(4s)=−A∣y−b∣2−∣x∣2/(4(t+s)) holds, since the quadratic terms give −A∣y∣2, the linear terms give 2Ab⋅y=x⋅y/(2t), and the constant term gives A∣b∣2−∣x∣2/(4t)=−∣x∣2/(4(t+s)).

3.1step 2.1step 1.2F1F6givenalgebra

Therefore the absolutely convergent (indeed nonnegative) integral defining the convolution equals (4πt)−n/2(4πs)−n/2e−∣x∣2/(4(t+s))∫Rne−A∣y−b∣2 dy, where the last integral is ∫Rne−A∣z∣2 dz=(π/A)n/2=(4πts/(t+s))n/2 by the translation case of [F6] and step 1.2; the prefactor simplifies to (4πt)−n/2(4πs)−n/2(4πts/(t+s))n/2=(4π(t+s))−n/2, so Γ(x−y,t)Γ(y,s) is integrable in y and Γt∗Γs(x)=(4π(t+s))−n/2e−∣x∣2/(4(t+s))=Γ(x,t+s) by [F1].

4.1F1step 3.1given∎

Steps 1.1, 2.1, 1.2 and 3.1 show that for every fixed x the convolution integral converges absolutely and equals Γ(x,t+s); as s,t>0 and x were arbitrary, Γt∗Γs=Γt+s as functions on Rn.

Depends on

Used by

Dependency tree · two levels

66 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