ExampleConstruction: AI-generatedVerification: 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.

A Caputo startup singularity and a graded-grid calculation

Example

Let $u (t) = \sqrt{t}$ , $0 \leq t \leq T$ , and $α = 1 / 2$ . Then $u$ is absolutely continuous and $D_{C}^{1 / 2} u (t) = Γ (3 / 2)$ for $t > 0$ , but $u \notin C^{2} ([0, T])$ . With $λ = 0$ and forcing $f (t) = Γ (3 / 2)$ , the uniform-grid first L1 step has state error

$u (h) - U^{1} = (1 - Γ (3 / 2)^{2}) \sqrt{h} > 0,$

so it is not $O (h^{3 / 2})$ . For the power-graded mesh $t_{k} = T (k / N)^{2}$ with $N = 4$ , the nodes are $0, T / 16, T / 4, 9 T / 16, T$ ; the first-step state error is $(1 - Γ (3 / 2)^{2}) \sqrt{T} / N$ . This first-node calculation does not prove an optimal global graded-mesh rate.

Facts & Assumptions

Given: Countable Choice, $T > 0$ , $u (t) = t^{1 / 2}$ , $α = 1 / 2$ , $λ = 0$ , $u_{0} = 0$ , $f (t) = Γ (3 / 2)$ , and an integer $N \geq 1$ .

[A1]

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

[F1]

Absolute continuity on a compact interval: $u$ is absolutely continuous when the sum of its absolute endpoint increments over any finite family of intervals with pairwise disjoint interiors is small whenever their total length is small.

[F2]

Fractional integral and Caputo derivative: for continuous $g$ , $I^{β} g (t) = Γ (β)^{- 1} \int_{0}^{t} (t - s)^{β - 1} g (s) d s$ is finite for every $t$ ; for $u \in A C$ with $u^{'} \in L^{1}$ , $D_{C}^{α} u = Γ (1 - α)^{- 1} \int_{0}^{t} (t - s)^{- α} u^{'} (s) d s$ almost everywhere, and at points where this integral is finite its pointwise integral value is the representative used below.

[F3]

The real Gamma function by Euler's integral: $Γ (q) = \int_{0}^{\infty} s^{q - 1} e^{- s} d s$ for $q > 0$ .

[F4]

Euler's real Beta integral and The real Beta--Gamma identity: $B (p, q) = Γ (p) Γ (q) / Γ (p + q)$ for $p, q > 0$ .

[F5]

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

[F6]

Uniform-grid and graded-grid L1 discretization: the first-step L1 weight on a uniform or general grid is $b_{1, 1} = t_{1}^{- α} / Γ (2 - α)$ .

[F7]

L1 stability and the smooth-data error bound: the $O (h^{2 - α})$ uniform-grid estimate assumes $u \in C^{2} ([0, T])$ .

[F8]

Real powers for positive bases, with the zero-base positive-exponent convention, Continuity and derivatives of positive-base real powers, and Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : for $t > 0$ , $(t^{1 / 2})^{'} = 1 / (2 \sqrt{t})$ and $(t^{1 / 2})^{''} = - 1 / (4 t^{3 / 2})$ .

[F9]

Integral of the fractional power kernel and Change of variable in an improper integral: $\int_{0}^{t} s^{- 1 / 2} d s = 2 \sqrt{t}$ for $t > 0$ , by reflection from the displayed kernel integral.

[F10]

Absolutely continuous functions have integrable derivatives: if $u$ is absolutely continuous, then $u^{'} \in L^{1} (0, T)$ .

[F11]

Monotonicity and nonnegative homogeneity of the nonnegative integral: pointwise domination of nonnegative measurable functions preserves the integral inequality and finiteness.

[F12]

Additivity of the nonnegative Lebesgue integral: the nonnegative integral is additive over a finite measurable partition.

[F13]

A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions: under [A1], if $S : (0, 1) \to (0, t)$ is a $C^{1}$ diffeomorphism and $g \in L^{1} (0, t)$ , then $\int_{0}^{t} g (s) d s = \int_{0}^{1} g (S (y)) ∣ S^{'} (y) ∣ d y$ .

[F14]

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)$ : for a continuous function on a closed interval differentiable on its interior, some interior derivative equals the secant slope.

[F15]

Positive L1 weights, discrete comparison, and residual stability: the returned L1 sequence satisfies its discrete equation at each grid node.

Verification

technique · direct

1.1givenF1F8F9F14algebra

Fix an arbitrary $ε > 0$ and set $η = \min (T, ε^{2} / 16)$ and $δ = ε^{2} / 8$ . By [F14] and $u^{'} (s) > 0$ for $s > 0$ , $u$ is increasing. Reorder any finite family of intervals with pairwise disjoint interiors by left endpoints; since $u$ is increasing, absolute endpoint increments equal endpoint increments, and monotonicity across the gaps shows their sum on a subinterval $[a, b]$ is at most $u (b) - u (a)$ . For $t > 0$ , $u^{'} (t) = 1 / (2 \sqrt{t})$ and $u (t) = \int_{0}^{t} (2 \sqrt{s})^{- 1} d s$ by [F9]. If $T \leq ε^{2} / 16$ , the family contributes at most $u (T) - u (0) = \sqrt{T} \leq ε / 4 < ε$ . If $T > ε^{2} / 16$ , split each interval at $η = ε^{2} / 16$ . The pieces below $η$ contribute at most $u (η) - u (0) = \sqrt{η} = ε / 4$ . On pieces above $η$ , $u^{'} (s) \leq 1 / (2 \sqrt{η}) = 2 / ε$ , so [F14] bounds their total increments by $(2 / ε) δ = ε / 4$ . Thus [F1]'s defining condition holds. But $u^{''} (t) = - 1 / (4 t^{3 / 2})$ is unbounded as $t ↓ 0$ , so $u \notin C^{2} ([0, T])$ .

2.1givenA1F2F10F11F12F8step 1.1

Fix $t > 0$ . By step 1.1 and [A1], [F10] gives $u^{'} \in L^{1} (0, T)$ . On $(0, t / 2)$ , $(t - s)^{- 1 / 2} \leq (t / 2)^{- 1 / 2}$ ; on $(t / 2, t)$ , $u^{'} (s) \leq 1 / (2 \sqrt{t / 2})$ . The fractional-integral clause of [F2] makes $(t - s)^{- 1 / 2}$ integrable on $(0, t)$ ; [F11] bounds the product on each half, and [F12] adds the two finite integrals. Hence $(t - s)^{- 1 / 2} u^{'} (s) \in L^{1} (0, t)$ for every $t > 0$ .

3.1givenA1F2F4F5F13step 2.1algebra

For the pointwise representative in [F2], apply [F13] to the integrable kernel in step 2.1 with $S (y) = t y$ . This is a $C^{1}$ diffeomorphism with $S^{'} (y) = t$ , and the Jacobian cancels the factor $t^{- 1}$ in $(t y)^{- 1 / 2} (t - t y)^{- 1 / 2}$ . Therefore $D_{C}^{1 / 2} u (t) = \frac{1}{2 Γ (1 / 2)} \int_{0}^{1} (1 - y)^{- 1 / 2} y^{- 1 / 2} d y = \frac{B (1 / 2, 1 / 2)}{2 Γ (1 / 2)} = \frac{1}{2} Γ (1 / 2) = Γ (3 / 2),$ using the Beta–Gamma identity [F4] and $Γ (1) = 1$ plus the functional equation [F5]. This holds for every $t > 0$ .

4.1givenF3F4F5F6F7F15step 3.1algebra

For the uniform grid, [F6] and [F15] give the equation $δ_{h}^{1 / 2} U^{1} = f (h)$ , hence $U^{1} = Γ (3 / 2)^{2} \sqrt{h}$ . Also $Γ (3 / 2) = \int_{0}^{\infty} \sqrt{s} e^{- s} d s < \frac{1}{2} \int_{0}^{\infty} (s + 1) e^{- s} d s = 1,$ because $(\sqrt{s} - 1)^{2} \geq 0$ with strict inequality except at $s = 1$ , and [F3]–[F5] evaluate the last integrals. Hence the stated error is positive. Its ratio to $h^{3 / 2}$ is $(1 - Γ (3 / 2)^{2}) / h$ , which is unbounded as $h ↓ 0$ ; the smooth-data theorem [F7] cannot be extended to this example.

5.1givenF6F15algebra∎

On the power-graded grid, $t_{1} = T / N^{2}$ , so [F6] gives $b_{1, 1} = N / (Γ (3 / 2) \sqrt{T})$ . The first discrete equation, justified by [F15], yields $U^{1} = Γ (3 / 2)^{2} \sqrt{T} / N$ , and subtracting it from $u (t_{1}) = \sqrt{T} / N$ gives the displayed graded first-step error. For $N = 4$ the nodes follow by substituting $k = 0, 1, 2, 3, 4$ into $t_{k} = T (k / 4)^{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

90 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)
Martin Stynes, Eugene O'Riordan, and José Luis Gracia, Error Analysis of a Finite Difference Method on Graded Meshes for a Time-Fractional Diffusion Equation, SIAM Journal on Numerical Analysis 55 (2017), §§1, 3–5 (standard reference, not scraped)