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

Duhamel solution for a time-independent source

Example

Assume Countable Choice. Let n≥1, 1≤p<∞, T>0 and let f∈Lp(Rn) be viewed as the time-independent source f(x,t):=f(x); if f is spatially Hölder continuous with compact support, read the classical statement below. The heat potential of The Duhamel heat potential is Df(t)=∫0tHt−sf ds=∫0tHτf dτ, the substitution τ=t−s removing the time dependence. Then Df∈C([0,T];Lp(Rn)), Df(0)=0, and in the classical compactly supported case (Df)t−ΔDf=f on Rn×(0,T]. In particular Df 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 ∫0tHt−sf ds and ∫0tHτf dτ agree.

Facts & Assumptions

Given: Countable Choice, n≥1, 1≤p<∞, T>0, a fixed f∈Lp(Rn) regarded as the constant curve s↦f on [0,T], and, for the classical clause, the same f as a compactly supported spatially Hölder continuous function.

[A1]

Countable Choice is the ambient hypothesis (The Axiom of Countable Choice (ACω)).

[F1]

Duhamel principle: the heat potential Df(t)=∫0tHt−sf(s) ds of a continuous Lp-valued forcing lies in C([0,T];Lp), satisfies Df(0)=0 and the forced semigroup relation; in the classical setting with f bounded, jointly continuous and uniformly spatially Hölder the scalar potential u(t,x)=∫0t∫Γ(x−y,t−s)f(y,s) dy ds is C1,2 with ut−Δu=f, u(0,⋅)=0, and is the unique classical solution in every Gaussian growth class (Duhamel principle for the whole-space heat equation).

[F2]

The heat potential is defined by the Bochner integral Df(t)=∫0tHt−sf(s) ds of the continuous curve s↦Ht−sf(s) (The Duhamel heat potential), and Hσg is the Lp class of Γ(⋅,σ)∗g with the flow strongly continuous for 1≤p<∞ (The heat evolution Ht of initial data, The heat Cauchy problem for Lp data).

[F3]

The Bochner integral is defined by approximation with X-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 s↦t−s preserves those measures on [0,t] because it is the reflection of the interval about its midpoint.

Verification

Given: Countable Choice, 1≤p<∞, a fixed f∈Lp(Rn) read as the constant curve on [0,T], and the compactly supported Hölder case for the classical clause.

1.1A1F1F2given

The constant curve s↦f belongs to C([0,T];Lp(Rn)), so [F1] applies to it: Df∈C([0,T];Lp(Rn)), Df(0)=0, and Df satisfies the forced semigroup relation with the constant forcing.

2.1step 1.1F2F3given

The two representations agree. For each fixed t the curves s↦Ht−sf and τ↦Hτf are norm continuous by [F2], and they are related by the reflection s↦t−s of [0,t]; 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 ∫0tHt−sf ds=∫0tHτf dτ.

3.1step 2.1F1F2given∎

Classical compactly supported case. If f is spatially Hölder continuous with compact support, then as a function of (x,t) it is bounded, jointly continuous and uniformly spatially Hölder on Rn×[0,T]; by [F1] the scalar potential u(t,x)=∫0t∫Γ(x−y,t−s)f(y) dy ds is C1,2 with ut−Δu=f and u(0,⋅)=0, and it represents the Bochner potential Df in the sense of [F2]; moreover ∣u∣≤T∥f∥∞, so u lies in the Gaussian growth class and is the unique classical solution with zero initial data there. Hence (Df)t−ΔDf=f on Rn×(0,T], the representation of step 2.1 shows that the two displayed formulas for Df coincide, and no commutation of the unbounded Laplacian with the flow on arbitrary Lp 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