Common.Real.Sequence.Arithmetic

A characterization of an arithmetic sequence, i.e. a sequence with a common difference between each term.

structure Real.Arithmetic : Type

A 0th-indexed arithmetic sequence.

• a₀ : ℝ
• Δ : ℝ

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

Returns the value of the nth term of an arithmetic sequence.

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

Equations

• Real.Arithmetic.termClosed seq n = seq.a₀ + seq.Δ * ↑n

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

Returns the value of the nth term of an arithmetic sequence.

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

Equations

• Real.Arithmetic.termRecursive x 0 = x.a₀
• Real.Arithmetic.termRecursive x (Nat.succ n) = x.Δ + Real.Arithmetic.termRecursive x n

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

The recursive and closed term definitions of an arithmetic sequence agree with one another.

theorem Real.Arithmetic.term_closed_sub_succ_delta {n : ℕ} {seq : Real.Arithmetic} : Real.Arithmetic.termClosed seq n = Real.Arithmetic.termClosed seq (n + 1) - seq.Δ

A term is equal to the next in the sequence minus the common difference.

noncomputable def Real.Arithmetic.sumClosed (seq : Real.Arithmetic) (n : ℕ) : ℝ

The summation of the first n + 1 terms of an arithmetic sequence.

This function calculates the sum directly.

Equations

• Real.Arithmetic.sumClosed seq n = (↑n + 1) * (seq.a₀ + Real.Arithmetic.termClosed seq n) / 2

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

The summation of the first n + 1 terms of an arithmetic sequence.

This function calculates the sum recursively.

Equations

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

theorem Real.Arithmetic.sum_recursive_closed (seq : Real.Arithmetic) (n : ℕ) : Real.Arithmetic.sumRecursive seq n = Real.Arithmetic.sumClosed seq n

The recursive and closed definitions of the sum of an arithmetic sequence agree with one another.