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.

L1 stability and the smooth-data error bound

Statement

Assume Countable Choice. Let $0 < α < 1$ , $λ \geq 0$ , $T > 0$ , and $h = T / N$ for an integer $N \geq 1$ , with uniform grid $t_{n} = n h$ . Let $u \in C^{2} ([0, T])$ and set $U^{0} = u (0)$ . For $1 \leq n \leq N$ , define the exact nodal forcing by its pointwise Caputo integral representative, $F^{n} : = \frac{1}{Γ (1 - α)} \int_{0}^{t_{n}} (t_{n} - s)^{- α} u^{'} (s) d s + λ u (t_{n}) (1 \leq n \leq N) .$ The integral is finite by the kernel-power bound and boundedness of $u^{'}$ . We use it as the pointwise representative of $D_{C}^{α} u$ for this smooth datum. Let $U^{n}$ be the uniform-grid L1 solution from Uniform-grid and graded-grid L1 discretization using those forcing values. The proof verifies absolute continuity of $u$ , so its Caputo derivative is defined. Put $C_{α} : = \frac{1}{Γ (1 - α)} (\frac{1}{1 - α} + \frac{1 + α}{2}) .$ Then $\max_{0 \leq n \leq N} ∣ U^{n} - u (t_{n}) ∣ \leq \frac{C_{α} T^{α}}{Γ (1 + α)} ∥ u^{''} ∥_{\infty} h^{2 - α} .$ The estimate is only asserted under the displayed $C^{2}$ hypothesis; its constant is not claimed uniform as $α ↑ 1$ .

Facts & Assumptions

Given: Countable Choice, $0 < α < 1$ , $λ \geq 0$ , $T > 0$ , $h = T / N$ , the uniform grid $t_{n} = n h$ , and $u \in C^{2} ([0, T])$ .

[A1]

Countable Choice: every sequence of nonempty sets admits a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )); it is used only in [F10].

[F1]

Uniform-grid and graded-grid L1 discretization: the discrete derivative is the integral of the piecewise-constant secant slope against $(t_{n} - s)^{- α} / Γ (1 - α)$ on each grid interval, and the algorithm's returned sequence satisfies its discrete equation by Positive L1 weights, discrete comparison, and residual stability.

[F2]

Positive L1 weights, discrete comparison, and residual stability: if $δ_{T}^{α} e^{n} + λ e^{n} = r^{n}$ , $e^{0} = 0$ , and $\max_{n} ∣ r^{n} ∣ \leq R$ , then $\max_{n} ∣ e^{n} ∣ \leq T^{α} R / Γ (1 + α)$ .

[F3]

Fractional integral and Caputo derivative: $D_{C}^{α} u (t) = Γ (1 - α)^{- 1} \int_{0}^{t} (t - s)^{- α} u^{'} (s) d s$ .

[F4]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{2} ([0, T])$ makes $u^{'}$ and $u^{''}$ continuous, with one-sided endpoint derivatives.

[F5]

Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact metric space, and compact subset of a metric space, and A continuous real function on a compact subset of $R$ is bounded: continuous real functions on $[0, T]$ are bounded; in particular $M_{1} : = ∥ u^{'} ∥_{\infty}$ and $M_{2} : = ∥ u^{''} ∥_{\infty}$ are finite.

[F6]

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.

[F7]

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 function continuous on a closed interval and differentiable in its interior has an interior point where its derivative equals its secant slope.

[F8]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous function on a compact interval is Riemann integrable.

[F9]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : the Riemann integral of a Riemann-integrable derivative equals the endpoint increment.

[F10]

A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: under [A1], a bounded Riemann-integrable function has the same Riemann and Lebesgue integrals.

[F11]

The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ : $Γ (2 - α) = (1 - α) Γ (1 - α)$ .

[F12]

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

[F13]

Integral of the fractional power kernel: $\int_{0}^{h} r^{- α} d r = h^{1 - α} / (1 - α)$ .

Proof

1.1givenF5F6F7construct

Set $M_{1} = ∥ u^{'} ∥_{\infty} < \infty$ by [F5]. For every interval $[a, b] \subseteq [0, T]$ , [F7] gives $∣ u (b) - u (a) ∣ \leq M_{1} (b - a)$ . Thus for any finite disjoint interval family, the sum of endpoint increments is at most $M_{1}$ times the total interval length. Given $ε > 0$ , choose $δ = ε / (M_{1} + 1)$ ; [F6] then shows $u$ is absolutely continuous.

2.1givenA1F4F5F7F8F9F10step 1.1

Put $M_{2} = ∥ u^{''} ∥_{\infty}$ . On each grid interval $[t_{k - 1}, t_{k}]$ , let $m_{k} = (u (t_{k}) - u (t_{k - 1})) / h$ and $e_{k} (s) = m_{k} - u^{'} (s)$ . The continuous function $u^{'}$ is Riemann integrable by [F8]; [F9] and [F10] give $h m_{k} = \int_{t_{k - 1}}^{t_{k}} u^{'} (s) d s$ for the Lebesgue integral, so $\int_{t_{k - 1}}^{t_{k}} e_{k} (s) d s = 0$ . By [F7] applied to $u^{'}$ , for any $r, s$ in this interval, $∣ u^{'} (r) - u^{'} (s) ∣ \leq M_{2} ∣ r - s ∣ \leq M_{2} h$ . Averaging in $r$ gives $∣ e_{k} (s) ∣ \leq M_{2} h$ .

3.1givenF1F3F11F13step 2.1construct

The formula [F1] and the Caputo definition [F3] now give, with $d_{n} : = Γ (1 - α)^{- 1} \int_{0}^{t_{n}} (t_{n} - s)^{- α} u^{'} (s) d s$ and $τ_{n} : = δ_{h}^{α} u (t_{n}) - d_{n}$ , $τ_{n} = \frac{1}{Γ (1 - α)} \sum_{k = 1}^{n} \int_{t_{k - 1}}^{t_{k}} e_{k} (s) (t_{n} - s)^{- α} d s .$

4.1step 2.1step 3.1F5F11F12F13algebra

On the last interval, [F13] and [F11] bound the absolute contribution to $τ_{n}$ by $\frac{M_{2} h}{Γ (1 - α)} \int_{0}^{h} r^{- α} d r = \frac{M_{2} h^{2 - α}}{Γ (2 - α)} .$ For $k < n$ , subtract the kernel value at the interval midpoint, using $\int e_{k} = 0$ from step 2.1. The derivative of the kernel has magnitude at most $α ((n - k) h)^{- α - 1}$ on that interval, so its variation from the midpoint is at most $α h ((n - k) h)^{- α - 1} / 2$ . Thus the $k$ th earlier contribution is at most $\frac{α M_{2}}{2 Γ (1 - α)} h^{2 - α} (n - k)^{- 1 - α} .$ Since $x^{- 1 - α}$ is decreasing, each term with $j \geq 2$ is at most $\int_{j - 1}^{j} x^{- 1 - α} d x$ ; hence $\sum_{j = 1}^{n - 1} j^{- 1 - α} \leq 1 + \int_{1}^{\infty} x^{- 1 - α} d x = 1 + 1 / α$ . Summing and using [F11] yields $∣ τ_{n} ∣ \leq C_{α} M_{2} h^{2 - α}$ for every $n$ .

4.2givenF1step 3.1algebra

Set $E^{n} = U^{n} - u (t_{n})$ . By the definition of $F^{n}$ , subtracting its exact nodal identity from the uniform-grid recurrence gives $δ_{h}^{α} E^{n} + λ E^{n} = - τ_{n}$ , with $E^{0} = 0$ .

5.1step 4.1step 4.2F2∎

Apply [F2] with $R = C_{α} M_{2} h^{2 - α}$ from step 4.1. This gives the claimed maximum error bound.

Depends on

Used by

A Caputo startup singularity and a graded-grid calculation Example

Dependency tree · two levels

91 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

Yumin Lin and Chuanju Xu, Finite difference/spectral approximations for the time-fractional diffusion equation, Journal of Computational Physics 225 (2007), §3 (standard reference, not scraped)
Bangti Jin, Raytcho Lazarov, and Zhi Zhou, An Analysis of the L1 Scheme for the Subdiffusion Equation with Nonsmooth Data, IMA Journal of Numerical Analysis, §§1–3 (standard reference, not scraped)