English
The convergents of a real ξ are defined recursively by convergent(ξ,0)=⌊ξ⌋ and convergent(ξ,n+1)=⌊ξ⌋ + convergent(fract ξ)^{-1}(n)^{-1}.
Русский
Сходимые дроби ξ определяются рекурсивно: конвергент(ξ,0)=⌊ξ⌋, конвергент(ξ,n+1)=⌊ξ⌋ + (конвергент( fract(ξ) ))^{-1}(n).
LaTeX
$$$$\\text{Convergent}(\\xi,0)=\\lfloor\\xi\\rfloor,\\qquad \\text{Convergent}(\\xi,n+1)=\\lfloor\\xi\\rfloor + (\\text{Convergent}(\\operatorname{fract}(\\xi))^{-1})(n)^{-1}. $$$$
Lean4
/-- We give a direct recursive definition of the convergents of the continued fraction
expansion of a real number `ξ`. The main reason for that is that we want to have the
convergents as rational numbers; the versions `(GenContFract.of ξ).convs` and
`(GenContFract.of ξ).convs'` always give something of the same type as `ξ`.
We can then also use dot notation `ξ.convergent n`.
Another minor reason is that this demonstrates that the proof
of Legendre's theorem does not need anything beyond this definition.
We provide a proof that this definition agrees with the other one;
see `Real.convs_eq_convergent`.
(Note that we use the fact that `1/0 = 0` here to make it work for rational `ξ`.) -/
noncomputable def convergent : ℝ → ℕ → ℚ
| ξ, 0 => ⌊ξ⌋
| ξ, n + 1 => ⌊ξ⌋ + (convergent (fract ξ)⁻¹ n)⁻¹
