English
Define the exact value approximated by a continued fraction: if the fractional part fr = 0, the exact value is conts.a/conts.b; otherwise it is the a/b of the nextConts constructed from fr⁻¹, pconts, and conts.
Русский
Определим точное значение аппроксимации непрерывной дробью: если дробная часть fr = 0, то точное значение = conts.a/conts.b; иначе — значение следующей пары conts, построенной из fr⁻¹, предшествующих и текущих частей.
LaTeX
$$$\\\\forall {K} [Field K] [LinearOrder K] [FloorRing K] (pconts conts : GenContFract.Pair K) (fr : K),\n GenContFract.compExactValue pconts conts fr = \\\\begin{cases} conts.a/conts.b, & fr = 0 \\\\text{else } (nextConts 1 fr^{-1} pconts conts).a / (nextConts 1 fr^{-1} pconts conts).b \\\\end{cases}$$$
Lean4
/-- Given two continuants `pconts` and `conts` and a value `fr`, this function returns
- `conts.a / conts.b` if `fr = 0`
- `exactConts.a / exactConts.b` where `exactConts = nextConts 1 fr⁻¹ pconts conts`
otherwise.
This function can be used to compute the exact value approximated by a continued fraction
`GenContFract.of v` as described in lemma `compExactValue_correctness_of_stream_eq_some`.
-/
protected def compExactValue (pconts conts : Pair K) (fr : K) : K :=
-- if the fractional part is zero, we exactly approximated the value by the last continuants
if fr = 0 then conts.a / conts.b
else -- otherwise, we have to include the fractional part in a final continuants step.
let exactConts := nextConts 1 fr⁻¹ pconts conts
exactConts.a / exactConts.b
