LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Principal-branch generating function for backward-Euler convolution quadrature

Statement

Let $0 < α < 1$ and let $(ω_{j})_{j \geq 0}$ be the weights defined by Backward-Euler convolution quadrature for a Caputo equation. Then the complex power series

$W (z) : = \sum_{j = 0}^{\infty} ω_{j} z^{j}$

converges absolutely for every $z$ in the open unit disc $D = {z \in C : ∣ z ∣ < 1}$ , and $W (z) = (1 - z)_{Log}^{} (z \in D),$ where the right side is the principal-branch power from Complex powers defined from a holomorphic logarithm branch. It is well-defined there because $1 - z$ lies in the principal-logarithm slit plane.

Facts & Assumptions

Given: $0 < α < 1$ and the backward-Euler CQ coefficient recurrence.

[F1]

Backward-Euler convolution quadrature for a Caputo equation: $ω_{0} = 1$ and $ω_{j} = ((j - 1 - α) / j) ω_{j - 1}$ for $j \geq 1$ .

[F2]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges and If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ : for $0 \leq r < 1$ , $\sum_{j \geq 0} r^{j}$ converges, and a nonnegative series dominated termwise by a convergent nonnegative series converges.

[F3]

Complex series, absolute convergence, complex power series, and radius of convergence: the radius of a complex power series is the radius of its real modulus series. Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term: inside its disc of convergence, the sum is holomorphic.

[F4]

A real power series about a centre, its interval of convergence, and its radius in $[0, + \infty]$ and Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius: a real power series can be differentiated termwise inside its radius.

[F5]

Continuity and derivatives of positive-base real powers, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : for $x > 0$ , $(x^{q})^{'} = q x^{q - 1}$ and ordinary real chain and product rules hold.

[F6]

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)$ : a differentiable real function with zero derivative on an interval is constant.

[F7]

The unit disc, the upper half-plane, and Blaschke factors and Star-shaped plane domains are homologically simply connected: the nonempty open unit disc is a complex domain.

[F8]

Complex powers defined from a holomorphic logarithm branch: $z_{Log}^{} = \exp (α Log z)$ on the principal-logarithm slit plane. The principal logarithm is the normalised holomorphic branch on the slit plane: the principal logarithm is holomorphic there.

[F9]

The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself, and Linearity, product, reciprocal, and quotient rules for complex derivatives: compositions of complex differentiable maps are complex differentiable, the exponential is entire, and affine maps are holomorphic.

[F10]

On positive reals, the principal branch power agrees with the published real power: on positive real bases, principal-branch powers agree with real powers.

[F11]

Identity theorem for holomorphic functions: two holomorphic functions on a complex domain that agree on a set with an interior accumulation point agree throughout the domain.

[F12]

Real and imaginary parts, complex conjugation, and modulus, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , and The reals form a totally ordered field: if $x \geq 1$ is real, then $∣ x ∣ = x$ .

Proof

1.1givenF1F2F3algebra

The recurrence [F1] gives $∣ ω_{0} ∣ = 1$ , $ω_{1} = - α$ with $∣ ω_{1} ∣ = α < 1$ , and for $j \geq 2$ gives $ω_{j} = ((j - 1 - α) / j) ω_{j - 1}$ with $0 < (j - 1 - α) / j < 1$ , so induction yields $∣ ω_{j} ∣ \leq 1$ for all $j$ . For each $0 \leq r < 1$ , [F2] bounds $\sum_{j \geq 0} ∣ ω_{j} ∣ r^{j}$ by a convergent geometric series; the radius definition [F3] therefore gives radius at least $1$ , and the complex series sum $W$ is holomorphic on $D$ by [F3].

1.2givenF1F4F5F6algebra

For real $x \in (- 1, 1)$ the same coefficients define a real power series of radius at least $1$ ; termwise differentiation [F4] gives $W^{'} (x) = \sum_{j \geq 0} (j + 1) ω_{j + 1} x^{j}$ . By [F1], $(j + 1) ω_{j + 1} = (j - α) ω_{j}$ , hence $W^{'} (x) = \sum_{j \geq 0} (j - α) ω_{j} x^{j} = x W^{'} (x) - α W (x)$ and $(1 - x) W^{'} (x) = - α W (x)$ . Since $1 - x > 0$ , [F5] gives $H^{'} (x) = 0$ for $H (x) : = W (x) (1 - x)^{- α}$ ; [F6] makes $H$ constant, and $H (0) = ω_{0} = 1$ , so $W (x) = (1 - x)^{α}$ throughout $(- 1, 1)$ .

1.3givenF8F9F12construct

Fix $z \in D$ . If $1 - z$ were real $r \leq 0$ , then $z = 1 - r \geq 1$ would be positive real, so [F12] would give $∣ z ∣ = z \geq 1$ , a contradiction. Thus $1 - z$ is in the slit plane and $P (z) : = (1 - z)_{Log}^{}$ is defined; [F8] makes the principal logarithm holomorphic there, and [F9] with the branch definition makes $P$ holomorphic on $D$ .

2.1step 1.1step 1.2step 1.3F7F10F11∎

By [F7] the unit disc is a complex domain. For every real $x \in (- 1, 1)$ , [F10] identifies $P (x)$ with $(1 - x)^{α}$ , so step 1.2 gives $P (x) = W (x)$ . The agreement set contains an interval accumulating at $0 \in D$ ; since $W$ and $P$ are holomorphic by steps 1.1 and 1.3, the identity theorem [F11] gives $W = P$ throughout $D$ , including $z = 0$ .

Depends on

Used by

Backward-Euler fractional weights and positive partial sums Lemma

Dependency tree · two levels

126 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

C. Lubich, Convolution Quadrature and Discretized Operational Calculus I, Numerische Mathematik 52 (1988), §1.1 (standard reference, not scraped)
Ralf Hiptmair, Advanced Numerical Methods for Computational Science and Engineering, ETH Zürich lecture notes (2023), §§3.3.2.24–3.3.2.27 (standard reference, not scraped)