Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29
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.

Local conditioning times backward error controls forward error to first order

Statement

Let f:X→Y be a map between normed spaces, let x∈dom⁡f, and let κ:=κabs(f,x) be the absolute local condition number of Absolute and relative local condition numbers of a problem map.

  1. Quantified form. If κ<+∞, then for every c>κ there is a δ>0 such that every h∈X with 0<∥h∥<δ and x+h∈dom⁡f satisfies ∥f(x+h)−f(x)∥  ≤  c ∥h∥.
  2. First-order form. If κ<+∞, then along admissible h, ∥f(x+h)−f(x)∥  ≤  (κ+o(1))∥h∥as ∥h∥→0, that is: for every ε>0 there is δ>0 such that 0<∥h∥<δ implies ∥f(x+h)−f(x)∥≤(κ+ε)∥h∥.
  3. Relative form. If additionally x≠0 and f(x)≠0, and κrel:=κ ∥x∥/∥f(x)∥, then along admissible h, ∥f(x+h)−f(x)∥∥f(x)∥  ≤  (κrel+o(1))∥h∥∥x∥as ∥h∥→0.

In the vocabulary of Forward and backward stability for a problem family under an arithmetic model: a computed value y^=f(x+h) has backward error ∥h∥, and its forward error is, to first order in that backward error, at most the condition number times the backward error; the linear-system instance uses the backward error of Normwise and componentwise backward error for an approximate linear-system solution.

Facts & Assumptions

Given: Normed spaces X,Y, a map f:X→Y, a point x∈dom⁡f, and κ=inf⁡δ>0Sf,x(δ) where Sf,x(δ)=sup⁡{∥f(x+h)−f(x)∥/∥h∥:0<∥h∥<δ, x+h∈dom⁡f}.

[L1]

The absolute condition number is the infimum over δ>0 of the nondecreasing map δ↦Sf,x(δ) (Absolute and relative local condition numbers of a problem map).

[L2]

An infimum characterisation: if κ is the infimum of a set S⊆[0,+∞], then for every c>κ there is an element s∈S with s<c; in particular for every c>κ there is δ>0 with Sf,x(δ)<c.

Proof

technique · direct
1.1L1L2choose

By [L2] applied to the set S={Sf,x(δ):δ>0} whose infimum is κ by [L1], every c>κ admits some δ0>0 with Sf,x(δ0)<c.

2.1step 1.1givenalgebra

By the definition of Sf,x(δ0) as a supremum, every admissible h with 0<∥h∥<δ0 satisfies ∥f(x+h)−f(x)∥/∥h∥≤Sf,x(δ0)<c, hence ∥f(x+h)−f(x)∥≤c∥h∥, which is claim 1 with δ:=δ0.

3.1step 2.1algebra

For every ε>0 the number c:=κ+ε is strictly larger than κ, so claim 1 supplies δ>0 with ∥f(x+h)−f(x)∥≤(κ+ε)∥h∥ for all admissible h of norm below δ; this is exactly the stated bound, which is claim 2.

4.1step 3.1givenalgebra

For the relative form, divide the inequality of claim 2 by the fixed positive number ∥f(x)∥ and multiply by the fixed positive number ∥x∥: ∥f(x+h)−f(x)∥/∥f(x)∥≤(κ+ε)∥h∥/∥f(x)∥=(κ∥x∥/∥f(x)∥+ε∥x∥/∥f(x)∥)∥h∥/∥x∥, and the error term is o(1)∥h∥/∥x∥ because the positive constants ∥x∥,∥f(x)∥ are fixed, which is claim 3.

5.1step 2.1step 3.1step 4.1∎

Claims 1, 2 and 3 are steps 2.1, 3.1 and 4.1.

Depends on

Used by

Dependency tree · two levels

8 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