Estimation and rounding

Wanjiru is at a market in Nairobi with a 1000-shilling note. She wants a bag of rice for $289$ shillings, cooking oil for $412$ shillings and tomatoes for $198$ shillings. Before she reaches the stall, she wants to know: is $1000$ shillings enough?

Meanwhile her brother Kwame is doing homework. His calculator says $39 \times 61 = 1379$. Does that look right?

Neither of them needs the exact answer straight away. They need a quick answer they can trust. That is what estimation is for. You will use the place value and multiplication from whole-number arithmetic.

Where is $37$? It lies between the tens $30$ and $40$, and it is closer to $40$: only $3$ away, while $30$ is $7$ away. So we say $37$ rounded to the nearest ten is $40$.

Every number between $30$ and $40$ is closer to one of the two tens, except the halfway number $35$, which is exactly $5$ from each. We need a rule for that case. The usual school rule is: halfway rounds up, so $35$ rounds to $40$.

Below, the straight line shows each number $n$ and the staircase shows $n$ rounded to the nearest ten. Move $n$ and watch the gap between the two dots:

The rounding error. This graph shows the error (the rounded number minus the number itself) for every number from $0$ to $100$. The two flat lines are at $5$ and $-5$. Does the error ever escape?

Rounding decimals. Put the numbers on a line and choose $10$ parts for each whole, so the tick marks are tenths. Which tenth is each number closest to?

Rounding to the nearest ten changes a number by at most 5

For whole numbers we can say exactly how far: rounding moves a number up by at most $5$ (as with $35 \to 40$) or down by at most $4$ (as with $34 \to 30$). In the same way, rounding to the nearest hundred changes a number by at most $50$, and rounding to the nearest tenth by at most $0.05$.

Bounds add up

The same works with any bounds: add the lower bounds to get a lower bound, and add the upper bounds to get an upper bound. Multiplying works the same way for whole numbers: $30 \times 20 \le a \times b \le 40 \times 30$.

Subtracting is different! To make $a - b$ as large as possible, take the largest $a$ and the smallest $b$: at most $40 - 20 = 20$. To make it as small as possible, take the smallest $a$ and the largest $b$: at least $30 - 30 = 0$. For differences, the bounds work crosswise.

Rounding errors can add up

If you round several numbers before adding, each one may be off by up to $5$. So with $3$ numbers the total may be off by up to $3 \times 5 = 15$. Rounding the total once is off by at most $5$.

• $15 + 15 + 15 = 45$, which rounds to $50$. Rounding first: $20 + 20 + 20 = 60$, which is $15$ too much. The worst case really happens.
• $14 + 14 + 14 = 42$, which rounds to $40$. Rounding first: $10 + 10 + 10 = 30$. Rounding at every step gave a different final answer.

Most of the time errors partly cancel, because some numbers are rounded up and others down. But "most of the time" is not "always", and Margaret measures how often below.

How far off is a product estimate?

The area model from whole-number arithmetic tells us exactly. Since $39 = 40 - 1$ and $61 = 60 + 1$,

The estimate $2400$ was only $21$ too big. Small changes to the factors make small changes to the product, and the distributive law measures them.

1. "Rounding $35$ to the nearest ten gives $40$." — True, by the halfway-rounds-up rule.
2. "Rounding a whole number to the nearest ten never changes it by more than $5$." — True. The proof is above.
3. "Rounding at every step never changes the final rounded answer." — False. $14 + 14 + 14$: rounding first gives $30$, but $42$ rounds to $40$.
4. "If $30 \le a \le 40$ and $20 \le b \le 30$, then $a - b \le 10$." — False. $a = 40$ and $b = 20$ give $20$.
5. "$3.46$ rounded to the nearest whole number is $4$." — False. It is $3$.

/-- Round to the nearest ten, with halves rounded **up**: add `5`, then knock off the ones
digit. (`(n + 5) / 10` counts the whole tens in `n + 5`.) -/
def roundTen (n : Nat) : Nat := (n + 5) / 10 * 10

/-- The lesson's examples: `37 → 40`, `34 → 30`, the halfway case `35 → 40`, `999 → 1000`,
and `4372` rounds to `4370` (nearest ten) and `4400` (nearest hundred); `2950 → 3000`. -/
theorem round_examples :
    roundTen 37 = 40 ∧ roundTen 34 = 30 ∧ roundTen 35 = 40 ∧ roundTen 999 = 1000 ∧
      roundTen 4372 = 4370 ∧ roundHundred 4372 = 4400 ∧ roundHundred 2950 = 3000 := by
  decide

/-- Rounding to the nearest ten always gives a multiple of ten. This applies core Lean's
`Nat.mul_mod_left`: `(m × 10) % 10 = 0`. -/
theorem roundTen_multiple (n : Nat) : roundTen n % 10 = 0 := Nat.mul_mod_left _ _

/-- Rounding to the nearest ten moves a whole number **up by at most 5** or **down by at most
4**. So the rounding error is never more than `5`. -/
theorem roundTen_error (n : Nat) : roundTen n ≤ n + 5 ∧ n ≤ roundTen n + 4 := by
  unfold roundTen
  omega

/-- The gap (distance) between two whole numbers: the bigger minus the smaller. -/
def gap (a b : Nat) : Nat := if a ≤ b then b - a else a - b

/-- `roundTen n` really is a **nearest** multiple of ten: no multiple of ten `m` is closer to
`n`. (At a halfway point such as `35`, both `30` and `40` are equally close; we chose `40`.) -/
theorem roundTen_nearest (n m : Nat) (hm : m % 10 = 0) : gap n (roundTen n) ≤ gap n m := by
  unfold gap roundTen
  split <;> split <;> omega

/-- If `a` is between `la` and `ua`, and `b` is between `lb` and `ub`, then `a + b` is between
`la + lb` and `ua + ub`. This applies core Lean's `Nat.add_le_add` twice. -/
theorem add_bounds {a b la ua lb ub : Nat} (ha₁ : la ≤ a) (ha₂ : a ≤ ua)
    (hb₁ : lb ≤ b) (hb₂ : b ≤ ub) : la + lb ≤ a + b ∧ a + b ≤ ua + ub :=
  ⟨Nat.add_le_add ha₁ hb₁, Nat.add_le_add ha₂ hb₂⟩

/-- The example from the lesson: if `30 ≤ a ≤ 40` and `20 ≤ b ≤ 30`, then `50 ≤ a + b ≤ 70`.
It is `add_bounds` with the numbers filled in. -/
theorem bounds_example (a b : Nat) (ha₁ : 30 ≤ a) (ha₂ : a ≤ 40) (hb₁ : 20 ≤ b) (hb₂ : b ≤ 30) :
    50 ≤ a + b ∧ a + b ≤ 70 :=
  add_bounds ha₁ ha₂ hb₁ hb₂

/-- Bounds for a difference work **crosswise**: the largest `a − b` uses the largest `a` and the
smallest `b`. If `la ≤ a ≤ ua`, `lb ≤ b ≤ ub` and `ub ≤ la` (so no subtraction goes below
zero), then `la − ub ≤ a − b ≤ ua − lb`. -/
theorem sub_bounds {a b la ua lb ub : Nat} (ha₁ : la ≤ a) (ha₂ : a ≤ ua)
    (hb₁ : lb ≤ b) (hb₂ : b ≤ ub) (h : ub ≤ la) : la - ub ≤ a - b ∧ a - b ≤ ua - lb := by
  omega

/-- Bounds for a product: if `la ≤ a ≤ ua` and `lb ≤ b ≤ ub` (whole numbers, so nothing is
negative), then `la × lb ≤ a × b ≤ ua × ub`. This applies core Lean's `Nat.mul_le_mul`. -/
theorem mul_bounds {a b la ua lb ub : Nat} (ha₁ : la ≤ a) (ha₂ : a ≤ ua)
    (hb₁ : lb ≤ b) (hb₂ : b ≤ ub) : la * lb ≤ a * b ∧ a * b ≤ ua * ub :=
  ⟨Nat.mul_le_mul ha₁ hb₁, Nat.mul_le_mul ha₂ hb₂⟩

/-- Wanjiru's shopping: prices between `200` and `300`, `400` and `500`, and `100` and `200`
shillings always total between `700` and `1000`. So `1000` shillings is certainly enough.
The actual prices `289 + 412 + 198 = 899` fit. -/
theorem shopping (a b c : Nat) (ha₁ : 200 ≤ a) (ha₂ : a ≤ 300) (hb₁ : 400 ≤ b) (hb₂ : b ≤ 500)
    (hc₁ : 100 ≤ c) (hc₂ : c ≤ 200) : 700 ≤ a + b + c ∧ a + b + c ≤ 1000 := by
  omega

/-- Checking a calculator: `39 × 61` is near `40 × 60 = 2400`, so `1379` must be wrong. The
area model gives the exact gap: `(40 − 1) × (60 + 1) = 2400 + 40 − 60 − 1 = 2379`. -/
theorem product_estimate : 39 * 61 = 2379 ∧ 40 * 60 = 2400 ∧ 39 * 61 ≠ 1379 := by decide

/-- Rounding at every step can change the answer: rounding each `14` first gives
`10 + 10 + 10 = 30`, but the total `42` rounds to `40`. -/
theorem round_each_step_differs :
    roundTen 14 + roundTen 14 + roundTen 14 = 30 ∧ roundTen (14 + 14 + 14) = 40 := by decide

/-- Rounding `k` numbers before adding can move the total by up to `5` for each number: the
rounded total is at most `5 × k` above and at most `4 × k` below the true total. Induction on
the list, adding one number's rounding error (`roundTen_error`) at a time. -/
theorem rounded_total_error (xs : List Nat) :
    totalRounded xs ≤ total xs + 5 * xs.length ∧ total xs ≤ totalRounded xs + 4 * xs.length := by
  induction xs with
  | nil => simp [totalRounded, total]
  | cons x xs ih =>
    have hx := roundTen_error x
    simp only [totalRounded, total, List.length_cons]
    omega

/-- The bound `5 × k` can really be reached: `15 + 15 + 15 = 45`, but rounding each `15` up
to `20` gives `60`, which is `15 = 5 × 3` too much. -/
theorem error_bound_reached :
    totalRounded [15, 15, 15] = 60 ∧ total [15, 15, 15] = 45 ∧ 60 = 45 + 5 * 3 := by decide

/-- Rounding twice can go wrong. In hundredths, `3.46` is `346`. Rounded to the nearest whole
(`roundHundred`) it is `300`, that is `3`. But rounding first to the nearest tenth (`350`, that
is `3.5`) and then to the nearest whole gives `400`, that is `4`. -/
theorem double_rounding : roundHundred 346 = 300 ∧ roundTen 346 = 350 ∧ roundHundred 350 = 400 := by
  decide

"""How rounding errors add up: round first, or add first?

Rounding one number to the nearest ten moves it by at most 5, so rounding k
numbers before adding can move the total by up to 5k. We check every list of
three numbers below 60 exactly, then simulate (with a fixed seed) many
shopping lists of 5, 20 and 80 prices and compare the worst case 5k with the
errors that actually happen: positive and negative errors partly cancel.
"""

import random
import statistics

def round_ten(n):
    """Round a whole number to the nearest ten, halves up (35 -> 40)."""
    if n < 0:
        raise ValueError("whole numbers only")
    return (n + 5) // 10 * 10

def round_first_error(numbers):
    """(sum of rounded numbers) - (exact sum)."""
    return sum(round_ten(x) for x in numbers) - sum(numbers)

def exhaustive_triples(limit):
    """Over all triples from range(limit): (count, min error, max error,
    how often rounding first gives a different rounded total)."""
    rounded = [round_ten(x) for x in range(limit)]
    count = low = high = differ = 0
    for a in range(limit):
        for b in range(limit):
            for c in range(limit):
                exact = a + b + c
                err = rounded[a] + rounded[b] + rounded[c] - exact
                low, high = min(low, err), max(high, err)
                differ += rounded[a] + rounded[b] + rounded[c] != round_ten(exact)
                count += 1
    return count, low, high, differ

def simulate(k, trials, rng):
    """Errors of 'round first' for random lists of k prices from 100 to 999."""
    errors = []
    for _ in range(trials):
        prices = [rng.randint(100, 999) for _ in range(k)]
        errors.append(round_first_error(prices))
    return errors

def main():
    print("One number: rounding to the nearest ten moves it by at most 5:")
    worst = max(abs(round_ten(n) - n) for n in range(10_000))
    print(f"  largest change over 0..9,999: {worst}")
    count, low, high, differ = exhaustive_triples(60)
    print(f"All {count:,} lists of three numbers below 60, rounded first:")
    print(f"  error ranges from {low} to +{high} (the bound is -12 to +15)")
    print("  the rounded-first total differs from the rounded exact total in")
    print(f"  {differ:,} lists ({differ / count:.0%})")
    print()
    rng = random.Random(2024)
    print("Random shopping lists (prices 100-999, 2,000 lists each, seed 2024):")
    print("  items   worst possible   largest seen   typical size (RMS)")
    for k in (5, 20, 80):
        errors = simulate(k, 2_000, rng)
        rms = statistics.fmean(e * e for e in errors) ** 0.5
        print(f"  {k:>5}   {5 * k:>14}   {max(map(abs, errors)):>12}"
              f"   {rms:>18.1f}")
    print("  The typical error grows like the square root of the number of")
    print("  items, not like the number of items: errors up and down cancel.")
    print()
    print("Epistemic status: the bound 5k is proved in the lesson; the triples")
    print("are checked completely; the shopping lists are a random simulation,")
    print("so their numbers are statistical evidence that depends on the seed.")

if __name__ == "__main__":
    main()

The worst case grows in step with the number of items. The typical error grows much more slowly, because errors up and down partly cancel. The random lists are statistical evidence: a different seed would give slightly different numbers, but the worst-case bound is a theorem.

"""What to do with a 5: three rounding rules and Python's own round().

At school, halves round up (35 -> 40). Python's built-in round() uses another
rule, "round half to even" (25 -> 20, 35 -> 40), which many computers and
scientists use because it has no upward bias. We compare the rules on every
whole number from 0 to 9,999, show Python's round() in action, and show why
round(2.675, 2) gives 2.67: the computer never stored 2.675 exactly.
"""

from decimal import Decimal

def half_up(n):
    """School rounding to the nearest ten: halves go up."""
    return (n + 5) // 10 * 10

def half_even(n):
    """Nearest ten; a half goes to the ten whose tens digit is even."""
    q, r = divmod(n, 10)
    if r > 5 or (r == 5 and q % 2 == 1):
        q += 1
    return q * 10

def always_down(n):
    """Chop off the ones digit (this is not rounding to the nearest ten!)."""
    return n // 10 * 10

RULES = [("halves up (school)", half_up), ("halves to even", half_even),
         ("always down", always_down)]

def average_error(rule, numbers):
    """Exact average of rule(n) - n, as a Decimal."""
    total = sum(rule(n) - n for n in numbers)
    return Decimal(total) / Decimal(len(numbers))

def main():
    numbers = range(10_000)
    print("Rounding 0..9,999 to the nearest ten; average of (rounded - exact):")
    for name, rule in RULES:
        print(f"  {name:<20} {average_error(rule, numbers):+.1f}")
    print("  Halves-up pushes totals up a little; halves-to-even does not.")
    print()
    print("Halves up and halves to even can differ only on numbers ending in 5:")
    for n in (25, 35, 45, 65):
        print(f"  {n:>5}: up -> {half_up(n):>5}, to even -> {half_even(n):>5}")
    print()
    print("Python's built-in round() rounds halves to even:")
    print(f"  round(2.5) = {round(2.5)}, round(3.5) = {round(3.5)},"
          f" round(25, -1) = {round(25, -1)}, round(35, -1) = {round(35, -1)}")
    agree = all(round(n, -1) == half_even(n) for n in numbers)
    print(f"  round(n, -1) == halves-to-even for all n in 0..9,999: {agree}")
    print()
    print(f"A float surprise: round(2.675, 2) = {round(2.675, 2)}, because the")
    print("number the computer actually stores for 2.675 is")
    print(f"  {Decimal(2.675)}")
    print()
    print("Epistemic status: all averages are exact (every number was checked")
    print("and the arithmetic uses whole numbers and Decimal). Which rule is")
    print("'right' is a choice, not a theorem: each rule is a convention.")

if __name__ == "__main__":
    main()

Take your time. You can open a hint whenever you like.

Rounding to the nearest ten sorts the whole numbers into groups. The numbers that round to $40$ are $\{35, 36, 37, 38, 39, 40, 41, 42, 43, 44\}$. The numbers that round to $50$ are $\{45, \dots, 54\}$, and so on. Every whole number lands in exactly one group, and the groups never overlap. A sorting like this is a partition (sets). A pair of bounds describes a set too: "between $700$ and $1000$" is the set of all numbers $x$ with $700 \le x \le 1000$.

• Greece. Archimedes, in Measurement of a Circle (3rd century BCE), drew polygons inside and outside a circle and proved that $3\tfrac{10}{71} < \pi < 3\tfrac17$. It is one of the earliest uses of lower and upper bounds. Eratosthenes estimated the size of the Earth from the angles of shadows in Syene and Alexandria.
• China. Liu Hui (3rd century CE) refined the polygon method. Zu Chongzhi (5th century CE) showed that $3.1415926 < \pi < 3.1415927$, a record that stood for almost a thousand years.
• India. In the Āryabhaṭīya (499 CE), Āryabhaṭa gave $\pi \approx \tfrac{62832}{20000} = 3.1416$ and called the value āsanna, "approximate". He said clearly that it was an estimate.
• Central Asia. In 1424 Jamshīd al-Kāshī, working in Samarkand, computed $\pi$ correctly to $16$ decimal places. He worked out in advance how accurate each step had to be, so that the rounding errors could not spoil the final answer.
• The 20th century. The physicist Enrico Fermi was famous for quick, reasoned estimates of quantities that seemed impossible to work out. Such questions are now called Fermi problems.

• Lawrence Weinstein and John A. Adam, Guesstimation (2008). Estimation puzzles for curious teenagers and adults.
• Sanjoy Mahajan, Street-Fighting Mathematics (2010). The art of educated guessing, for grown-ups.
• George Pólya, How to Solve It (1945). A classic on problem solving, including checking whether an answer is reasonable.