LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

The diagonal heat semigroup has the stated generator domain

Statement

Let $H$ , $A$ , and $E_{t}$ be as in Diagonal Dirichlet sine-mode heat model with constant forcing. The maps $E_{t}$ for $t \geq 0$ satisfy $E_{0} = I$ and $E_{t + s} = E_{t} E_{s}$ , are contractions in $ℓ^{2}$ , and are strongly continuous at $t = 0$ . Define the generator domain to consist of those $u \in H$ for which the right limit $\lim_{t ↓ 0} \frac{E_{t} u - u}{t}$ exists in $H$ . This domain is exactly $D (A) = {u : \sum_{k \geq 1} k^{4} ∣ u_{k} ∣^{2} < \infty}$ , and the limit equals $A u = (- k^{2} u_{k})_{k \geq 1}$ .

Facts & Assumptions

Given: The sequence space, diagonal operator, and maps in the Statement.

[F1]

Diagonal Dirichlet sine-mode heat model with constant forcing and Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ : $H$ consists of real families $u = (u_{k})_{k \geq 1}$ with $\sum_{k \geq 1} ∣ u_{k} ∣^{2} < \infty$ , and $(E_{t} u)_{k} = \exp (- k^{2} t) u_{k}$ for every $k \geq 1$ .

[F2]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ : $\exp (x + y) = \exp (x) \exp (y)$ and $\exp (0) = 1$ .

[F3]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ and The exponential function is strictly increasing: $\exp (x) > 0$ , and $x \leq y$ implies $\exp (x) \leq \exp (y)$ .

[F4]

The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : the scalar exponential is differentiable with derivative $\exp (x)$ , its compositions obey the chain rule, and a differentiable scalar function on an interval obeys the mean-value theorem.

Proof

1.1F1F2F3algebra

Coordinatewise, [F2] gives $\exp (- k^{2} (t + s)) = \exp (- k^{2} t) \exp (- k^{2} s)$ and $E_{0} u = u$ , so $E_{t + s} = E_{t} E_{s}$ . If $t \geq 0$ , [F3] gives $0 < \exp (- k^{2} t) \leq 1$ ; hence $\sum_{k} ∣ (E_{t} u)_{k} ∣^{2} \leq \sum_{k} ∣ u_{k} ∣^{2}$ , proving that $E_{t}$ maps $H$ to itself and is a contraction.

1.2F1F3F4algebra

At $x = 0$ the bound $0 \leq 1 - \exp (- x) \leq x$ is equality; for $x > 0$ , [F4] applied to $s \mapsto \exp (- s)$ on $[0, x]$ gives $1 - \exp (- x) = x \exp (- ξ)$ for some $ξ \in (0, x)$ , and [F3] bounds $\exp (- ξ)$ by $1$ . Thus the bound holds for all $x \geq 0$ . For $u \in D (A)$ , the $k$ th coordinate of $(E_{t} u - u) / t$ tends to $- k^{2} u_{k}$ by the chain rule and exponential derivative in [F4]. Its difference from that limit has absolute value at most $2 k^{2} ∣ u_{k} ∣$ , by the same bound. The squared tail of these differences is therefore at most $4 \sum_{k > K} k^{4} ∣ u_{k} ∣^{2}$ , which tends to zero; on every finite head the coordinate limits give norm convergence. Hence the right limit exists in $H$ and equals $A u$ .

2.1F1F3F4step 1.1algebrachoose

Fix $u \in H$ and $ε > 0$ . By convergence of its square sum, choose $K$ so that $\sum_{k > K} ∣ u_{k} ∣^{2} < ε^{2} / 4$ . The squared norm of the tail of $E_{t} u - u$ is at most this tail because $∣ \exp (- k^{2} t) - 1 ∣ \leq 1$ by [F3]; for the finitely many indices $k \leq K$ , continuity of the exponential at zero from [F4] makes their squared sum less than $ε^{2} / 4$ for all sufficiently small $t > 0$ . Thus $∥ E_{t} u - u ∥_{2} < ε$ , proving strong continuity at zero.

3.1F1F4step 1.2algebra∎

Conversely, suppose $(E_{t} u - u) / t$ converges in $H$ to $v$ . For each $k$ , coordinate evaluation is continuous since $∣ w_{k} ∣ \leq ∥ w ∥_{2}$ ; therefore its limit is $v_{k} = - k^{2} u_{k}$ , using [F4]. Since $v \in H$ , $\sum_{k} k^{4} ∣ u_{k} ∣^{2} = \sum_{k} ∣ v_{k} ∣^{2} < \infty$ , so $u \in D (A)$ . Together with step 1.2 this identifies the generator domain and its value.

Depends on

Used by

Dependency tree · two levels

52 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

Richard S. Laugesen, Spectral Theory of Partial Differential Equations, complete 120-page graduate lecture notes (standard reference, not scraped)