arithGeom_eq' — Mathlib

English

In the same setting, arithGeom a b u0 corresponds to the function n ↦ a^n (u0 - b/(1-a)) + b/(1-a).

Русский

В той же настройке arithGeom(a,b,u0) задаёт функцию n ↦ a^n (u0 - b/(1-a)) + b/(1-a).

LaTeX

$$$\\mathrm{arithGeom}(a,b,u_0) = \\; n \\mapsto a^n\\left(u_0 - \\dfrac{b}{\,1-a\}\\right) + \\dfrac{b}{\,1-a\}$$$

Lean4

theorem arithGeom_eq' (ha : a ≠ 1) : arithGeom a b u₀ = fun n ↦ a ^ n * (u₀ - (b / (1 - a))) + b / (1 - a) :=
  by
  ext
  exact arithGeom_eq ha _

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