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.
Duhamel solution for a time-independent source
Example
Assume Countable Choice. Let , , and let be viewed as the time-independent source ; if is spatially Hölder continuous with compact support, read the classical statement below. The heat potential of The Duhamel heat potential is the substitution removing the time dependence. Then , , and in the classical compactly supported case on . In particular is the solution of the inhomogeneous Cauchy problem with zero initial data produced by the Duhamel principle, and for a time-independent source the two representations and agree.
Facts & Assumptions
Given: Countable Choice, , , , a fixed regarded as the constant curve on , and, for the classical clause, the same as a compactly supported spatially Hölder continuous function.
Countable Choice is the ambient hypothesis (The Axiom of Countable Choice ()).
Duhamel principle: the heat potential of a continuous -valued forcing lies in , satisfies and the forced semigroup relation; in the classical setting with bounded, jointly continuous and uniformly spatially Hölder the scalar potential is with , , and is the unique classical solution in every Gaussian growth class (Duhamel principle for the whole-space heat equation).
The heat potential is defined by the Bochner integral of the continuous curve (The Duhamel heat potential), and is the class of with the flow strongly continuous for (The heat evolution of initial data, The heat Cauchy problem for data).
The Bochner integral is defined by approximation with -valued simple functions (Bochner-integrable function), with convergence of the approximating integrals governed by the norm estimate and dominated convergence (Bochner dominated convergence theorem); for a finitely-valued curve the integral is the finite sum of the values times the Lebesgue measures of the corresponding level sets, and the substitution preserves those measures on because it is the reflection of the interval about its midpoint.
Verification
Given: Countable Choice, , a fixed read as the constant curve on , and the compactly supported Hölder case for the classical clause.
The constant curve belongs to , so [F1] applies to it: , , and satisfies the forced semigroup relation with the constant forcing.
The two representations agree. For each fixed the curves and are norm continuous by [F2], and they are related by the reflection of ; by [F3] both Bochner integrals are limits of the integrals of simple approximations, and for a finitely-valued approximation the substitution reduces to the equality of the Lebesgue measures of a measurable level set and its reflection, so passing to the limit gives .
Classical compactly supported case. If is spatially Hölder continuous with compact support, then as a function of it is bounded, jointly continuous and uniformly spatially Hölder on ; by [F1] the scalar potential is with and , and it represents the Bochner potential in the sense of [F2]; moreover , so lies in the Gaussian growth class and is the unique classical solution with zero initial data there. Hence on , the representation of step 2.1 shows that the two displayed formulas for coincide, and no commutation of the unbounded Laplacian with the flow on arbitrary data is asserted.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
41 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)