fastFibAux — Mathlib

English

An auxiliary function computes the pair (F_n, F_{n+1}) by binary recursion.

Русский

Вспомогательная функция вычисляет пару (F_n, F_{n+1}) по двоичному представлению n.

LaTeX

$$fastFibAux(n) = (fib(n), fib(n+1))$$

Lean4

/-- Computes `(Nat.fib n, Nat.fib (n + 1))` using the binary representation of `n`.
Supports `Nat.fastFib`. -/
def fastFibAux : ℕ → ℕ × ℕ :=
  Nat.binaryRec (fib 0, fib 1) fun b _ p =>
    if b then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

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