Finish proving arithmetic/geometric sums.

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

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}
 

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

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}