TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Spatial analyticity of heat flow at positive time

Statement

Assume Countable Choice. Let $n \geq 1$ , $1 \leq p \leq \infty$ , $f \in L^{p} (R^{n})$ , and $t > 0$ . Then $H_{t} f$ is real analytic on $R^{n}$ (for complex data the real and imaginary parts are real analytic). For every $r > 0$ and multi-index $α$ , $∥ D^{α} H_{t} f ∥_{\infty} \leq α! r^{- ∣ α ∣} M_{n, p, t, r} ∥ f ∥_{p}$ , where $M_{n, p, t, r} = ∥ Γ (\cdot, t) \exp (r \sum_{i} ∣ x_{i} ∣ / (2 t) + n r^{2} / (4 t)) ∥_{p^{'}} < \infty$ , $1 / p + 1 / p^{'} = 1$ . The spatial Taylor series converges absolutely and equals $H_{t} f (x + h)$ for every real $h$ , uniformly for $h$ in each compact box. In particular taking $r = \sqrt{t}$ gives a factorial Gaussian derivative bound $C_{n, p} α! t^{- ∣ α ∣ / 2 - n / (2 p)} ∥ f ∥_{p}$ .

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $1 \leq p \leq \infty$ with conjugate $p^{'}$ , $f \in L^{p} (R^{n})$ , $t > 0$ , $r > 0$ , a centre $a \in R^{n}$ and a multi-index $α$ .

[A1]

Countable Choice is the hypothesis carried by the integration, differentiation and measure-theoretic suppliers below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The heat kernel is $Γ (w, t) = (4 π t)^{- n / 2} e^{- ∣ w ∣^{2} / (4 t)}$ , where $∣ w ∣^{2} = \sum_{i} w_{i}^{2}$ (The heat kernel on $R^{n}$ and its causal extension).

[F2]

The real exponential is $\exp (u) = \sum_{k \geq 0} u^{k} / k!$ , with the factorial of The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , and the series converges absolutely for every real $u$ (The real exponential function and the number $e$ by a power series, The exponential series converges absolutely for every real argument); for all real $u, v$ , $\exp (u) \exp (v) = \exp (u + v)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[F3]

The absolutely convergent representative $u (x, t) = \int_{R^{n}} Γ (x - y, t) f (y) d y$ is defined at every point and is $C^{\infty}$ in $x$ for $t > 0$ , with $D^{α} u (\cdot, t) = (D^{α} Γ_{t}) * f$ (Spatial and time derivatives pass through heat convolution for positive time); its class is $H_{t} f$ .

[F4]

For conjugate exponents and measurable $B, F$ with $B \in L^{p^{'}}$ and $F \in L^{p}$ , $\int ∣ B F ∣ \leq ∥ B ∥_{p^{'}} ∥ F ∥_{p}$ (Holder's inequality for integrals, including the endpoint cases).

[F5]

If $g_{N} \to g$ pointwise and $∣ g_{N} ∣ \leq G$ pointwise with $G$ integrable, then $\int g_{N} \to \int g$ (Dominated convergence).

[F6]

On sigma-finite product spaces, Tonelli's theorem equates the double integrals of a nonnegative measurable function with either iterated integral (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability); the counting measure on $N^{n}$ is sigma-finite, so it may be used as one factor.

[F7]

$\int_{- \infty}^{\infty} e^{- s^{2}} d s = \sqrt{π}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ ).

[F8]

The multi-indexed power series of Multi-indexed power series in $C^{m}$ and their absolute convergence converge absolutely at a point exactly when the associated series of moduli does, and box partial sums converge to the sum of an absolutely convergent series.

[F9]

Fix $m \geq 1$ , $a \in C^{m}$ , a polyradius $r$ and coefficients with $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ . Then $\sum_{α} c_{α} (z - a)^{α}$ converges absolutely and uniformly on each ${\overline{Δ}}_{θ r} (a)$ , $0 < θ < 1$ , its sum $g$ is holomorphic on $Δ_{r} (a)$ , and every iterated complex partial derivative exists there with $\partial_{z}^{β} g (a) = β! c_{β}$ (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

[F10]

A real analytic germ at $a$ is represented on a polydisc by $f (x) = \sum_{α} c_{α} (x - a)^{α}$ with real coefficients $c_{α} = D^{α} f (a) / α!$ , absolutely convergent there (Real analytic germs in several variables).

Proof

technique · direct

1.1A1F1F2F8givenalgebra

Expansion of the translated kernel: put $w = a - y$ and fix real $h$ with $∣ h_{i} ∣ \leq r$ for every $i$ . By [F1] and the addition formula [F2], $Γ (a + h - y, t) = Γ (w, t) \prod_{i < n} \exp (- w_{i} h_{i} / (2 t)) \exp (- h_{i}^{2} / (4 t))$ ; expanding each factor by the exponential series of [F2] and regrouping the finite products gives $Γ (a + h - y, t) = \sum_{α} b_{α} (w) h^{α}$ with $b_{α} (w) = Γ (w, t) \prod_{i < n} \sum_{m_{i} + 2 ℓ_{i} = α_{i}} \frac{(- w_{i} / (2 t))^{m_{i}}}{m_{i}!} \frac{(- 1 / (4 t))^{ℓ_{i}}}{ℓ_{i}!}$ , and the nonnegative series of moduli is bounded by $\sum_{α} ∣ b_{α} (w) ∣ r^{∣ α ∣} \leq Γ (w, t) \prod_{i < n} \exp (r ∣ w_{i} ∣ / (2 t)) \exp (r^{2} / (4 t)) = : B_{r} (w)$ , because the product of the two absolutely convergent exponential series is the absolutely convergent series for the product of the exponentials.

2.1step 1.1F1F6F7givenalgebra

The inequality $2 r ∣ w_{i} ∣ \leq w_{i}^{2} / 2 + 2 r^{2}$ gives $B_{r} (w) \leq (4 π t)^{- n / 2} \exp (3 n r^{2} / (4 t)) \exp (- ∣ w ∣^{2} / (8 t))$ . The last Gaussian is bounded and has integrable positive powers, by the Gaussian integral [F7], a scaling in each coordinate, and Tonelli [F6]. Thus $M_{n, p, t, r} : = ∥ B_{r} ∥_{p^{'}} < \infty$ for every $1 \leq p^{'} \leq \infty$ .

3.1step 1.1step 2.1F4F6given

Coefficient bounds: for every multi-index $α$ define $c_{α} (a) : = \int_{R^{n}} b_{α} (a - y) f (y) d y$ , absolutely convergent because $∣ b_{α} ∣ \leq r^{- ∣ α ∣} B_{r}$ and $B_{r} \in L^{p^{'}}$ with $f \in L^{p}$ by [F4]. Tonelli's theorem [F6] applied to the nonnegative summands over the counting index $α$ and $y \in R^{n}$ gives $\sum_{α} r^{∣ α ∣} ∣ c_{α} (a) ∣ \leq \sum_{α} r^{∣ α ∣} \int ∣ b_{α} (a - y) ∣ ∣ f (y) ∣ d y \leq \int B_{r} (a - y) ∣ f (y) ∣ d y \leq M_{n, p, t, r} ∥ f ∥_{p}$ by step 2.1 and [F4], the bound being uniform in the centre $a$ .

4.1step 1.1step 2.1step 3.1F3F5F8given

Power-series expansion of the representative: fix the centre $a$ and real $h$ with $∣ h_{i} ∣ \leq r$ . For the box partial sums $S_{N} (y) : = \sum_{α_{i} \leq N for all i} b_{α} (a - y) h^{α}$ of step 1.1 one has $S_{N} (y) \to Γ (a + h - y, t)$ pointwise in $y$ and $∣ S_{N} (y) ∣ \leq B_{r} (a - y)$ ; since $B_{r} (a - \cdot) ∣ f ∣ \in L^{1}$ by steps 2.1 and 3.1, dominated convergence [F5] gives $u (a + h, t) = \int Γ (a + h - y, t) f (y) d y = \sum_{α} c_{α} (a) h^{α}$ , where $u$ is the everywhere-defined representative of [F3]. The summable bound $\sum_{α} ∣ c_{α} (a) ∣ r^{∣ α ∣} < \infty$ from step 3.1 also gives uniform absolute convergence on this closed box, by [F8].

5.1step 3.1step 4.1F9given

Holomorphic extension and derivative formula: by step 3.1 the coefficients satisfy $∣ c_{α} (a) ∣ \leq r^{- ∣ α ∣} M_{n, p, t, r} ∥ f ∥_{p}$ for every $α$ , so [F9] with polyradius $(r, \dots, r)$ gives a holomorphic function $g$ on the polydisc $Δ_{r} (a) \subseteq C^{n}$ whose power series is $\sum_{α} c_{α} (a) (z - a)^{α}$ and whose iterated complex partial derivatives at $a$ are $\partial^{β} g (a) = β! c_{β} (a)$ ; by step 4.1 the restriction of $g$ to the real polydisc agrees with the representative $u (\cdot, t)$ , so $D^{α} u (a, t) = α! c_{α} (a)$ and $∣ D^{α} H_{t} f (a) ∣ = α! ∣ c_{α} (a) ∣ \leq α! r^{- ∣ α ∣} M_{n, p, t, r} ∥ f ∥_{p}$ , uniformly in $a$ .

6.1step 4.1step 5.1F3F10given

Real analyticity: if $f$ is real-valued, the coefficients $c_{α} (a)$ of step 4.1 are real and the absolute convergence of $\sum_{α} c_{α} (a) h^{α}$ for every real $h$ (step 4.1 with $r$ arbitrary) exhibits $u (\cdot, t)$ as a real analytic germ at every centre $a$ in the sense of [F10]; for complex $f$ apply the same conclusion to $Re f$ and $Im f$ , which lie in $L^{p}$ with $∥ \cdot ∥_{p} \leq ∥ f ∥_{p}$ , and add the two expansions using linearity of the integral, so the real and imaginary parts of $H_{t} f$ are real analytic.

6.2step 5.1givenalgebra

The choice $r = \sqrt{t}$ : the substitution $w = \sqrt{t} z$ gives $B_{\sqrt{t}} (\sqrt{t} z) = (4 π t)^{- n / 2} e^{- ∣ z ∣^{2} / 4} e^{\sum_{i} ∣ z_{i} ∣ / 2} e^{n / 4}$ and $d w = t^{n / 2} d z$ . For $p^{'} < \infty$ apply this to the $L^{p^{'}}$ integral; for $p^{'} = \infty$ take essential suprema. In both cases $M_{n, p, t, \sqrt{t}} = t^{- n / (2 p)} C_{n, p}$ with $C_{n, p} : = ∥ (4 π)^{- n / 2} e^{- ∣ \cdot ∣^{2} / 4} e^{\sum_{i} ∣ \cdot_{i} ∣ / 2} e^{n / 4} ∥_{p^{'}} < \infty$ ; step 5.1 with this $r$ gives the stated factorial Gaussian bound $C_{n, p} α! t^{- ∣ α ∣ / 2 - n / (2 p)} ∥ f ∥_{p}$ .

7.1step 5.1step 6.1step 6.2given∎

Steps 1.1, 2.1, 3.1, 4.1, 5.1, 6.1 and 6.2 establish the absolutely convergent spatial Taylor expansion of $H_{t} f$ at every centre with coefficients $c_{α} (a)$ , the uniform factorial bound $∥ D^{α} H_{t} f ∥_{\infty} \leq α! r^{- ∣ α ∣} M_{n, p, t, r} ∥ f ∥_{p}$ for every $r > 0$ , the real analyticity of $H_{t} f$ (real and imaginary parts for complex data), and the specialisation $r = \sqrt{t}$ ; the expansion converges for every real displacement because $r$ is arbitrary.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

106 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)