Vanishing second differences force an affine sequence
Provedeq_add_sub_mul_natCast_of_sub_two_mul_add_eq_zeroLet be a commutative ring, let be a natural number, and let be a sequence. Assume that the second differences of vanish in the range determined by , namely that for every natural number with ; note that this hypothesis is vacuous when . Then for every natural number with one has
where is understood via the canonical ring homomorphism . Thus on the initial segment the sequence is the arithmetic progression with initial term and common difference . The recurrence is stated in the shifted form with indices , , rather than , , , so that no truncated subtraction on occurs; the conclusion is asserted for all indices up to and including , one step beyond the last index at which the recurrence is assumed.
This is the elementary statement that solutions of the linear recurrence , whose characteristic polynomial is , are exactly the affine sequences — equivalently, that a discrete harmonic function on a path is affine. It is used in the analysis of divisors supported on the special fibre of a resolution of an singularity, where the condition of zero intersection with each exceptional component is precisely the vanishing of second differences; the consumer is MvPolynomial.CrossingQuotient.Resolution.exists_open_pullback_twist_iso_tensorUnit_of_degree_eq_zero.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false
theorem eq_add_sub_mul_natCast_of_sub_two_mul_add_eq_zero
{R : Type*} [CommRing R] (e : ℕ) (a : ℕ → R)
(h : ∀ k : ℕ, k + 1 < e → a k - 2 * a (k + 1) + a (k + 2) = 0)
(k : ℕ) (hk : k ≤ e) :
a k = a 0 + (a 1 - a 0) * k := by sorry