From c18b0e6f1de8d961a5a9cc29ff55b448b01de63d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 9 Apr 2023 08:11:27 -0600 Subject: [PATCH] Finish proving arithmetic/geometric sums. --- common/Common/Sequence/Arithmetic.lean | 52 +++++++++++++++++++++++--- common/Common/Sequence/Arithmetic.tex | 3 +- common/Common/Sequence/Geometric.lean | 27 ++++++++++--- common/Common/Sequence/Geometric.tex | 3 +- 4 files changed, 73 insertions(+), 12 deletions(-) diff --git a/common/Common/Sequence/Arithmetic.lean b/common/Common/Sequence/Arithmetic.lean index fdb73a1..fc91c32 100644 --- a/common/Common/Sequence/Arithmetic.lean +++ b/common/Common/Sequence/Arithmetic.lean @@ -38,7 +38,8 @@ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) : seq.termRecursive n = seq.termClosed n := by induction n with | zero => unfold termRecursive termClosed; norm_num - | succ n ih => calc + | succ n ih => + calc termRecursive seq (Nat.succ n) = seq.Δ + seq.termRecursive n := rfl _ = seq.Δ + seq.termClosed n := by rw [ih] @@ -47,13 +48,26 @@ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) _ = seq.a₀ + seq.Δ * ↑(n + 1) := by simp _ = termClosed seq (n + 1) := rfl +/-- +A term is equal to the next in the sequence minus the common difference. +-/ +theorem term_closed_sub_succ_delta {seq : Arithmetic} + : seq.termClosed n = seq.termClosed (n + 1) - seq.Δ := + calc + seq.termClosed n + _ = seq.a₀ + seq.Δ * n := rfl + _ = seq.a₀ + seq.Δ * n + seq.Δ - seq.Δ := by rw [add_sub_cancel] + _ = seq.a₀ + seq.Δ * (↑n + 1) - seq.Δ := by ring_nf + _ = seq.a₀ + seq.Δ * ↑(n + 1) - seq.Δ := by simp only [Nat.cast_add, Nat.cast_one] + _ = seq.termClosed (n + 1) - seq.Δ := rfl + /-- The summation of the first `n + 1` terms of an arithmetic sequence. This function calculates the sum directly. -/ noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real := - ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 + (n + 1) * (seq.a₀ + seq.termClosed n) / 2 /-- The summation of the first `n + 1` terms of an arithmetic sequence. @@ -61,15 +75,43 @@ The summation of the first `n + 1` terms of an arithmetic sequence. This function calculates the sum recursively. -/ def sum_recursive : Arithmetic → Nat → Real - | _, 0 => 0 + | seq, 0 => seq.a₀ | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n +/-- +Simplify a summation of terms found in the proof of `sum_recursive_closed`. +-/ +private lemma sub_delta_summand_eq_two_mul_a₀ {seq : Arithmetic} + : seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ = 2 * seq.a₀ := + calc + seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ + _ = seq.a₀ + (seq.a₀ + seq.Δ * ↑(n + 1)) - (n + 1) * seq.Δ := rfl + _ = seq.a₀ + seq.a₀ + seq.Δ * ↑(n + 1) - (n + 1) * seq.Δ := by rw [←add_assoc] + _ = seq.a₀ + seq.a₀ + seq.Δ * (n + 1) - (n + 1) * seq.Δ := by simp only [Nat.cast_add, Nat.cast_one] + _ = 2 * seq.a₀ := by ring_nf + /-- The recursive and closed definitions of the sum of an arithmetic sequence agree with one another. -/ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat) - : sum_recursive seq n = sum_closed seq n := - sorry + : seq.sum_recursive n = seq.sum_closed n := by + induction n with + | zero => + unfold sum_recursive sum_closed termClosed + norm_num + | succ n ih => + calc + seq.sum_recursive (n + 1) + _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl + _ = seq.termClosed (n + 1) + seq.sum_closed n := by rw [ih] + _ = seq.termClosed (n + 1) + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 := rfl + _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed n + seq.a₀ + seq.termClosed n) / 2 := by ring_nf + _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * (seq.termClosed (n + 1) - seq.Δ) + seq.a₀ + (seq.termClosed (n + 1) - seq.Δ)) / 2 := by rw [@term_closed_sub_succ_delta n] + _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + (seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ)) / 2 := by ring_nf + _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + 2 * seq.a₀) / 2 := by rw [sub_delta_summand_eq_two_mul_a₀] + _ = ((n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by ring_nf + _ = (↑(n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by simp only [Nat.cast_add, Nat.cast_one] + _ = seq.sum_closed (n + 1) := rfl end Arithmetic diff --git a/common/Common/Sequence/Arithmetic.tex b/common/Common/Sequence/Arithmetic.tex index fe790dc..e8d6223 100644 --- a/common/Common/Sequence/Arithmetic.tex +++ b/common/Common/Sequence/Arithmetic.tex @@ -1,5 +1,6 @@ \documentclass{article} \usepackage{amsfonts, amsthm} +\usepackage{hyperref} \newtheorem{theorem}{Theorem} @@ -15,7 +16,7 @@ $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ \begin{proof} -Common.Sequence.Arithmetic.sum\_recursive\_closed +\href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum\_recursive\_closed} \end{proof} diff --git a/common/Common/Sequence/Geometric.lean b/common/Common/Sequence/Geometric.lean index d810360..09a6c04 100644 --- a/common/Common/Sequence/Geometric.lean +++ b/common/Common/Sequence/Geometric.lean @@ -61,15 +61,32 @@ The summation of the first `n + 1` terms of a geometric sequence. This function calculates the sum recursively. -/ def sum_recursive : Geometric → Nat → Real - | _, 0 => 0 - | seq, (n + 1) => seq.termClosed n + seq.sum_recursive n + | seq, 0 => seq.a₀ + | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n /-- -The recursive and closed definitions of the sum of an arithmetic sequence agree +The recursive and closed definitions of the sum of a geometric sequence agree with one another. -/ theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1) - : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := - sorry + : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by + have h : 1 - seq.r ≠ 0 := by + intro h + rw [sub_eq_iff_eq_add, zero_add] at h + exact False.elim (p (Eq.symm h)) + induction n with + | zero => + unfold sum_recursive sum_closed_ratio_neq_one + simp + rw [mul_div_assoc, div_self h, mul_one] + | succ n ih => + calc + sum_recursive seq (n + 1) + _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl + _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih] + _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl + _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h] + _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf + _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl end Geometric diff --git a/common/Common/Sequence/Geometric.tex b/common/Common/Sequence/Geometric.tex index b4e5c12..5aea705 100644 --- a/common/Common/Sequence/Geometric.tex +++ b/common/Common/Sequence/Geometric.tex @@ -1,5 +1,6 @@ \documentclass{article} \usepackage{amsfonts, amsthm} +\usepackage{hyperref} \newtheorem{theorem}{Theorem} @@ -15,7 +16,7 @@ $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ \begin{proof} -Common.Sequence.Geometric.sum\_recursive\_closed. +\href{Geometric.lean}{Common.Sequence.Geometric.sum\_recursive\_closed} \end{proof}