PROOF 76

Prove.

Adding rounded values accumulates error

On the real numbers ℝ.

A way to read this proof

First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.

What you may use

A1|a + b| ≤ |a| + |b|
triangle inequality
A2a ≤ b, c ≤ d ⟹ a+c ≤ b+d
addition of inequalities
A3a ≤ b ≤ c ⟹ a ≤ c
transitivity of order
A4(a+b)+c = a+(b+c)
associativity of addition
A5a + b = b + a
commutativity of addition
A6adding c n times gives nc
meaning of a natural-number multiple
A7a(b − c) = ab − ac
distributive law
A8|x − round(x)| ≤ 1/2
bound on rounding error (Proof 75)
A9round(1/2) = 1
halves round up (Proof 75)
A10c ≥ 0 ⟹ |c| = c
meaning of absolute value
RP(1), P(k) ⟹ P(k+1)
mathematical induction
Ea = b ⟹ same operation on both sides
properties of equality

D1eᵢ = round(xᵢ) − xᵢ
rounding error of each term
L1T − S = e₁ + ⋯ + eₙ
Lemma 1
L2|Σaᵢ| ≤ Σ|aᵢ|
Lemma 2 — n-term triangle inequality
T1|T − S| ≤ n/2
Theorem 1

Nothing outside this list may be cited.

Definition D1

For real numbers x₁, …, xₙ, set S = x₁ + ⋯ + xₙ, T = round(x₁) + ⋯ + round(xₙ), eᵢ = round(xᵢ) − xᵢ.

Proof.

(1)eᵢ is the error incurred by rounding the i-th term.convention

(2)round(xᵢ) = xᵢ + eᵢ(1), E

∎

Lemma L1

T − S = e₁ + ⋯ + eₙ

Proof.

(1)T = (x₁ + e₁) + ⋯ + (xₙ + eₙ)D1, E

(2)Repeated application of associativity and commutativity of addition collects the xᵢ together and the eᵢ together.A4, A5, R

(3)T = S + (e₁ + ⋯ + eₙ)(1), (2)

(4)Subtracting S from both sides gives T − S = e₁ + ⋯ + eₙ(3), E

∎

Lemma L2

For every n, |a₁ + ⋯ + aₙ| ≤ |a₁| + ⋯ + |aₙ|

Proof.

(1)For n = 1 both sides equal |a₁|.convention

(2)Suppose it holds for n = k.assumption

(3)|(a₁ + ⋯ + aₖ) + aₖ₊₁| ≤ |a₁ + ⋯ + aₖ| + |aₖ₊₁|A1

(4)|a₁ + ⋯ + aₖ| + |aₖ₊₁| ≤ (|a₁| + ⋯ + |aₖ|) + |aₖ₊₁|(2), A2

(5)|a₁ + ⋯ + aₖ₊₁| ≤ |a₁| + ⋯ + |aₖ₊₁|(3), (4), A3

(6)Therefore it holds for every n.(1), (5), R

∎

Theorem T1

Rounding each of n real numbers and adding gives |T − S| ≤ n/2

Proof.

(1)T − S = e₁ + ⋯ + eₙL1

(2)|T − S| ≤ |e₁| + ⋯ + |eₙ|(1), L2

(3)For each i, |eᵢ| ≤ 1/2D1, A8

(4)|e₁| + ⋯ + |eₙ| ≤ 1/2 + ⋯ + 1/2(3), A2

(5)The sum of 1/2 added n times is n/2.A6

(6)|T − S| ≤ n/2(2), (4), (5), A3

∎

Corollary C

If xᵢ = 1/2 for every i, then |T − S| = n/2.

Proof.

(1)Suppose xᵢ = 1/2 for every i.assumption

(2)S is 1/2 added n times, so S = n/2(1), D1, A6

(3)round(1/2) = 1, so T is 1 added n times, and T = n(1), D1, A9, A6

(4)T − S = n − n/2(2), (3), E

(5)n − n/2 = n(1 − 1/2) = n/2A7

(6)n/2 ≥ 0, so |T − S| = n/2(4), (5), A10

(7)Therefore the bound n/2 of T1 cannot be improved.(6), T1

∎

Remark

Can A1 be removed from this proof?

That each term's error is at most 1/2 is already given. Check which line carries it over to the error of the sum.