Alphabeta MathHow 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 local IMEX Euler branch from contraction
Statement
Let , , , , and let be defined on the closed Euclidean ball . Suppose and there, with and . Then the IMEX Euler equation has exactly one solution in . Every in that ball satisfies In the algorithm One-step IMEX Euler with an implicit branch and residual status, ; this is a local branch result and gives no root outside the selected ball.
Facts & Assumptions
Given: , and the bounds in the Statement.
One-step IMEX Euler with an implicit branch and residual status: the implicit update is and its unscaled update residual is .
and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in : with the Euclidean metric is complete.
Complete metric space: every Cauchy sequence converges in the space and Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric: a metric space is complete when every Cauchy sequence converges to a point in that space.
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation: the Euclidean norm satisfies .
Lipschitz map, -Hölder map for rational , and contraction: a map is a contraction with constant when its output distance is at most times its input distance, where .
A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction from a nonempty complete metric space into itself has a unique fixed point.
Proof
The ball is nonempty because it contains . If is Cauchy in the ball, it is Cauchy in , so [F2] gives a limit . By [F4], ; letting gives , so remains in the ball. Thus the ball is a nonempty complete metric space by [F3].
Define . For every in the ball, , so maps the ball into itself; for in the ball, , and makes a contraction as in [F5].
Applying [F6] to the complete ball and the contraction from step 1.2 gives a unique fixed point , which is exactly the unique solution of in the ball.
For any in the ball, [F4] and step 2.1 give . Since , rearranging proves the residual bound.
Depends on
- One-step IMEX Euler with an implicit branch and residual status
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- Complete metric space: every Cauchy sequence converges in the space
- $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$
- Lipschitz map, $\alpha$-Hölder map for rational $0 < \alpha \le 1$, and contraction
- A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point
Used by
Dependency tree · two levels
56 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.