The sum of a second-order linear recurrence

For a summable sequence d obeying d (r + 2) = D • d (r + 1) - S • d r, its sum σ satisfies the identity:

σ - D • σ + S • σ = d 0 + (d 1 - D • d 0).

The values lie in a Hausdorff topological additive group, and each fixed scalar acts additively and continuously. For a nonassociative ring acting on itself by left multiplication, this gives (1 - D + S) * σ = d 0 + (d 1 - D * d 0).

In an associative ring, this corresponds to evaluating the characteristic polynomial at 1 in the formal generating-function identity (1 - D x + S x²) ∑ d r xʳ = d 0 + (d 1 - D d 0) x, and it is how a local Euler factor (1 - a_p p^{-s} + c_p p^{-2s})⁻¹ is recovered from a prime-power recurrence for the coefficients of a Dirichlet series.

Main results

• HasSum.sub_smul_add_smul_eq_of_linearRec₂: the scalar-action identity.
• HasSum.one_sub_add_mul_eq_of_linearRec₂: the ring identity.

theorem HasSum.sub_smul_add_smul_eq_of_linearRec₂ {A : Type u_1} {M : Type u_2} [AddCommGroup M] [DistribSMul A M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul A M] [T2Space M] {D S : A} {σ : M} {d : ℕ → M} (h : HasSum d σ) (hd : ∀ (r : ℕ), d (r + 2) = D • d (r + 1) - S • d r) : σ - D • σ + S • σ = d 0 + (d 1 - D • d 0)

The sum of a second-order linear recurrence. If d has sum σ and obeys d (r + 2) = D • d (r + 1) - S • d r, then σ - D • σ + S • σ = d 0 + (d 1 - D • d 0).

theorem HasSum.one_sub_add_mul_eq_of_linearRec₂ {R : Type u_3} [NonAssocRing R] [TopologicalSpace R] [IsTopologicalAddGroup R] [ContinuousConstSMul R R] [T2Space R] {D S σ : R} {d : ℕ → R} (h : HasSum d σ) (hd : ∀ (r : ℕ), d (r + 2) = D * d (r + 1) - S * d r) : (1 - D + S) * σ = d 0 + (d 1 - D * d 0)

The sum of a second-order linear recurrence in a ring. If d has sum σ and obeys d (r + 2) = D * d (r + 1) - S * d r, then (1 - D + S) * σ = d 0 + (d 1 - D * d 0).