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.
The forward and central error bounds have explicit balancing steps
Statement
Let . Consider the conservative error bounds from Forward and central differences have first- and second-order error bounds on a permitted step interval , where every stencil with stays inside the domain. If and , the forward bound
has the unique unconstrained minimizer and minimum . On the minimizer is . If and , the central conservative bound
has the unique unconstrained minimizer and minimum ; on the minimizer is . These optimize the displayed error bounds, not the unknown actual error.
If and the corresponding truncation constant is positive, the bound has infimum as and no minimizer for . If the corresponding truncation constant is and , the bound decreases with , so its capped minimum is at . If and the corresponding truncation constant are both zero, every permitted step is optimal.
Facts & Assumptions
Given: The derivative bounds, evaluation-error bound and permitted cap described above.
Forward and central differences have first- and second-order error bounds: the forward and central conservative bounds are and .
Square roots exist: a unique with ; the positives are and Existence and uniqueness of -th roots: a unique with : positive real numbers have unique positive square and cube roots.
Proof
Given: The hypotheses listed above.
Set . The identity gives , while . Since , equality holds exactly at . Thus is the unique unconstrained minimizer and its value is .
Set and . From , and . The difference is , with equality only at . Thus uniquely minimizes the unconstrained bound, and the minimum is .
If , then , since . Hence strictly decreases up to ; the global bound from step 1.1 gives the cap minimizer .
If , then , since and . Hence the central bound strictly decreases up to , so the cap minimizer is .
If and the corresponding truncation constant is positive, the bound in [F1] is a positive multiple of or and has infimum as , not attained for . If a truncation constant is and , the bound is a positive multiple of and decreases to as , while on a permitted capped interval it is minimized at . If both constants vanish the bound is identically zero.
Depends on
Used by
Dependency tree · two levels
27 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
- Nicholas J. Higham, What Is the Complex Step Approximation? (standard reference, not scraped)
- Andreas Buttenschoen, Introduction to Scientific Computing, Numerical Differentiation (standard reference, not scraped)