arithGeom — Mathlib

English

Definition: For a ring with multiplication and addition, the sequence (u_n) is defined by u_0 = u_0 and u_{n+1} = a u_n + b.

Русский

Определение: в кольце с умножением и сложением последовательность (u_n) задаётся: u_0 = u_0 и u_{n+1} = a u_n + b.

LaTeX

$$$(\mathrm{arithGeom}(a,b,u_0))(0) = u_0 \land (\forall n \in \mathbb{N})\; (\mathrm{arithGeom}(a,b,u_0))(n+1) = a\, (\mathrm{arithGeom}(a,b,u_0))(n) + b$$$

Lean4

/-- Arithmetic-geometric sequence with starting value `u₀` and recurrence relation
`u (n + 1) = a * u n + b`. -/
def arithGeom [Mul R] [Add R] (a b u₀ : R) : ℕ → R
  | 0 => u₀
  | n + 1 => a * arithGeom a b u₀ n + b

Похожие утверждения