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

First-order CQ error for a compatible quadratic datum

Statement

Let $0 < α < 1$ , $λ \geq 0$ , $T > 0$ , $u_{0} \in R$ , and $u (t) = u_{0} + t^{2}$ on $[0, T]$ . Define

$f (t) : = \frac{2 t^{2 - α}}{Γ (3 - α)} + λ (u_{0} + t^{2}) .$

Then $u$ solves $D_{C}^{α} u + λ u = f$ and satisfies the compatibility condition $u^{'} (0) = 0$ . For $h = T / N$ and the backward-Euler CQ solution from Backward-Euler convolution quadrature for a Caputo equation with $F^{n} = f (n h)$ , there is a constant $C_{α, T}$ independent of $N$ , $u_{0}$ , and $λ$ such that

$\max_{0 \leq n \leq N} ∣ U^{n} - u (n h) ∣ \leq C_{α, T} h .$

Facts & Assumptions

Given: $0 < α < 1$ , $λ \geq 0$ , $T > 0$ , $u_{0} \in R$ , $u (t) = u_{0} + t^{2}$ , the forcing above, and $h = T / N$ .

[F1]

Fractional integral and Caputo derivative: $D_{C}^{α} u = I^{1 - α} u^{'}$ almost everywhere. At points where the integral is finite, its pointwise integral value supplies the representative used here; step 2.1 verifies finiteness for this polynomial.

[F2]

Backward-Euler convolution quadrature for a Caputo equation: ${\overset{ˉ}{\partial}}_{h}^{α} v^{n} = h^{- α} \sum_{j = 0}^{n} ω_{j} v^{n - j}$ for $v^{0} = 0$ .

[F3]

The real Beta--Gamma identity: $B (p, q) = Γ (p) Γ (q) / Γ (p + q)$ for positive $p, q$ .

[F4]

The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ : $Γ (x + 1) = x Γ (x)$ for $x > 0$ and $Γ (1) = 1$ .

[F5]

Generating-coefficient estimate for the quadratic CQ datum: if $β = 2 - α$ , the coefficient $s_{n}$ in the real Taylor series of $z (1 + z) (1 - z)^{α - 3}$ on $(- 1, 1)$ satisfies $∣ s_{n} - 2 n^{β} / Γ (β + 1) ∣ \leq C_{α} n^{β - 1}$ .

[F6]

Scalar resolvent stability for backward-Euler convolution quadrature: the algorithm's updates define the unique sequence satisfying the shifted CQ recurrence; for zero initial data and $λ \geq 0$ , the solution driven by forcing $r^{n}$ is bounded by $Γ (1 - α) (2 T)^{α} \max_{n} ∣ r^{n} ∣$ .

[F7]

Absolute continuity on a compact interval: absolute continuity means that summed endpoint increments over any finite disjoint interval family are small whenever the total interval length is small.

[F8]

Real powers for positive bases, with the zero-base positive-exponent convention and Continuity and derivatives of positive-base real powers: $0^{p} = 0$ for $p > 0$ , $t^{p}$ is continuous for $t \geq 0$ , and $(t^{p})^{'} = p t^{p - 1}$ for $t > 0$ .

[F9]

The real Gamma function by Euler's integral: $Γ (q) > 0$ for $q > 0$ .

[F10]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: $\sum_{n \geq 0} z^{n} = (1 - z)^{- 1}$ for $∣ z ∣ < 1$ .

[F11]

Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius: a power series can be differentiated term by term inside its radius.

[F12]

Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients: the product of two power-series sums has the Cauchy-product coefficients inside their common radius.

Proof

1.1givenF1F7F8algebraconstruct

For any finite disjoint interval family $[a_{j}, b_{j}] \subseteq [0, T]$ , $\sum_{j} ∣ u (b_{j}) - u (a_{j}) ∣ = \sum_{j} (b_{j} - a_{j}) (a_{j} + b_{j}) \leq 2 T \sum_{j} (b_{j} - a_{j}) .$ Given $ε > 0$ , choosing $δ = ε / (2 T + 1)$ verifies absolute continuity by [F7]. For almost every $t \in (0, T)$ , $u^{'} (t) = 2 t$ by [F8], so $u^{'} \in L^{1} (0, T)$ ; therefore the Caputo derivative is defined by [F1].

2.1givenF1F3F4F8F9step 1.1algebra

By [F8], $u^{'} (s) = 2 s$ for $s > 0$ ; at $s = 0$ the one-sided difference quotient is $s^{2} / s = s \to 0$ , so $u^{'} (0) = 0$ . Thus [F1] gives $D_{C}^{α} u (t) = \frac{2}{Γ (1 - α)} \int_{0}^{t} (t - s)^{- α} s d s = \frac{2 t^{2 - α}}{Γ (1 - α)} B (2, 1 - α) = \frac{2 t^{2 - α}}{Γ (3 - α)},$ where the substitution $s = t y$ and [F3]–[F4] give the last two equalities. Thus the stated $f$ makes $u$ an exact solution, and $u^{'} (0) = 0$ .

3.1step 2.1F2F5F10F11F12algebra

Put $v (t) = t^{2}$ , so $v (n h) = h^{2} n^{2}$ . Starting from the geometric series [F10] and differentiating termwise by [F11] gives $\sum_{n \geq 0} n^{2} z^{n} = z (1 + z) / (1 - z)^{3}$ . Multiplying this generating series by $h^{- α} (1 - z)^{α}$ and using [F12] shows that the discrete Caputo derivative of the exact nodal values is $h^{2 - α} s_{n}$ , with $s_{n}$ from [F5]. The exact derivative from step 2.1 is $2 h^{2 - α} n^{2 - α} / Γ (3 - α)$ .

4.1step 3.1F5algebra

Therefore the residual $τ_{n} : = {\overset{ˉ}{\partial}}_{h}^{α} v (n h) - D_{C}^{α} v (n h)$ satisfies $∣ τ_{n} ∣ \leq C_{α} h^{2 - α} n^{1 - α} = C_{α} h (n h)^{1 - α} \leq C_{α} T^{1 - α} h$ by [F5].

5.1step 4.1F2F6algebra∎

Subtracting the exact equation from the CQ recurrence, the error $E^{n} : = U^{n} - u (n h)$ has $E^{0} = 0$ and satisfies ${\overset{ˉ}{\partial}}_{h}^{α} E^{n} + λ E^{n} = - τ_{n}$ . Apply [F6] and step 4.1 to obtain $\max_{n} ∣ E^{n} ∣ \leq Γ (1 - α) (2 T)^{α} C_{α} T^{1 - α} h .$ The coefficient of $h$ depends only on $α$ and $T$ , proving the result.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

72 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–2 (standard reference, not scraped)
Ralf Hiptmair, Advanced Numerical Methods for Computational Science and Engineering, lecture notes (2023), §3.3.2 (standard reference, not scraped)