Arithmetic-geometric sequences

An arithmetic-geometric sequence is a sequence defined by the recurrence relation u (n + 1) = a * u n + b.

Main definitions

• arithGeom a b u₀: arithmetic-geometric sequence with starting value u₀ and recurrence relation u (n + 1) = a * u n + b.

Main statements

• arithGeom_eq: for a ≠ 1, arithGeom a b u₀ n = a ^ n * (u₀ - (b / (1 - a))) + b / (1 - a)
• tendsto_arithGeom_atTop_of_one_lt: if 1 < a and b / (1 - a) < u₀, then arithGeom a b u₀ n tends to +∞ as n tends to +∞. tendsto_arithGeom_nhds_of_lt_one: if 0 ≤ a < 1, then arithGeom a b u₀ n tends to b / (1 - a) as n tends to +∞.
• arithGeom_strictMono: if 1 < a and b / (1 - a) < u₀, then arithGeom a b u₀ is strictly monotone.

def arithGeom {R : Type u_1} [Mul R] [Add R] (a b u₀ : R) : ℕ → R

Arithmetic-geometric sequence with starting value u₀ and recurrence relation u (n + 1) = a * u n + b.

@[simp]

theorem arithGeom_zero {R : Type u_1} {a b u₀ : R} [Mul R] [Add R] : arithGeom a b u₀ 0 = u₀

theorem arithGeom_succ {R : Type u_1} {a b u₀ : R} [Mul R] [Add R] (n : ℕ) : arithGeom a b u₀ (n + 1) = a * arithGeom a b u₀ n + b

theorem arithGeom_eq_add_sum {R : Type u_1} {a b u₀ : R} [CommSemiring R] (n : ℕ) : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k

theorem arithGeom_same_eq_sum {R : Type u_1} {a b : R} [CommSemiring R] (n : ℕ) : arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k

theorem arithGeom_zero_eq_sum {R : Type u_1} {a b : R} [CommSemiring R] (n : ℕ) : arithGeom a b 0 n = b * ∑ k ∈ Finset.range n, a ^ k

theorem arithGeom_eq {R : Type u_1} {a b u₀ : R} [Field R] (ha : a ≠ 1) (n : ℕ) : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)

theorem arithGeom_eq' {R : Type u_1} {a b u₀ : R} [Field R] (ha : a ≠ 1) : arithGeom a b u₀ = fun (n : ℕ) => a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)

theorem arithGeom_same_eq_mul_div' {R : Type u_1} {a b : R} [Field R] (ha : a ≠ 1) (n : ℕ) : arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)

theorem arithGeom_same_eq_mul_div {R : Type u_1} {a b : R} [Field R] (ha : a ≠ 1) (n : ℕ) : arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)

theorem arithGeom_zero_eq_mul_div' {R : Type u_1} {a b : R} [Field R] (ha : a ≠ 1) (n : ℕ) : arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

theorem arithGeom_zero_eq_mul_div {R : Type u_1} {a b : R} [Field R] (ha : a ≠ 1) (n : ℕ) : arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)

theorem div_lt_arithGeom {R : Type u_1} {a b u₀ : R} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (ha_pos : 0 < a) (ha_ne : a ≠ 1) (h0 : b / (1 - a) < u₀) (n : ℕ) : b / (1 - a) < arithGeom a b u₀ n

theorem arithGeom_strictMono {R : Type u_1} {a b u₀ : R} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (ha : 1 < a) (h0 : b / (1 - a) < u₀) : StrictMono (arithGeom a b u₀)

theorem tendsto_arithGeom_atTop_of_one_lt {R : Type u_1} {a b u₀ : R} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (ha : 1 < a) (h0 : b / (1 - a) < u₀) : Filter.Tendsto (arithGeom a b u₀) Filter.atTop Filter.atTop

theorem tendsto_arithGeom_nhds_of_lt_one {R : Type u_1} {a b u₀ : R} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] [TopologicalSpace R] [OrderTopology R] (ha_pos : 0 ≤ a) (ha : a < 1) : Filter.Tendsto (arithGeom a b u₀) Filter.atTop (nhds (b / (1 - a)))