Manuscript Em04-A@2 · Em04-A-v2.tex · proposition · f5b28abc

Proposition: Entrywise certificate

Validated dynamical residual interfaces › Finite polynomial data and arithmetic enclosure · lines 1578–1597 · proof included or linked

Em04-A@2#prop:entrywise

Back to manuscript

If certified bounds satisfy

∣ R_{ij} (τ) ∣ \leq b_{k, ij} (τ \in [t_{k}, t_{k + 1}]),

then an admissible residual bound is

B_{k} = N (i, j \sum b_{k, ij}^{2})^{1/2},

with the displayed value rounded upward.

Proof. For singular values $s_{ℓ}$ , Cauchy–Schwarz gives $\sum_{ℓ} s_{ℓ} \leq N (\sum_{ℓ} s_{ℓ}^{2})^{1/2}$ . Hence $∥ R ∥_{1} \leq N ∥ R ∥_{F}$ . The entrywise bounds enclose its Frobenius norm.

Displayed formulas in this passage

unlabeled · line 1581
$∣ R_{ij} (τ) ∣ \leq b_{k, ij} (τ \in [t_{k}, t_{k + 1}]),$
unlabeled · line 1586
$B_{k} = N (i, j \sum b_{k, ij}^{2})^{1/2},$

Nearby in this section

section: Finite polynomial data and arithmetic enclosure
section: Finite polynomial data and arithmetic enclosure