sqrtTwoAddSeries — Mathlib

English

The sequence sqrtTwoAddSeries x n is defined by sqrtTwoAddSeries(x,0) = x and sqrtTwoAddSeries(x,n+1) = √(2 + sqrtTwoAddSeries(x,n)).

Русский

Для данного x последовательность sqrtTwoAddSeries x n задаётся рекурсивно: sqrtTwoAddSeries(x,0) = x и sqrtTwoAddSeries(x,n+1) = √(2 + sqrtTwoAddSeries(x,n)).

LaTeX

$$$\\\\sqrtTwoAddSeries(x,n) = \\\\begin{cases} x, & n=0 \\\\\\\\ \\\\sqrt{2 + \\\\sqrtTwoAddSeries(x,n-1)}, & n>0 \\\\end{cases}$$$

Lean4

/-- the series `sqrtTwoAddSeries x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
  starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrtTwoAddSeries 0 n / 2`
-/
@[simp]
noncomputable def sqrtTwoAddSeries (x : ℝ) : ℕ → ℝ
  | 0 => x
  | n + 1 => √(2 + sqrtTwoAddSeries x n)

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