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 diagonal stiff diffusion step with linear reaction
Statement
Take , , , and . Compute the exact first-step state and the exponential-Euler and ETD2 first-step states, showing how the diagonal linear diffusion is exponentiated while the reaction is approximated.
Facts & Assumptions
Given: The finite-dimensional ODE, initial state, step size, and exact step maps from Exponential Euler and the two-stage ETD2 step maps.
Exponential Euler and the two-stage ETD2 step maps: exponential Euler is , while ETD2 uses the predictor and the correction.
The phi-function family by everywhere-convergent series: , so the matrix functions used at finite arguments are defined by convergent series.
The exponential function is smooth and : the real exponential is differentiable with .
If is differentiable with integrable then ; and a bounded derivative makes Lipschitz: integrating a continuous derivative from to gives the endpoint change.
The exponential is positive and satisfies : and for every real .
Sums, scalar multiples, products and quotients: , , , and when : products of differentiable real-valued functions obey the product rule.
The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with : the derivative of is for a fixed real .
Rectangular matrix multiplication and the identity matrix , including zero-sized shapes: powers of a diagonal matrix are diagonal with the corresponding scalar powers on the diagonal.
The displayed is componentwise, .
Verification
For coordinate with , put . The exact equation is , . The product rule [F6] and chain rule [F7] show . Integrating by [F4] gives , since [F3], [F7] give antiderivative . Dividing by the positive exponential using [F5] yields .
By [F8], powers of are diagonal with entries , so the series [F2] evaluates the matrix phi functions coordinatewise. The exact exponential-Euler map has and reaction value , so its coordinate is . The ETD2 predictor has that same coordinate; hence and the ETD2 coordinate is .
In particular the stiff coordinate uses : its exact, exponential-Euler, and ETD2 values are respectively , , and . All exponential and phi actions are at explicit matrix/scalar arguments; any numerical implementation must return the certificates specified by Certified-action implementation of exponential Euler and ETD2.
Depends on
- If $f : [a,b] \to \mathbb{R}^m$ is differentiable with integrable $f'$ then $\int_a^b f' = f(b)-f(a)$; and a bounded derivative makes $f$ Lipschitz
- The norm $\lVert v\rVert=\sqrt{\langle v,v\rangle}$ induced by a real or complex inner product
- The standard formulas $\langle x,y\rangle=\sum_{k<n}x_k y_k$ on $\mathbb R^n$ and $\sum_{k<n}x_k\overline{y_k}$ on $\mathbb C^n$ are inner products
- Exponential Euler and the two-stage ETD2 step maps
- Certified-action implementation of exponential Euler and ETD2
- The phi-function family by everywhere-convergent series
- The real exponential function and the number $e$ by a power series
- The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$
- The exponential function is smooth and $(\exp)'=\exp$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- 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)$
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
71 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
- Marlis Hochbruck and Alexander Ostermann, Exponential Integrators, Acta Numerica 19 (2010) (standard reference, not scraped)
- ISEM Team 2011/12, Operator Semigroups for Numerical Analysis, 15th Internet Seminar on Evolution Equations (standard reference, not scraped)