/-- The average rate of change of `f` between `a` and `b`: change in the quantity divided bythe 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)
change_eq_rate_mul_timetheoremProved here from basic factspropext, Classical.choice, Quot.sound
change_eq_rate_mul_timeLean 4Proved here from basic factsFormally verified
/-- Change = average rate × elapsed time. On a distance–time graph: distance covered = averagespeed × 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
avg_rate_lineartheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 changeover **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
avg_rate_consttheoremProved here from basic factspropext, Classical.choice, Quot.sound
avg_rate_constLean 4Proved here from basic factsFormally verified
/-- A quantity that does not change has average rate of change `0` over every interval: ahorizontal 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]
increasing_iff_avg_rate_postheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 averagerate 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)
constant_iff_avg_rate_zerotheoremProved here from basic factspropext, Classical.choice, Quot.sound
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]
avg_rate_splittheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 twoparts, 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
avg_rate_betweentheoremProved here from basic factspropext, Classical.choice, Quot.sound
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)`, replacethe 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
/-- 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)
same_average_different_journeystheoremProved here from basic factspropext, Classical.choice, Quot.sound
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
round_trip_averagetheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 totaldistance ÷ 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
round_trip_exampletheoremProved here from basic factspropext, Classical.choice, Quot.sound
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
round_trip_le_meantheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 nevernegative; 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
/-- A quantity that never changes has average rate of change `0`.Hint: `unfold avgRate`, then `k − k = 0` (`Rat.sub_self`), and `0 / x = 0 * x⁻¹ = 0`(`Rat.div_def`, `Rat.zero_mul`). -/theorem avg_rate_const (k a b : Rat) : avgRate (fun _ => k) a b = 0 := by sorry
Show the compiled solution
avg_rate_constLean 4Proved here from basic factsFormally verified
/-- A quantity that does not change has average rate of change `0` over every interval: ahorizontal 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]
/-- `60` km at `30` km/h and `60` km back at `60` km/h: the average speed is `40` km/h.Hint: first work out the two times by hand. Then `grind` can check the arithmetic withfractions. -/theorem round_trip_example : (60 + 60 : Rat) / (60 / 30 + 60 / 60) = 40 := by sorry
Show the compiled solution
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