Sequence proof

Stream: new members

[Zhang]

Let ${a_n}$ be an arithmetic sequence with common difference $d$, and ${b_n}$ be a geometric sequence with common ratio $q$. Given that the summation of the first $n$ terms of ${a_n+b_n}$ is $S_n = n^2 - n + 2^n - 1$, show that $d + q$ is $4$.
Hint 1: Recall that a sequence is realized as type ℕ → ℝ, a function from natural numbers to real numbers, with indexing starting from $1$.
Hint 2: You are expected to use def to define arithmetic and geometric sequences.
Hint 3: Summation of a sequence can be defined using the ∑ notation.

[Ruben Van de Velde]

What is your question and what have you tried?

[Zhang]

import Mathlib
open Nat
open Real
open BigOperators

-- Define arithmetic sequence
def a_seq (n : ℕ) (a d : ℕ) : ℕ :=
a + (n - 1) * d

-- Define geometric sequence
def b_seq (n : ℕ) (b q : ℕ) : ℕ :=
b * q^(n - 1)

-- Define sum function S_n
def S_n (n : ℕ) : ℕ :=
n^2 - n + 2^n - 1

theorem sum_arithmetic (n : ℕ) (a d : ℕ) :
∑ i ∈ Finset.range n, (a + i * d) = n * a + (n * (n - 1) * d) / 2 := by
induction' n with k hk
· simp -- Base case: S_0 = 0

rw [Finset.sum_range_succ] -- Expand sum
rw [hk] -- Apply induction hypothesis
rw [add_comm ((k * (k - 1) * d) / 2) (a + k * d)]
rw [← add_assoc (k * a) a (k * d), ← add_mul]
rw [add_comm ((k * d) (k * (k - 1) * d) / 2) ]
have h_div : (k * (k - 1) * d) / 2 + k * d = ((k * (k - 1) + 2 * k) * d) / 2 := by
rw [← Nat.mul_add_div (by norm_num : 0 < 2)]
rw [mul_comm 2 k, ← add_mul]
rw [h_div]
-- Calculate k * (k - 1) + 2k = k * (k - 1 + 2) = k * (k + 1)
rw [Nat.add_sub_cancel]
rw [mul_comm k (k + 1)]
exact rfl

theorem sum_geometric (n : ℕ) (b q : ℕ) (h : q ≠ 1) :
∑ i ∈ Finset.range n, b * q^i = b * (1 - q^n) / (1 - q) :=
by
-- Handle the case when n = 0
cases n with k
· simp -- The case when n = 0 automatically holds (sum of zero terms)

-- Induction: start from n = 1
induction' k with k hk
· simp -- Handle the case when n = 1
rw [Finset.sum_range_succ] -- Split S_(k+1) = S_k + b * q^k
rw [hk] -- Induction hypothesis
rw [mul_sub, mul_one] -- Expand b * (1 - q^k)
rw [add_div (b * (1 - q^k)) (b * q^k) (1 - q)] -- Unify denominators
rw [← mul_add] -- Factor out b
rw [sub_add, add_sub_cancel]
exact rfl

[Zhang]

Not quite clear about how to modify the induction part. And still cofused about how to prove p+q=4

[Kevin Buzzard]

Can you read #backticks and then edit your message?

[Zhang]

import Mathlib
open Nat
open Real
open BigOperators

-- Define arithmetic sequence
def a_seq (n : ℕ) (a d : ℕ) : ℕ :=
a + (n - 1) * d

-- Define geometric sequence
def b_seq (n : ℕ) (b q : ℕ) : ℕ :=
b * q^(n - 1)

-- Define sum function S_n
def S_n (n : ℕ) : ℕ :=
n^2 - n + 2^n - 1

theorem sum_arithmetic (n : ℕ) (a d : ℕ) :
∑ i ∈ Finset.range n, (a + i * d) = n * a + (n * (n - 1) * d) / 2 := by
induction' n with k hk
· simp -- Base case: S_0 = 0

rw [Finset.sum_range_succ] -- Expand sum
rw [hk] -- Apply induction hypothesis
rw [add_comm ((k * (k - 1) * d) / 2) (a + k * d)]
rw [← add_assoc (k * a) a (k * d), ← add_mul]
rw [add_comm ((k * d) (k * (k - 1) * d) / 2) ]
have h_div : (k * (k - 1) * d) / 2 + k * d = ((k * (k - 1) + 2 * k) * d) / 2 := by
rw [← Nat.mul_add_div (by norm_num : 0 < 2)]
rw [mul_comm 2 k, ← add_mul]
rw [h_div]
-- Calculate k * (k - 1) + 2k = k * (k - 1 + 2) = k * (k + 1)
rw [Nat.add_sub_cancel]
rw [mul_comm k (k + 1)]
exact rfl

theorem sum_geometric (n : ℕ) (b q : ℕ) (h : q ≠ 1) :
∑ i ∈ Finset.range n, b * q^i = b * (1 - q^n) / (1 - q) :=
by
-- Handle the case when n = 0
cases n with k
· simp -- The case when n = 0 automatically holds (sum of zero terms)

-- Induction: start from n = 1
induction' k with k hk
· simp -- Handle the case when n = 1
rw [Finset.sum_range_succ] -- Split S_(k+1) = S_k + b * q^k
rw [hk] -- Induction hypothesis
rw [mul_sub, mul_one] -- Expand b * (1 - q^k)
rw [add_div (b * (1 - q^k)) (b * q^k) (1 - q)] -- Unify denominators
rw [← mul_add] -- Factor out b
rw [sub_add, add_sub_cancel]
exact rfl