# 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.

source
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`.

Equations

- arithGeom a b u₀ 0 = u₀
- arithGeom a b u₀ n.succ = a * arithGeom a b u₀ n + b

Instances For

source
@[simp]
theorem arithGeom_zero {R : Type u_1} {a b u₀ : R} [Mul R] [Add R] :
arithGeom a b u₀ 0 = u₀
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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
source
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₀)
source
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
source
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)))