ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-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.

Heat evolution of affine and quadratic polynomials

Example

Assume Countable Choice, let $n \geq 1$ and $t > 0$ . For a polynomial $P : R^{n} \to R$ define the Gaussian moment integral $H_{t} P (x) : = \int_{R^{n}} Γ (x - y, t) P (y) d y, x \in R^{n},$ whenever this integral converges absolutely. For the polynomials $1$ , $y_{i}$ , $y_{i} y_{j}$ and $∣ y ∣^{2}$ it converges absolutely for every $x$ , and $H_{t} 1 = 1, H_{t} y_{i} = x_{i}, H_{t} (y_{i} y_{j}) = x_{i} x_{j} + 2 t δ_{i j}, H_{t} ∣ y ∣^{2} = ∣ x ∣^{2} + 2 n t .$ These integrals extend the convolution formula to these polynomial data; nonconstant polynomial data are not asserted to lie in $L^{p}$ or to be bounded.

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $t > 0$ , $x \in R^{n}$ and coordinate indices $0 \leq i, j < n$ .

[A1]

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

[F1]

The heat kernel is $Γ (z, t) = (4 π t)^{- n / 2} e^{- ∣ z ∣^{2} / (4 t)}$ with $\int_{R^{n}} Γ (z, t) d z = 1$ (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

[F2]

All first and second moments of the kernel are absolutely integrable and $\int z_{i} Γ (z, t) d z = 0$ , $\int z_{i} z_{j} Γ (z, t) d z = 2 t δ_{i j}$ , $\int ∣ z ∣^{2} Γ (z, t) d z = 2 n t$ (First and second Gaussian heat-kernel moments).

[F3]

Translations preserve Lebesgue measurability and measure (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation), as does reflection $z \mapsto - z$ , whose linear matrix has $∣ \det (- I) ∣ = 1$ (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not). Thus $T_{x} (z) = x - z$ is a measurable measure-preserving involution. For nonnegative measurable $q$ , allowing infinity, and for integrable real $q$ , $\int q \circ T_{x} = \int q$ (Integral invariance under measure-preserving maps).

Verification

technique · direct

1.1A1F1F2F3givenalgebra

Absolute convergence: put $q (z) = Γ (z, t) P (x - z)$ . For $P \equiv 1$ the integrand is $Γ (z, t)$ , integrable with integral $1$ by [F1]; for $P (y) = y_{i}$ the substituted integrand is $x_{i} Γ (z, t) - z_{i} Γ (z, t)$ , a sum of integrable terms by [F1] and the first-moment clause of [F2]; for $P (y) = y_{i} y_{j}$ it is the finite expansion $x_{i} x_{j} Γ - x_{i} z_{j} Γ - x_{j} z_{i} Γ + z_{i} z_{j} Γ$ , integrable by [F1] and the second-moment clause of [F2]; and for $P (y) = ∣ y ∣^{2}$ it is $∣ x ∣^{2} Γ - 2 \sum_{i} x_{i} z_{i} Γ + ∣ z ∣^{2} Γ$ , integrable by the same clauses. Thus $q \in L^{1}$ in all four cases; applying [F3] to $∣ q ∣$ and $q$ shows that $q (x - y) = Γ (x - y, t) P (y)$ is absolutely integrable and $H_{t} P (x) = \int q (z) d z$ .

2.1step 1.1F1F2givenalgebra

Constant and affine data: by [F1], $H_{t} 1 (x) = \int Γ (z, t) d z = 1$ ; by [F1] and the vanishing first moments of [F2], $H_{t} y_{i} (x) = \int Γ (z, t) (x_{i} - z_{i}) d z = x_{i} \int Γ (z, t) d z - \int z_{i} Γ (z, t) d z = x_{i}$ .

3.1step 1.1step 2.1F1F2givenalgebra

Quadratic data: expanding as in step 1.1 and using [F1] and the covariance clause of [F2], $H_{t} (y_{i} y_{j}) (x) = x_{i} x_{j} \int Γ - x_{i} \int z_{j} Γ - x_{j} \int z_{i} Γ + \int z_{i} z_{j} Γ = x_{i} x_{j} + 2 t δ_{i j}$ , and, summing the diagonal identities, $H_{t} ∣ y ∣^{2} (x) = ∣ x ∣^{2} \int Γ - 2 \sum_{i} x_{i} \int z_{i} Γ + \int ∣ z ∣^{2} Γ = ∣ x ∣^{2} + 2 n t$ .

4.1step 1.1step 2.1step 3.1given∎

Steps 1.1, 2.1 and 3.1 show that all four moment integrals converge absolutely for every $x$ and have the stated values, which is the example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)
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)