Skip to content
The Lumenary
Grades 6–8Ages 11–14 60 min

Graphs of change

A graph can tell a whole story — where something sped up, stopped or turned back. Steepness is the rate of change, and averages hide surprises.

Formally verified · 14 LeanComputationally tested · 2 PythonAI-drafted · awaiting human reviewMathematically reviewed: Awaiting human review

Your guides: Chloe, Margaret, Gideon

MotivationH

A story in a graph

Keza lives near Huye in Rwanda. One Saturday she cycles to the market, 66 kilometres away, and back. Her phone records how far she is from home, minute by minute. Here is the graph.

0204060time (minutes)0246km from homeABCDE
Keza's distance from home during her trip to market. Segment A: riding out; B: stopped to fix a loose chain; C: riding on; D: at the market; E: riding home.

Without being told anything else, we can read off a lot. When was she stopped? When was she riding fastest? How far did she ride altogether? And here is a harder one: the graph starts and ends at zero. Does that mean that, on average, nothing happened? By the end of this lesson you will be able to answer all of these precisely.

IntuitionH

Reading the shape of a graph

A graph of change, drawn in the coordinate plane, shows how one quantity depends on another — very often, how something changes over time. Read it from left to right, like a sentence:

  • Going up (segments A and C): the distance from home is increasing — Keza is riding away.
  • Flat (B and D): the distance is not changing — she has stopped.
  • Going down (E): the distance is decreasing — she is coming back.

The steepness tells us how fast the quantity changes. Segment E is the steepest: she covers 66 km in 2020 minutes on the way home, faster than on the way out. (Perhaps the road home is downhill — but the graph does not show hills!)

DefinitionsH

Rates of change

Definition— average rate of change

If a quantity has the value y(a)y(a) at x=ax = a and y(b)y(b) at x=bx = b, with a≠ba \neq b, its average rate of change between aa and bb is

y(b)−y(a)b−a=change in ychange in x.\frac{y(b) - y(a)}{b - a} = \frac{\text{change in } y}{\text{change in } x}.

On the graph, it is the slope of the straight segment joining the two points (see linear relationships). Its units are "units of yy per unit of xx": kilometres per minute, degrees per hour, litres per second. A rate is a ratio of two changes (see ratios and rates).

Definition— increasing, decreasing, constant

On an interval of xx-values, a graph is

  • increasing if yy gets larger whenever xx gets larger: x1<x2x_1 < x_2 implies y(x1)<y(x2)y(x_1) < y(x_2);
  • decreasing if yy gets smaller whenever xx gets larger: x1<x2x_1 < x_2 implies y(x1)>y(x2)y(x_1) > y(x_2);
  • constant if yy has the same value at every xx in the interval.

Definition— average speed

For a journey, the average speed is the total distance travelled divided by the total time taken.

If a graph shows the distance from a starting point along a route, the slope of a segment is the average rate of change of that distance. As long as the traveller does not turn round during the segment, the size of the slope is the average speed, and its sign says whether they are moving away (++) or coming back (−-). If the graph shows the total distance travelled, it can never go down, and its slopes are exactly the average speeds.

Worked examplesH

Worked examples

Example— Rates on Keza's journey

segmenttimechange in distanceaverage ratein km/h
A00–2020 min+4+4 km420=0.2\tfrac{4}{20} = 0.2 km/min1212
B2020–2525 min00 km00 km/min00
C2525–3535 min+2+2 km210=0.2\tfrac{2}{10} = 0.2 km/min1212
D3535–5555 min00 km00 km/min00
E5555–7575 min−6-6 km−620=−0.3\tfrac{-6}{20} = -0.3 km/min−18-18

(To turn km per minute into km per hour, multiply by 6060.) A and C have the same slope, so she rode at the same average speed on both; E is steepest, 1818 km/h, and the minus sign records that she was heading home.

Example— The whole trip: zero change, but not nothing

Over the whole trip, from 00 to 7575 minutes, the distance from home changes by 0−0=00 - 0 = 0, so the average rate of change is 00 km/h. But Keza rode 4+2+6=124 + 2 + 6 = 12 km in 7575 minutes =1.25= 1.25 hours: her average speed was 121.25=9.6\tfrac{12}{1.25} = 9.6 km/h. A zero average rate of change does not mean nothing happened — only that she ended where she started.

Example— A table: a hot day in Delhi

Air temperatures on a hot day in Delhi (illustrative numbers):

time6 a.m.9 a.m.noon3 p.m.6 p.m.9 p.m.
temperature (°C)292933333838404037373333

From 6 a.m. to noon the average rate of change is 38−296=1.5\tfrac{38 - 29}{6} = 1.5 °C per hour. From noon to 6 p.m. it is 37−386=−16\tfrac{37 - 38}{6} = -\tfrac{1}{6} °C per hour: nearly zero, even though the temperature rose to 4040 °C and fell again in between. From 3 p.m. to 9 p.m. it is 33−406≈−1.17\tfrac{33 - 40}{6} \approx -1.17 °C per hour. The table only tells us the values at six moments; what happened between them is a guess.

Example— Sketching from a description

"The bath fills steadily for 8 minutes. Then the tap is turned off, and Tomás gets in — the water level jumps up. He lies still for 10 minutes, gets out, and pulls the plug; the bath empties steadily in 4 minutes."

A sketch of water depth against time: a straight rising segment for 8 minutes; a short, very steep rise when Tomás gets in; a flat segment for 10 minutes; a short, very steep drop when he gets out (back to the depth before he got in); then a straight falling segment down to 00, steeper than the filling segment because emptying takes 44 minutes rather than 88. The heights come from the story's quantities; the steepness from how fast things happen.

ProofH

What rates of change can tell us

Let yy be a quantity that depends on xx, and write R(a,b)R(a, b) for its average rate of change between aa and bb.

Theorem— change = rate × time

For a≠ba \neq b:   y(b)−y(a)=R(a,b)⋅(b−a)\;y(b) - y(a) = R(a, b) \cdot (b - a). On a distance–time graph: distance covered == average speed ×\times time taken.

Proof

Multiply the definition R(a,b)=y(b)−y(a)b−aR(a, b) = \dfrac{y(b) - y(a)}{b - a} by b−ab - a.

∎

Theorem— the sign of the rate

A graph is increasing on an interval if and only if every average rate of change R(x1,x2)R(x_1, x_2) with x1<x2x_1 < x_2 in the interval is positive. Likewise, it is constant on the interval if and only if all these average rates are 00.

Proof

Take x1<x2x_1 < x_2. The run x2−x1x_2 - x_1 is positive, so the quotient y(x2)−y(x1)x2−x1\dfrac{y(x_2) - y(x_1)}{x_2 - x_1} is positive exactly when the rise y(x2)−y(x1)y(x_2) - y(x_1) is positive, that is, exactly when y(x1)<y(x2)y(x_1) < y(x_2). "Increasing" says this for every such pair, and so does "all rates are positive". In the same way, the quotient is 00 exactly when y(x1)=y(x2)y(x_1) = y(x_2), so all the rates are 00 exactly when yy never changes.

∎

So a horizontal segment really does mean "not changing", and a straight segment that slopes upwards means steady increase. (Decreasing works the same way, with negative rates.)

Next: how do the rates over two pieces of an interval combine? Not by simply averaging them.

Theorem— combining intervals

For a<b<ca < b < c:

R(a,c)=(b−a) R(a,b)+(c−b) R(b,c)c−a.R(a, c) = \frac{(b - a)\,R(a, b) + (c - b)\,R(b, c)}{c - a}.

The rate over the whole interval is the average of the two rates, weighted by the lengths of the pieces. In particular, R(a,c)R(a, c) lies between R(a,b)R(a, b) and R(b,c)R(b, c).

Proof

The total change is the sum of the changes on the two pieces, and by "change = rate × time":

y(c)−y(a)=(y(b)−y(a))+(y(c)−y(b))=(b−a)R(a,b)+(c−b)R(b,c).y(c) - y(a) = \big(y(b) - y(a)\big) + \big(y(c) - y(b)\big) = (b - a)R(a, b) + (c - b)R(b, c).

Dividing by c−ac - a gives the formula. Now suppose R(a,b)≤R(b,c)R(a, b) \leq R(b, c) (otherwise swap the roles). Replacing R(b,c)R(b, c) by the smaller number R(a,b)R(a, b) makes the right-hand side no larger, so (c−a)R(a,c)≥(b−a)R(a,b)+(c−b)R(a,b)=(c−a)R(a,b)(c - a)R(a, c) \geq (b - a)R(a, b) + (c - b)R(a, b) = (c - a)R(a, b). Dividing by c−a>0c - a > 0 gives R(a,c)≥R(a,b)R(a, c) \geq R(a, b). Replacing R(a,b)R(a, b) by the larger R(b,c)R(b, c) shows R(a,c)≤R(b,c)R(a, c) \leq R(b, c) in the same way.

∎

For Keza's first 3535 minutes: R(0,35)=20⋅12+5⋅0+10⋅1235=727≈10.3R(0, 35) = \dfrac{20 \cdot 12 + 5 \cdot 0 + 10 \cdot 12}{35} = \dfrac{72}{7} \approx 10.3 km/h — between 00 and 1212, as it must be, but not their plain average.

Theorem— same average, different journeys

Two quantities can have the same average rate of change over an interval but behave differently within it.

Proof

One example is enough. Ana runs 100100 m at a steady 55 m/s, so she is 5t5t metres along after tt seconds. Ben runs at 77 m/s for 1010 seconds and then, tiring, at 33 m/s. Both finish 100100 m in 2020 s, so both average 55 m/s. But after 1010 s Ana has run 5050 m and Ben 7070 m.

∎

Theorem— round trips

If you travel a distance dd at speed uu and return at speed vv (with d,u,v>0d, u, v > 0), your average speed is

2ddu+dv=2uvu+v,\frac{2d}{\frac{d}{u} + \frac{d}{v}} = \frac{2uv}{u + v},

which is never more than u+v2\tfrac{u + v}{2}, and equals it only when u=vu = v.

Proof

The total distance is 2d2d, and the times for the two legs are du\tfrac{d}{u} and dv\tfrac{d}{v}. Multiplying the top and bottom of 2dd/u+d/v\tfrac{2d}{d/u + d/v} by uvd\tfrac{uv}{d} gives 2uvv+u\tfrac{2uv}{v + u}. For the comparison,

u+v2−2uvu+v=(u+v)2−4uv2(u+v)=(u−v)22(u+v),\frac{u + v}{2} - \frac{2uv}{u + v} = \frac{(u + v)^2 - 4uv}{2(u + v)} = \frac{(u - v)^2}{2(u + v)},

which is never negative (a square is never negative) and is 00 only when u=vu = v.

∎

The classic puzzle: drive 6060 km at 3030 km/h (22 hours) and back at 6060 km/h (11 hour). The average speed is 1203=40\tfrac{120}{3} = 40 km/h — not 4545. You spend more time at the slower speed, so it counts for more.

ExplanationH

From average to instantaneous

A stone dropped from a cliff falls faster and faster. In the idealised model with no air resistance, it has fallen d(t)=4.9 t2d(t) = 4.9\,t^2 metres after tt seconds. The graph is curved, so its average rate of change depends on the interval we choose. What is the stone's speed at the moment t=2t = 2?

Take a short interval from 22 to 2+h2 + h seconds (with h≠0h \neq 0). The average speed over it is

4.9(2+h)2−4.9⋅22h=4.9 (4h+h2)h=4.9 (4+h)=19.6+4.9 h   m/s.\frac{4.9(2 + h)^2 - 4.9 \cdot 2^2}{h} = \frac{4.9\,(4h + h^2)}{h} = 4.9\,(4 + h) = 19.6 + 4.9\,h \;\text{ m/s}.

As hh gets smaller and smaller — from either side — this gets as close as we like to 19.619.6 m/s. That number is the stone's instantaneous speed at t=2t = 2: what a speedometer would read. On the graph, the segments become the tangent line. Making this idea precise is the starting point of calculus (see introductory calculus).

Average speed over a shrinking interval

The straight line's slope is the average speed between P and Q. Shrink h.

PQ
  • d = 4.9t²
  • segment through P and Q
  • d = 4.9t²: y = 4.9
  • segment through P and Q: y = −4.9
Formal mathematicsF

Rates of change in Lean

In Lean, a changing quantity is a function f : Rat → Rat, and the average rate of change is a definition — the slope of the segment between two points of the graph.

avgRateLean 4Formally verified
/-- The average rate of change of `f` between `a` and `b`: change in the quantity divided by
the change in time, `(f b − f a) / (b − a)`. It is the slope of the segment of the graph from
`(a, f a)` to `(b, f b)`. Meaningful only for `a ≠ b`; the theorems below assume that. -/
def avgRate (f : Rat → Rat) (a b : Rat) : Rat := (f b - f a) / (b - a)
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
change_eq_rate_mul_timeLean 4Proved here from basic factsFormally verified
/-- Change = average rate × elapsed time. On a distance–time graph: distance covered = average
speed × time taken. (This is the definition of `avgRate`, multiplied out.) -/
theorem change_eq_rate_mul_time (f : Rat → Rat) (a b : Rat) (h : a ≠ b) :
    f b - f a = avgRate f a b * (b - a) := by
  have hrun : b - a ≠ 0 := fun h0 => h (by grind)
  unfold avgRate
  exact (Rat.div_mul_cancel hrun).symm
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

A straight-line graph has the same rate everywhere, and a horizontal one has rate 00:

avg_rate_linearLean 4Proved here from basic factsFormally verified
/-- For a quantity changing at a constant rate, `f(t) = m·t + c`, the average rate of change
over **every** interval is `m`: the graph is a straight line of slope `m`. -/
theorem avg_rate_linear (m c a b : Rat) (h : a ≠ b) :
    avgRate (fun t => m * t + c) a b = m := by
  have hrun : b - a ≠ 0 := fun h0 => h (by grind)
  unfold avgRate
  rw [show m * b + c - (m * a + c) = m * (b - a) by grind]
  exact Rat.mul_div_cancel hrun
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
avg_rate_constLean 4Proved here from basic factsFormally verified
/-- A quantity that does not change has average rate of change `0` over every interval: a
horizontal graph. -/
theorem avg_rate_const (k a b : Rat) : avgRate (fun _ => k) a b = 0 := by
  unfold avgRate
  rw [Rat.sub_self, Rat.div_def, Rat.zero_mul]
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

What the sign of the rate tells us, proved exactly as in the human proof:

increasing_iff_avg_rate_posLean 4Proved here from basic factsFormally verified
/-- A graph is increasing (`y` gets larger whenever `x` gets larger) exactly when every average
rate of change is positive. For `x < y` the run `y − x` is positive, so the quotient
`(f y − f x)/(y − x)` is positive exactly when the rise `f y − f x` is (`Rat.lt_div_iff`). -/
theorem increasing_iff_avg_rate_pos (f : Rat → Rat) :
    (∀ x y, x < y → f x < f y) ↔ (∀ x y, x < y → 0 < avgRate f x y) := by
  have key : ∀ x y, x < y → (0 < avgRate f x y ↔ f x < f y) := by
    intro x y hxy
    have hrun : 0 < y - x := (Rat.lt_iff_sub_pos x y).mp hxy
    unfold avgRate
    rw [Rat.lt_div_iff hrun, Rat.zero_mul]
    exact (Rat.lt_iff_sub_pos (f x) (f y)).symm
  constructor
  · intro hinc x y hxy
    exact (key x y hxy).mpr (hinc x y hxy)
  · intro hpos x y hxy
    exact (key x y hxy).mp (hpos x y hxy)
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
constant_iff_avg_rate_zeroLean 4Proved here from basic factsFormally verified
/-- A quantity is constant exactly when its average rate of change is `0` over every interval:
"a horizontal graph means the quantity is not changing", and conversely. -/
theorem constant_iff_avg_rate_zero (f : Rat → Rat) :
    (∀ x y, f x = f y) ↔ (∀ x y, x < y → avgRate f x y = 0) := by
  constructor
  · intro hconst x y _
    unfold avgRate
    rw [hconst y x, Rat.sub_self, Rat.div_def, Rat.zero_mul]
  · intro hzero
    -- For `x < y`, change = rate × time = 0 × time = 0.
    have step : ∀ x y, x < y → f x = f y := by
      intro x y hxy
      have hch := change_eq_rate_mul_time f x y (Rat.ne_of_lt hxy)
      rw [hzero x y hxy, Rat.zero_mul] at hch
      grind
    intro x y
    rcases Rat.le_total (a := x) (b := y) with hxy | hyx
    · rcases Rat.le_iff_lt_or_eq.mp hxy with hlt | heq
      · exact step x y hlt
      · rw [heq]
    · rcases Rat.le_iff_lt_or_eq.mp hyx with hlt | heq
      · exact (step y x hlt).symm
      · rw [heq]
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

Combining intervals: the weighted average, and the theorem that the whole rate lies between the rates of the parts.

avg_rate_splitLean 4Proved here from basic factsFormally verified
/-- The average rate over a whole interval is a **weighted average** of the rates over its two
parts, weighted by their lengths:
`(c − a)·R(a, c) = (b − a)·R(a, b) + (c − b)·R(b, c)`.
Both sides equal the total change `f c − f a` (`change_eq_rate_mul_time`). -/
theorem avg_rate_split (f : Rat → Rat) (a b c : Rat) (hab : a ≠ b) (hbc : b ≠ c)
    (hac : a ≠ c) :
    (c - a) * avgRate f a c = (b - a) * avgRate f a b + (c - b) * avgRate f b c := by
  have h1 := change_eq_rate_mul_time f a c hac
  have h2 := change_eq_rate_mul_time f a b hab
  have h3 := change_eq_rate_mul_time f b c hbc
  grind
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
avg_rate_betweenLean 4Proved here from basic factsFormally verified
/-- The average speed over a whole journey lies between the average speeds of its two legs:
for `a < b < c`, if `R(a, b) ≤ R(b, c)` then `R(a, b) ≤ R(a, c) ≤ R(b, c)`.
Proof: in the weighted average `(c − a)·R(a, c) = (b − a)·R(a, b) + (c − b)·R(b, c)`, replace
the larger rate by the smaller one (or the smaller by the larger), then divide by `c − a > 0`. -/
theorem avg_rate_between (f : Rat → Rat) (a b c : Rat) (hab : a < b) (hbc : b < c)
    (hle : avgRate f a b ≤ avgRate f b c) :
    avgRate f a b ≤ avgRate f a c ∧ avgRate f a c ≤ avgRate f b c := by
  have hac : a < c := by grind
  have hsplit := avg_rate_split f a b c (Rat.ne_of_lt hab) (Rat.ne_of_lt hbc) (Rat.ne_of_lt hac)
  have h1 : 0 ≤ b - a := Rat.le_of_lt ((Rat.lt_iff_sub_pos a b).mp hab)
  have h2 : 0 ≤ c - b := Rat.le_of_lt ((Rat.lt_iff_sub_pos b c).mp hbc)
  have h3 : 0 < c - a := (Rat.lt_iff_sub_pos a c).mp hac
  -- Replace one rate by the other, in each term of the weighted average.
  have low : (c - b) * avgRate f a b ≤ (c - b) * avgRate f b c :=
    Rat.mul_le_mul_of_nonneg_left hle h2
  have high : (b - a) * avgRate f a b ≤ (b - a) * avgRate f b c :=
    Rat.mul_le_mul_of_nonneg_left hle h1
  constructor
  · apply Rat.le_of_mul_le_mul_left _ h3
    calc (c - a) * avgRate f a b
        = (b - a) * avgRate f a b + (c - b) * avgRate f a b := by grind
      _ ≤ (b - a) * avgRate f a b + (c - b) * avgRate f b c := by grind
      _ = (c - a) * avgRate f a c := hsplit.symm
  · apply Rat.le_of_mul_le_mul_left _ h3
    calc (c - a) * avgRate f a c
        = (b - a) * avgRate f a b + (c - b) * avgRate f b c := hsplit
      _ ≤ (b - a) * avgRate f b c + (c - b) * avgRate f b c := by grind
      _ = (c - a) * avgRate f b c := by grind
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

Ana and Ben, as Lean functions, and the theorem that their averages agree while their journeys differ:

steadyLean 4Formally verified
/-- A steady runner: `5` metres every second, so `5t` metres after `t` seconds. -/
def steady (t : Rat) : Rat := 5 * t
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
sprinterLean 4Formally verified
/-- A runner who starts fast and tires: `7` m/s for the first `10` seconds, then `3` m/s. -/
def sprinter (t : Rat) : Rat := if t ≤ 10 then 7 * t else 70 + 3 * (t - 10)
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
same_average_different_journeysLean 4Proved here from basic factsFormally verified
/-- Same average rate, different behaviour: over the `20` seconds both runners average
`5` m/s (both cover `100` m), yet after `10` seconds one is at `50` m and the other at `70` m.
An average rate does not tell you what happens inside the interval. -/
theorem same_average_different_journeys :
    avgRate steady 0 20 = 5 ∧ avgRate sprinter 0 20 = 5 ∧ steady 10 ≠ sprinter 10 := by
  have h20 : ¬ ((20 : Rat) ≤ 10) := by decide
  have h0 : (0 : Rat) ≤ 10 := by decide
  have h10 : (10 : Rat) ≤ 10 := by decide
  refine ⟨?_, ?_, ?_⟩
  · unfold avgRate steady
    grind
  · unfold avgRate sprinter
    rw [ite_eq_right h20, ite_eq_left h0]
    grind
  · unfold steady sprinter
    rw [ite_eq_left h10]
    grind
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

And the round-trip surprise, in general and for the classic numbers:

round_trip_averageLean 4Proved here from basic factsFormally verified
/-- Going a distance `d` at speed `u` and coming back at speed `v`, the average speed is total
distance ÷ total time `= 2d / (d/u + d/v) = 2uv / (u + v)` — not `(u + v)/2`. (The distance
`d` cancels.) -/
theorem round_trip_average (d u v : Rat) (hd : 0 < d) (hu : 0 < u) (hv : 0 < v) :
    (d + d) / (d / u + d / v) = 2 * u * v / (u + v) := by
  have hd' : d ≠ 0 := Rat.ne_of_gt hd
  have hu' : u ≠ 0 := Rat.ne_of_gt hu
  have hv' : v ≠ 0 := Rat.ne_of_gt hv
  have huv : u + v ≠ 0 := Rat.ne_of_gt (by grind)
  grind
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
round_trip_exampleLean 4Proved here from basic factsFormally verified
/-- The classic puzzle: `60` km out at `30` km/h (2 hours) and `60` km back at `60` km/h
(1 hour) is `120` km in `3` hours — an average of `40` km/h, not `45`. -/
theorem round_trip_example : (60 + 60 : Rat) / (60 / 30 + 60 / 60) = 40 := by
  grind
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor
round_trip_le_meanLean 4Proved here from basic factsFormally verified
/-- The round-trip average speed is never more than the mean of the two speeds:
`2uv/(u + v) ≤ (u + v)/2`. The difference is `(u − v)² / (2(u + v))`, and a square is never
negative; equality holds only when `u = v`. -/
theorem round_trip_le_mean (u v : Rat) (hu : 0 < u) (hv : 0 < v) :
    2 * u * v / (u + v) ≤ (u + v) / 2 := by
  have hpos : 0 < u + v := by grind
  have huv : u + v ≠ 0 := Rat.ne_of_gt hpos
  -- A square is never negative.
  have hsq : 0 ≤ (u - v) * (u - v) := by
    rcases Rat.le_total (a := 0) (b := u - v) with h | h
    · exact Rat.mul_nonneg h h
    · have h' : 0 ≤ -(u - v) := by grind
      have := Rat.mul_nonneg h' h'
      rw [Rat.neg_mul, Rat.mul_neg, Rat.neg_neg] at this
      exact this
  have hinv : 0 ≤ (2 * (u + v))⁻¹ := Rat.le_of_lt (Rat.inv_pos.mpr (by grind))
  have hdiff : (u + v) / 2 - 2 * u * v / (u + v) = (u - v) * (u - v) * (2 * (u + v))⁻¹ := by
    grind
  have hnonneg : 0 ≤ (u + v) / 2 - 2 * u * v / (u + v) := by
    rw [hdiff]
    exact Rat.mul_nonneg hsq hinv
  exact (Rat.le_iff_sub_nonneg _ _).mpr hnonneg
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/GraphsOfChange.leanTry it in the Lean web editor

What is formalised: every theorem in the "What rates of change can tell us" section, for quantities whose values are rational numbers. What is not formalised here: the instantaneous speed. Limits need the real numbers, which live in Mathlib rather than core Lean; there, the mean value theorem (exists_deriv_eq_slope) says that a smoothly changing quantity reaches its average rate of change as an instantaneous rate at some moment.

ComputationC

Rates by computer

A journey graph: segment rates, averages and round tripsPythonExact computationComputationally tested
"""Reading a distance-time graph by computer: rates, averages and a trap.

A cyclist's trip to market and back is given as a table of (time, distance
from home). The experiment computes the average rate of change on each
segment of the graph and says whether the distance is increasing, constant or
decreasing there; checks that the rate over a longer stretch is the
length-weighted average of the rates of its pieces; contrasts the average
rate of change of distance-from-home (zero for a round trip) with the
average speed; and computes round-trip average speeds, which are never more
than the mean of the two speeds. All arithmetic is exact (fractions).
"""

from fractions import Fraction as F

#: (minutes since leaving home, km from home): to market 6 km away and back
JOURNEY = [(0, 0), (20, 4), (25, 4), (35, 6), (55, 6), (75, 0)]

def avg_rate(p, q):
    """Average rate of change between points p = (a, f(a)) and q = (b, f(b))."""
    (a, fa), (b, fb) = p, q
    if a == b:
        raise ValueError("the two times must differ")
    return F(fb - fa, b - a)

def describe(rate):
    """Word for the behaviour of a segment with the given rate."""
    if rate > 0:
        return "increasing (moving away)"
    if rate < 0:
        return "decreasing (coming back)"
    return "constant (stopped)"

def segment_rates(points):
    """Rates on consecutive segments, as (start, end, rate) triples."""
    return [(p[0], q[0], avg_rate(p, q)) for p, q in zip(points, points[1:])]

def weighted_average_holds(points, i, j, k):
    """Check (t_k - t_i) R(i, k) == (t_j - t_i) R(i, j) + (t_k - t_j) R(j, k)."""
    pi, pj, pk = points[i], points[j], points[k]
    whole = (pk[0] - pi[0]) * avg_rate(pi, pk)
    parts = (pj[0] - pi[0]) * avg_rate(pi, pj) + (pk[0] - pj[0]) * avg_rate(pj, pk)
    return whole == parts

def distance_ridden(points):
    """Total distance travelled: the sum of the sizes of all the changes."""
    return sum(abs(q[1] - p[1]) for p, q in zip(points, points[1:]))

def round_trip_speed(u, v):
    """Average speed for equal distances at speeds u and v: 2uv / (u + v)."""
    if u <= 0 or v <= 0:
        raise ValueError("speeds must be positive")
    return F(2 * u * v, u + v)

def main():
    print("1. Segments of the journey (rates in km/h = 60 x km per minute)")
    for start, end, rate in segment_rates(JOURNEY):
        kmh = 60 * rate
        print(f"   {start:>2}-{end:>2} min: {str(kmh):>4} km/h  {describe(rate)}")
    print()
    print("2. Combining intervals: the rate over 0-35 min is the length-weighted")
    print("   average of the rates on its pieces 0-20, 20-25 and 25-35:")
    r = 60 * avg_rate(JOURNEY[0], JOURNEY[3])
    print(f"   (20 x 12 + 5 x 0 + 10 x 12) / 35 = {r} = {float(r):.2f} km/h")
    triples = [(i, j, k) for i in range(len(JOURNEY))
               for j in range(i + 1, len(JOURNEY))
               for k in range(j + 1, len(JOURNEY))]
    ok = all(weighted_average_holds(JOURNEY, *t) for t in triples)
    print(f"   rule checked for all {len(triples)} triples of table times: {ok}")
    print()
    whole = avg_rate(JOURNEY[0], JOURNEY[-1])
    ridden = distance_ridden(JOURNEY)
    hours = F(JOURNEY[-1][0], 60)
    print("3. The whole trip, 0-75 min:")
    print(f"   average rate of change of distance from home: {whole} km/h")
    print(f"   distance actually ridden: {ridden} km in {hours} h,")
    speed = ridden / hours
    print(f"   so the average speed is {speed} = {float(speed):.1f} km/h")
    print()
    print("4. Round trips, equal distances at speeds u and v (km/h):")
    for u, v in [(30, 60), (10, 20), (12, 18), (40, 40)]:
        avg = round_trip_speed(u, v)
        print(f"   u = {u:>2}, v = {v:>2}: average {str(avg):>5}"
              f" = {float(avg):5.2f}, mean of speeds {F(u + v, 2)}")
    print()
    print("Epistemic status: exact rational arithmetic (decimals are rounded for")
    print("display) on one made-up journey and four pairs of speeds. The lesson")
    print("proves the general facts: the weighted-average rule, and that a round")
    print("trip's average speed is never more than the mean of the two speeds")
    print("(equal only when the speeds are equal).")

if __name__ == "__main__":
    main()
Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Then the falling stone, with exact fractions: its average speed second by second, and over the shrinking intervals from 22 to 2+h2 + h.

A falling stone: average speeds over shrinking intervalsPythonExact computationComputationally tested
"""A curved graph: average speeds of a falling stone over shrinking intervals.

In the idealised model of a stone dropped from rest (no air resistance), it
has fallen d(t) = 4.9 t^2 metres after t seconds. Its distance-time graph is
curved, so the average rate of change depends on the interval. The
experiment computes, with exact fractions, the average speed in each of the
first four seconds, then the average speed over intervals [2, 2 + h] for
shrinking h (and for intervals ending at 2), and compares the results with
the exact formula 19.6 + 4.9h proved in the lesson. As h shrinks the average
speeds approach 19.6 m/s: a preview of the instantaneous speed (derivative).
"""

from fractions import Fraction as F

G_HALF = F(49, 10)  # 4.9 m/s^2, half the acceleration due to gravity

def fallen(t):
    """Distance fallen after t seconds in the model d(t) = 4.9 t^2."""
    return G_HALF * F(t) ** 2

def avg_speed(a, b):
    """Average rate of change of d between times a and b (a != b)."""
    if a == b:
        raise ValueError("the two times must differ")
    return (fallen(b) - fallen(a)) / (F(b) - F(a))

def formula(h):
    """The lesson's exact formula for the average speed over [2, 2 + h]."""
    return F(98, 5) + G_HALF * F(h)

def show(x):
    """A fraction with a decimal beside it, e.g. '1029/50 (= 20.58)'."""
    x = F(x)
    if x.denominator == 1:
        return str(x)
    return f"{x} (= {float(x):.4f})"

def main():
    print("1. Second by second (exact values; all are whole tenths)")
    for t in range(1, 5):
        print(f"   after {t} s: fallen {float(fallen(t)):5.1f} m;"
              f" average speed during second {t}:"
              f" {float(avg_speed(t - 1, t)):4.1f} m/s")
    print("   The rate grows each second: a curved, steepening graph.")
    print()
    print("2. Average speed over the interval from t = 2 to t = 2 + h")
    hs = [F(1), F(1, 10), F(1, 100), F(1, 1000)]
    for h in hs + [-h for h in hs]:
        rate = avg_speed(2, 2 + h)
        mark = "matches" if rate == formula(h) else "DIFFERS"
        print(f"   h = {str(h):>7}: {show(rate):<26} {mark} 19.6 + 4.9h")
    print("   As h shrinks (from either side) the values close in on 19.6.")
    print()
    print("Epistemic status: exact arithmetic in an idealised model (no air")
    print("resistance). Each value agrees with the formula 19.6 + 4.9h, which")
    print("the lesson proves by algebra for every h other than 0; that formula,")
    print("not these eight values, shows the averages approach 19.6 m/s.")

if __name__ == "__main__":
    main()
Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Every average speed over [2,2+h][2, 2 + h] matches the formula 19.6+4.9h19.6 + 4.9h exactly. But eight values of hh cannot prove where the averages are heading; the algebra in the previous section does, because it gives the formula for every h≠0h \neq 0.

Explore

Explore: reading graphs

Keza's trip as a graph you can trace. Move the trace slider (or hover) to read her distance from home at any minute.

Keza's trip

Where is the graph steepest? Where is it flat?

  • distance from home (km)
  • distance from home (km): y = 0.2

Two towns, with populations in thousands, tt years after a census:

Bigger or faster?

Which town is larger? Which is growing faster? Are those the same question?

same size
  • town A: 50 + 2t
  • town B: 20 + 5t
  • town A: 50 + 2t: y = 52
  • town B: 20 + 5t: y = 25

Things to try:

  • On Keza's graph, find the times when she was 33 km from home. How many are there, and what was she doing at each?
  • On the towns graph: town B's line is steeper, so B is growing faster — but A is larger until year 1010. Steeper means faster change, not more.
  • On the falling-stone graph in the previous section, set h=0h = 0. What does the line become?
Exercises

Exercises

1. Graphs of change

Warm-upHuman

On the graph of Keza's trip (segments A–E in the lesson), during which segment was she riding fastest?

Choose one

2. Graphs of change

Warm-upHuman

A village water tank holds 12001200 litres at 8 a.m. and 300300 litres at 11 a.m. What is the average rate of change of the amount of water, in litres per hour?

3. Graphs of change

CoreHuman

A bamboo shoot in a garden in Kyoto is 4040 cm tall on day 00, 130130 cm on day 33 and 180180 cm on day 55. What is its average rate of growth from day 00 to day 55, in cm per day?

4. Graphs of change

CoreHuman

A cyclist rides slowly up a steep hill, then quickly down the other side, each at a steady speed. Which describes the graph of distance travelled against time?

Choose one

5. Graphs of change

CoreHuman

Over the same week, the graph of plant P's height is steeper than the graph of plant Q's height. Which statement must be true?

Choose one

6. Graphs of change

CoreHuman

A bus travels 9090 km at 4545 km/h and then returns the same 9090 km at 9090 km/h. What is its average speed for the whole round trip, in km/h?

7. Graphs of change

StretchHuman

Amira cycles for a while at an average of 1212 km/h, then for a while at an average of 2020 km/h (she spends some time on each leg). Which of these could be her average speed for the whole ride? (Choose all that apply.)

Choose all that apply

8. Graphs of change

CoreFormal

Which Lean statement says that f : Rat → Rat is increasing (y gets larger whenever x gets larger)?

Choose one

9. Graphs of change

CoreComputational

Write average_rates(points) for a list of points (x, y) with increasing xx-values. Return the list of average rates of change between consecutive points, as Fractions. For Keza's journey [(0, 0), (20, 4), (25, 4), (35, 6), (55, 6), (75, 0)] (minutes, km) it should return the rates in km per minute.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

10. Graphs of change

StretchHuman

In the model d(t)=4.9t2d(t) = 4.9t^2, the average speed of the falling stone over the interval from t=3t = 3 to t=3+ht = 3 + h (with h≠0h \neq 0) is …

Choose one
Common misconceptionsH

Common misconceptions

Misconception

"The graph is a picture of the journey." A distance–time graph that rises and falls is not a hill. Rising means moving away, falling means coming back, and a cyclist climbing a real hill slowly makes the graph rise gently. Always read the axes first.

Misconception

"Steeper means bigger." Steepness measures how fast a quantity changes, not how large it is. Town B's graph is steeper than town A's, but A has more people until year 1010.

Misconception

"The average speed of a round trip is the average of the two speeds." It is total distance divided by total time: 3030 km/h out and 6060 km/h back gives 4040 km/h, not 4545, because more time is spent at the slower speed.

Misconception

"An average rate of 00 means nothing changed." Keza's distance from home has average rate 00 over the whole trip, yet she rode 1212 km. The average only compares the start and the end.

Misconception

"A flat line always means stopped." On a distance–time graph, yes. On a speed–time graph, a flat line means moving at a constant speed. The same shape tells different stories on different axes.

ViewpointsH

Other ways of seeing

Physics— Velocity, and distance as area

In physics, the slope of a position–time graph is velocity (speed with a direction, so it can be negative), and the slope of a velocity–time graph is acceleration. The reverse also holds: the area under a velocity–time graph is the change in position. For the falling stone, the velocity grows steadily, v=9.8 tv = 9.8\,t; the area under that straight line from 00 to tt is a triangle, 12⋅t⋅9.8t=4.9 t2\tfrac{1}{2} \cdot t \cdot 9.8t = 4.9\,t^2 — exactly the distance fallen. Galileo found by experiment that distances fallen grow like the square of the time, and gave a geometric argument of this kind (Two New Sciences, 1638).

Analysis— Limits and the mean value theorem

The instantaneous rate of change — the limit of average rates over shrinking intervals — is the derivative, the central idea of calculus. A beautiful theorem connects the two kinds of rate. Mean value theorem: if a quantity yy depends continuously on xx for a≤x≤ba \leq x \leq b and has an instantaneous rate of change at every xx strictly between aa and bb, then at some moment cc between them the instantaneous rate equals the average rate R(a,b)R(a, b). If you drive 120120 km in 22 hours, at some instant your speedometer read exactly 6060 km/h. (The hypotheses matter: a graph with a jump or a corner can avoid its average slope.)

Geometry— Slope as direction

Geometrically, an average rate of change is the slope of a chord joining two points of a graph, and the instantaneous rate is the slope of the tangent line, the line that touches the curve at one point and points in the curve's direction there. A graph is straight exactly when all its chords have the same slope, and it curves upwards when the slopes of its chords increase as we move to the right — as for the falling stone, whose average speeds in successive seconds are 4.94.9, 14.714.7, 24.524.5, 34.334.3 m/s.

History & global context

History and global context

  • Babylonian astronomers, on clay tablets from between about 350 and 50 BCE, computed how far the planet Jupiter moves along the sky by a calculation that amounts to finding the area of a trapezium under a graph of its daily motion against time — an "area under a velocity–time graph", more than a millennium before such figures were drawn in Europe (as Mathieu Ossendrijver showed in 2016).
  • In India, Bhāskara II (12th century) distinguished a planet's average daily motion from its tātkālika gati, its motion at a particular instant — an early idea of instantaneous rate of change.
  • In 14th-century Europe, scholars at Merton College, Oxford, studied "uniformly difform" (steadily accelerating) motion, and Nicole Oresme in Paris drew such motion as a figure: time along a base line and speed as heights above it. With it he gave a geometric proof of the Merton "mean speed" rule: a steadily accelerating body covers the same distance as one moving the whole time at its middle speed.
  • Galileo Galilei's Two New Sciences (1638) used such figures to analyse falling bodies, and William Playfair's Commercial and Political Atlas (1786) popularised line graphs of quantities changing over time, such as a country's trade year by year.
Further reading

Further reading

  • Malcolm Swan and the Shell Centre for Mathematical Education, The Language of Functions and Graphs (1985) — the classic collection of activities on interpreting real-world graphs, including the "graph is not a picture" trap.
  • I. M. Gelfand, E. G. Glagoleva and E. E. Shnol, Functions and Graphs (English edition 1990) — how to read and sketch graphs, from a great teacher.
  • Edward R. Tufte, The Visual Display of Quantitative Information (1983) — on drawing graphs that tell the truth.
  • Mathieu Ossendrijver, "Ancient Babylonian astronomers calculated Jupiter's position from the area under a time-velocity graph", Science 351 (2016).