Alphabeta Math
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.

Lp to Lq smoothing estimate for the heat flow

Statement

Assume Countable Choice, let n≥1 and 1≤p≤q≤∞, and let Q∈[1,∞] be determined by 1Q=1+1q−1p. Then for every f∈Lp(Rn) and every t>0, ∥Htf∥q≤Cn,p,q t−n2(1p−1q)∥f∥p,Cn,p,q:=(4π)−n2(1p−1q)Q−n2Q, with the endpoint Q=∞ (which occurs exactly at p=1, q=∞) read as Q−n/(2Q)→1; for p=q the constant is 1 and the estimate is the contraction clause.

Facts & Assumptions

Given: Countable Choice, n≥1, 1≤p≤q≤∞, the exponent Q with 1/Q=1+1/q−1/p, f∈Lp(Rn) and t>0.

[A1]

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

[F1]

For 1≤p≤∞ and f∈Lp(Rn), Htf is the Lp class of the convolution Γt∗f (The heat evolution Ht of initial data).

[F2]

For every s>0 the kernel satisfies Γ(x,s)=(4πs)−n/2e−∣x∣2/(4s), the scaling identity Γ(λx,λ2s)=λ−nΓ(x,s), and unit mass ∫RnΓ(x,s) dx=1 (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

[F3]

Assume Countable Choice; if 1≤p,q,r≤∞ satisfy 1/r=1/p+1/q−1 and f∈Lp, g∈Lq, then ∥f∗g∥r≤∥f∥p∥g∥q (Young's convolution inequality under Countable Choice).

Proof

technique · direct
1.1A1F1F3given

Young estimate: the triple (p,Q,q) is admissible because 1/Q=1+1/q−1/p means exactly 1/q=1/p+1/Q−1, and Q∈[1,∞] lies in the Young range since 0≤1/p−1/q≤1; hence, by [F3] applied to f and Γt∈LQ, ∥Htf∥q≤∥Γt∥Q∥f∥p for every t>0.

2.1step 1.1F2givenalgebra

Scaling of the kernel norm: the scaling identity of [F2] with λ=t gives Γt(x)=t−n/2Γ1(x/t), so the substitution x=t z yields ∥Γt∥Q=t−n/2tn/(2Q)∥Γ1∥Q=t−n2(1−1Q)∥Γ1∥Q for Q<∞, and for Q=∞ the same substitution gives ∥Γt∥∞=t−n/2∥Γ1∥∞.

3.1step 2.1F2givenalgebra

Gaussian norm: by [F2] with s=1, Γ1(x)=(4π)−n/2e−∣x∣2/4, and for Q<∞ the identity e−Q∣x∣2/4=(4π/Q)n/2Γ(x,1/Q) holds by the explicit formula, so unit mass gives ∥Γ1∥Q=(4π)−n/2(∫e−Q∣x∣2/4dx)1/Q=(4π)−n/2(4π/Q)n/(2Q); for Q=∞ the same formula is read as ∥Γ1∥∞=(4π)−n/2.

4.1step 1.1step 2.1step 3.1givenalgebra

Assembling the estimate: since 1−1Q=1p−1q by the definition of Q, steps 1.1, 2.1 and 3.1 give ∥Htf∥q≤t−n2(1p−1q)(4π)−n/2(4π/Q)n/(2Q)∥f∥p, and (4π)−n/2(4π/Q)n/(2Q)=(4π)−n2(1−1Q)Q−n/(2Q)=(4π)−n2(1p−1q)Q−n/(2Q)=Cn,p,q, which is the displayed estimate.

5.1step 4.1givenalgebra

Endpoints: if p=q then 1/Q=1 and Q=1, so Cn,p,q=1 and the estimate reads ∥Htf∥p≤∥f∥p; if Q=∞ then 1/p−1/q=1, which forces p=1 and q=∞, and the factor Q−n/(2Q) tends to 1 while the exponent is t−n/2, so the estimate reads ∥Htf∥∞≤(4πt)−n/2∥f∥1.

6.1step 4.1step 5.1given∎

Steps 1.1, 2.1, 3.1, 4.1 and 5.1 prove the displayed Lp to Lq estimate with the stated constant, including the endpoint conventions and the p=q contraction case.

Depends on

Used by

Dependency tree · two levels

38 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