English
For a SimpContFract with indices under mild hypotheses, a classic two-by-two determinant identity holds between consecutive contsAux terms: A_n B_{n+1} - B_n A_{n+1} equals (-1)^n.
Русский
Для простого континфракта при разумных предпосылках выполняется классическое детерминантное тождество между соседними contsAux: A_n B_{n+1} - B_n A_{n+1} = (-1)^n.
LaTeX
$$$$A_n B_{n+1} - B_n A_{n+1} = (-1)^n.$$$$
Lean4
theorem determinant_aux (hyp : n = 0 ∨ ¬(↑s : GenContFract K).TerminatedAt (n - 1)) :
((↑s : GenContFract K).contsAux n).a * ((↑s : GenContFract K).contsAux (n + 1)).b -
((↑s : GenContFract K).contsAux n).b * ((↑s : GenContFract K).contsAux (n + 1)).a =
(-1) ^ n :=
by
induction n with
| zero => simp [contsAux]
| succ n IH =>
-- set up some shorthand notation
let g := (↑s : GenContFract K)
let conts := contsAux g (n + 2)
set pred_conts := contsAux g (n + 1) with pred_conts_eq
set ppred_conts := contsAux g n with ppred_conts_eq
let pA := pred_conts.a
let pB := pred_conts.b
let ppA := ppred_conts.a
let ppB := ppred_conts.b
change pA * conts.b - pB * conts.a = (-1) ^ (n + 1)
have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp := Option.ne_none_iff_exists'.1 not_terminated_at_n
suffices pA * (ppB + gp.b * pB) - pB * (ppA + gp.b * pA) = (-1) ^ (n + 1)
by
simp only [conts, contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
have gp_a_eq_one : gp.a = 1 := s.property _ _ (partNum_eq_s_a s_nth_eq)
rw [gp_a_eq_one, this.symm]
ring
suffices ppA * pB - ppB * pA = (-1) ^ n by grind
exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n
