Common.Real.Sequence.Geometric

A characterization of a geometric sequence, i.e. a sequence with a common ratio between each term.

structure Real.Geometric : Type

A 0th-indexed geometric sequence.

• a₀ : ℝ
• r : ℝ

def Real.Geometric.termClosed (seq : Real.Geometric) (n : ℕ) : ℝ

Returns the value of the nth term of a geometric sequence.

This function calculates the value of this term directly. Keep in mind the sequence is 0th-indexed.

Equations

• Real.Geometric.termClosed seq n = seq.a₀ * seq.r ^ n

def Real.Geometric.termRecursive : Real.Geometric → ℕ → ℝ

Returns the value of the nth term of a geometric sequence.

This function calculates the value of this term recursively. Keep in mind the sequence is 0th-indexed.

Equations

• Real.Geometric.termRecursive x 0 = x.a₀
• Real.Geometric.termRecursive x (Nat.succ n) = x.r * Real.Geometric.termRecursive x n

theorem Real.Geometric.term_recursive_closed (seq : Real.Geometric) (n : ℕ) : Real.Geometric.termRecursive seq n = Real.Geometric.termClosed seq n

The recursive and closed term definitions of a geometric sequence agree with one another.

noncomputable def Real.Geometric.sumClosed (seq : Real.Geometric) (n : ℕ) : seq.r ≠ 1 → ℝ

The summation of the first n + 1 terms of a geometric sequence.

This function calculates the sum directly.

Equations

• Real.Geometric.sumClosed seq n x = seq.a₀ * (1 - seq.r ^ (n + 1)) / (1 - seq.r)

def Real.Geometric.sumRecursive : Real.Geometric → ℕ → ℝ

The summation of the first n + 1 terms of a geometric sequence.

This function calculates the sum recursively.

Equations

• Real.Geometric.sumRecursive x 0 = x.a₀
• Real.Geometric.sumRecursive x (Nat.succ n) = Real.Geometric.termClosed x (n + 1) + Real.Geometric.sumRecursive x n

theorem Real.Geometric.sum_recursive_closed (seq : Real.Geometric) (n : ℕ) (p : seq.r ≠ 1) : Real.Geometric.sumRecursive seq n = Real.Geometric.sumClosed seq n p

The recursive and closed definitions of the sum of a geometric sequence agree with one another.