arithGeom_succ

Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

URI: https://scilib.ai/kg/mathlib#arithGeom_succ

English

The recurrence relation for the next term is u_{n+1} = a u_n + b.

Русский

Рекуррентное соотношение следующего члена: u_{n+1} = a u_n + b.

LaTeX

$$$(\mathrm{arithGeom}(a,b,u_0))(n+1) = a\,(\mathrm{arithGeom}(a,b,u_0))(n) + b$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru