English
The finite exact value of the nth convergent subtraction is given by a determinant-like expression involving the convergents and conts.
Русский
Точное выражение разности между v и n-й сходной даётся через детерминантную формулу, использующую конвергенты и conts.
LaTeX
$$$\\\\forall {K} {v} {n} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {ifp : GenContFract.IntFractPair K},\\n Eq (IntFractPair.stream v n) (Some ifp) \\Rightarrow \\text{имеется } g := GenContFract.of v;\\n Eq (g.convs n)\\n \\\\Rightarrow (v - g.convs n) = \\\\ldots$$$
Lean4
/-- This lemma follows from the finite correctness proof, the determinant equality, and
by simplifying the difference. -/
theorem sub_convs_eq {ifp : IntFractPair K} (stream_nth_eq : IntFractPair.stream v n = some ifp) :
let g := of v
let B := (g.contsAux (n + 1)).b
let pB := (g.contsAux n).b
v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) :=
by
-- set up some shorthand notation
let g := of v
let conts := g.contsAux (n + 1)
let pred_conts := g.contsAux n
have g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr :=
compExactValue_correctness_of_stream_eq_some stream_nth_eq
obtain (ifp_fr_eq_zero | ifp_fr_ne_zero) := eq_or_ne ifp.fr 0
· suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]
replace g_finite_correctness : v = g.convs n := by
simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using g_finite_correctness
exact sub_eq_zero.2 g_finite_correctness
· -- more shorthand notation
let A := conts.a
let B := conts.b
let pA := pred_conts.a
let pB := pred_conts.b
suffices v - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by
simpa [ifp_fr_ne_zero]
-- now we can unfold `g.compExactValue` to derive the following equality for `v`
replace g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) := by
simpa [GenContFract.compExactValue, ifp_fr_ne_zero, nextConts, nextNum, nextDen, add_comm] using
g_finite_correctness
suffices (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by
rwa [g_finite_correctness]
-- To continue, we need use the determinant equality. So let's derive the needed hypothesis.
have n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1) :=
by
rcases n with - | n'
· simp
· have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
have : ¬g.TerminatedAt n' := (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
exact Or.inr this
have determinant_eq : pA * B - pB * A = (-1) ^ n :=
(SimpContFract.of v).determinant_aux n_eq_zero_or_not_terminatedAt_pred_n
have pB_ineq : (fib n : K) ≤ pB :=
haveI : n ≤ 1 ∨ ¬g.TerminatedAt (n - 2) :=
by
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
· simp [n_eq_zero]
· exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n
fib_le_of_contsAux_b this
have B_ineq : (fib (n + 1) : K) ≤ B :=
haveI : n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2) :=
by
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
· simp [n_eq_zero, le_refl]
· exact Or.inr not_terminatedAt_pred_n
fib_le_of_contsAux_b this
have zero_lt_B : 0 < B := B_ineq.trans_lt' <| cast_pos.2 <| fib_pos.2 n.succ_pos
have : 0 ≤ pB := (cast_nonneg _).trans pB_ineq
have : 0 < ifp.fr := ifp_fr_ne_zero.lt_of_le' <| IntFractPair.nth_stream_fr_nonneg stream_nth_eq
have : pB + ifp.fr⁻¹ * B ≠ 0 := by positivity
grind
