English
If the nth partial denominator is nonzero, then g.convs(n+1) equals (squashGCF g n).convs n.
Русский
Если n-ая частичная знаменатель не равен нулю, то g.convs(n+1) = (squashGCF g n).convs n.
LaTeX
$$$$g.convs(n+1) = (\text{squashGCF}(g,n)).convs(n), \; \text{при } g.partDens.get? n \neq 0.$$$$
Lean4
/-- The convergents coincide in the expected way at the squashed position if the partial denominator
at the squashed position is not zero. -/
theorem succ_nth_conv_eq_squashGCF_nth_conv [Field K]
(nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0) : g.convs (n + 1) = (squashGCF g n).convs n :=
by
rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n
· have : squashGCF g n = g := squashGCF_eq_self_of_terminated terminatedAt_n
simp only [this, convs_stable_of_terminated n.le_succ terminatedAt_n]
· obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n := Option.ne_none_iff_exists'.mp not_terminatedAt_n
have b_ne_zero : b ≠ 0 := nth_partDen_ne_zero (partDen_eq_s_b s_nth_eq)
cases n with
|
zero =>
suffices (b * g.h + a) / b = g.h + a / b by
simpa [squashGCF, s_nth_eq, conv_eq_conts_a_div_conts_b,
conts_recurrenceAux s_nth_eq zeroth_contAux_eq_one_zero first_contAux_eq_h_one]
grind
| succ
n' =>
obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' := g.s.ge_stable n'.le_succ s_nth_eq
let g' := squashGCF g (n' + 1)
set pred_conts := g.contsAux (n' + 1) with succ_n'th_contsAux_eq
set ppred_conts := g.contsAux n' with n'th_contsAux_eq
let pA := pred_conts.a
let pB := pred_conts.b
let ppA := ppred_conts.a
let ppB := ppred_conts.b
set pred_conts' := g'.contsAux (n' + 1) with succ_n'th_contsAux_eq'
set ppred_conts' := g'.contsAux n' with n'th_contsAux_eq'
let pA' := pred_conts'.a
let pB' := pred_conts'.b
let ppA' := ppred_conts'.a
let ppB' := ppred_conts'.b
have : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') :=
by
have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ := squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
rw [conv_eq_conts_a_div_conts_b, conts_recurrenceAux this n'th_contsAux_eq'.symm succ_n'th_contsAux_eq'.symm]
rw [this]
-- then compute the convergent of the original gcf by recursively unfolding the continuants
-- computation twice
have : g.convs (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
-- use the recurrence once
have : g.contsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
contsAux_recurrence s_n'th_eq n'th_contsAux_eq.symm succ_n'th_contsAux_eq.symm
rw [conv_eq_conts_a_div_conts_b, conts_recurrenceAux s_nth_eq succ_n'th_contsAux_eq.symm this]
rw [this]
suffices
((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
(b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
by
obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
simp [*, g', pA, pB, ppA, ppB, pA', pB', ppA', ppB',
(contsAux_eq_contsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
(contsAux_eq_contsAux_squashGCF_of_le n'.le_succ).symm]
symm
simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]
grind
