TheoremStatement: Literature-sourcedProof: 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.

Scalar resolvent stability for backward-Euler convolution quadrature

Statement

Let $0 < α < 1$ , $λ \geq 0$ , $T > 0$ , and $h = T / N$ with integer $N \geq 1$ . For any valid input $(u_{0}, F^{1}, \dots, F^{N})$ to Backward-Euler convolution quadrature for a Caputo equation, its updates define a unique sequence $V^{0} = 0, V^{1}, \dots, V^{N}$ satisfying

${\overset{ˉ}{\partial}}_{h}^{α} V^{n} + λ V^{n} = F^{n} - λ u_{0} (1 \leq n \leq N) .$

In particular, for $g^{1}, \dots, g^{N} \in R$ , use the algorithm with $u_{0} = 0$ and $F^{n} = g^{n}$ . Its output sequence $V$ satisfies

${\overset{ˉ}{\partial}}_{h}^{α} V^{n} + λ V^{n} = g^{n},$

where ${\overset{ˉ}{\partial}}_{h}^{α}$ is defined in Backward-Euler convolution quadrature for a Caputo equation. Then

$\max_{0 \leq n \leq N} ∣ V^{n} ∣ \leq Γ (1 - α) (2 T)^{α} \max_{1 \leq n \leq N} ∣ g^{n} ∣ .$

The direct full-history implementation uses exactly $N (N + 1) / 2$ terms in its convolution history sums. Retaining the solution sequence $V^{0}, \dots, V^{N}$ requires $N + 1$ solution values; this count excludes input and weight storage.

Facts & Assumptions

Given: $0 < α < 1$ , $λ \geq 0$ , $h = T / N$ , $V^{0} = 0$ , and forcing values $g^{n}$ .

[F1]

Backward-Euler convolution quadrature for a Caputo equation: for a general input $(u_{0}, F^{1}, \dots, F^{N})$ , the update is $(h^{- α} + λ) V^{n} = F^{n} - λ u_{0} - h^{- α} \sum_{j = 1}^{n} ω_{j} V^{n - j}$ ; for the zero-initial-value input $F^{n} = g^{n}$ , this is the recurrence in the stability claim.

[F2]

Backward-Euler fractional weights and positive partial sums: $ω_{j} < 0$ for $j \geq 1$ , $\sum_{j = 0}^{n} ω_{j} = p_{n} > 0$ , and $p_{n} \geq (n + 1)^{- α} / Γ (1 - α)$ .

[F3]

Real powers for positive bases, with the zero-base positive-exponent convention and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : for $h > 0$ and $α > 0$ , $h^{- α} = \exp (- α \log h) > 0$ .

[F4]

The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents gives $(x y)^{- α} = x^{- α} y^{- α}$ for $x, y > 0$ . By Continuity and derivatives of positive-base real powers, its derivative is $- α x^{- α - 1} < 0$ (positivity follows from [F3]); then 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)$ makes $x \mapsto x^{- α}$ decreasing on $(0, \infty)$ when $α > 0$ .

[F5]

Finite sums and finite products, by recursion defines the finite sums used below, and Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule permits reindexing them by a bijection.

Proof

1.1givenF1F3algebrainduction

For a general valid input $(u_{0}, F^{1}, \dots, F^{N})$ , [F3] and $λ \geq 0$ give $h^{- α} + λ > 0$ . Inductively, once $V^{0}, \dots, V^{n - 1}$ are defined, the update divides a specified real numerator by this positive denominator, so it gives a unique real $V^{n}$ . Rearranging the update gives ${\overset{ˉ}{\partial}}_{h}^{α} V^{n} + λ V^{n} = F^{n} - λ u_{0}$ by the operator definition in the algorithm. Induction proves the stated well-definedness and equation for the whole sequence.

1.2givenF1F5algebra

At update $n$ , [F1] includes exactly $n$ terms in the history sum. Thus the total count is $S = \sum_{n = 1}^{N} n$ . Reindexing by the bijection $n \mapsto N + 1 - n$ using [F5] also gives $S = \sum_{n = 1}^{N} (N + 1 - n)$ . Adding termwise yields $2 S = \sum_{n = 1}^{N} (N + 1) = N (N + 1)$ , so the total number is $N (N + 1) / 2$ . The sequence $V^{0}, \dots, V^{N}$ has exactly $N + 1$ solution values.

1.3givenF1F2choosealgebra

Write $G = \max_{1 \leq n \leq N} ∣ g^{n} ∣$ and $M = \max_{0 \leq n \leq N} ∣ V^{n} ∣$ . If $M = 0$ the claim is immediate. Otherwise choose the least index $n \geq 1$ with $∣ V^{n} ∣ = M$ . Taking absolute values in [F1] and using $- ω_{j} > 0$ gives $(h^{- α} + λ) M \leq G + h^{- α} M \sum_{j = 1}^{n} (- ω_{j}) .$ The sum on the right is $1 - p_{n}$ by [F2], so rearranging yields $(λ + h^{- α} p_{n}) M \leq G$ .

2.1step 1.3F2F3F4algebra∎

Since $n \leq N$ , $h (n + 1) \leq h (N + 1) = T + h \leq 2 T$ . By [F2], [F4], and [F3], $h^{- α} p_{n} \geq \frac{h^{- α} (n + 1)^{- α}}{Γ (1 - α)} = \frac{(h (n + 1))^{- α}}{Γ (1 - α)} \geq \frac{(2 T)^{- α}}{Γ (1 - α)} .$ As $λ \geq 0$ , step 1.3 gives $M \leq G / (h^{- α} p_{n}) \leq Γ (1 - α) (2 T)^{α} G$ . Since $V^{0} = 0$ , this is the stated estimate.

Depends on

Used by

Cited to discharge well-definedness by Backward-Euler convolution quadrature for a Caputo equation.

Dependency tree · two levels

54 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

Ralf Hiptmair, Advanced Numerical Methods for Computational Science and Engineering, lecture notes (2023), §3.3.3 (standard reference, not scraped)
C. Lubich, Convolution Quadrature and Discretized Operational Calculus I, Numerische Mathematik 52 (1988), §§1–2 (standard reference, not scraped)