feat(Algebra/ContinuedFractions): generalize determinant formula to GenContFract (#37997)

Let $g$ be a `GenContFract K`.

In this PR I generalize the determinant formula for continued fractions from the simple continued fraction case
$$A_n B_{n+1} - B_n A_{n+1} = (-1)^n$$
to the generalized continued fraction product formula
$$A_n B_{n+1} - B_n A_{n+1} = (-a_0) (-a_1) \dots (-a_n)$$

- The `SimpContFract` version is still available unchanged, so this should avoid breaking existing users of the old API.
- The use of `0` as the default partial numerator in `(g.partNums.get? i).getD 0` allows product formulation that remains valid when the fraction is terminated.

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -366,8 +366,14 @@ theorem sub_convs_eq {ifp : IntFractPair K}
         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 determinant_eq : pA * B - pB * A = (-1) ^ n := by
+      match hn : n with
+      | 0 => subst n; simp [pA, pB, A, B, pred_conts, conts]
+      | n' + 1 =>
+        subst n
+        simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n
+        rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n
+        exact (SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_n
     -- now all we got to do is to rewrite this equality in our goal and re-arrange terms;
     -- however, for this, we first have to derive quite a few tedious inequalities.
     have pB_ineq : (fib n : K) ≤ pB :=

Mathlib/Algebra/ContinuedFractions/Determinant.lean

@@ -5,22 +5,16 @@ Authors: Kevin Kappelmann
 -/
 module
 
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
 public import Mathlib.Algebra.ContinuedFractions.TerminatedStable
 public import Mathlib.Tactic.Ring
 
 /-!
-# Determinant Formula for Simple Continued Fraction
+# Determinant Formula for Generalized Continued Fraction
 
-## Summary
-
-We derive the so-called *determinant formula* for `SimpContFract`:
-`Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`.
-
-## TODO
-
-Generalize this for `GenContFract` version:
-`Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ₊₁)`.
+We derive the so-called *determinant formula* for `GenContFract`:
+`Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ)`.
 
 ## References
 
@@ -32,19 +26,20 @@ public section
 
 open GenContFract
 
-namespace SimpContFract
+variable {K : Type*} [Field K]
+
+namespace GenContFract
 
-variable {K : Type*} [Field K] {s : SimpContFract K} {n : ℕ}
+variable {g : GenContFract K} {n : ℕ}
 
-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
+private theorem determinant_aux (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)) :
+    (g.contsAux n).a * (g.contsAux (n + 1)).b -
+      (g.contsAux n).b * (g.contsAux (n + 1)).a =
+        ∏ i ∈ Finset.range n, - (g.partNums.get? i).getD 0 := 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
@@ -53,23 +48,45 @@ theorem determinant_aux (hyp : n = 0 ∨ ¬(↑s : GenContFract K).TerminatedAt
     let ppA := ppred_conts.a
     let ppB := ppred_conts.b
     -- let's change the goal to something more readable
-    change pA * conts.b - pB * conts.a = (-1) ^ (n + 1)
+    change pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
     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
     -- unfold the recurrence relation for `conts` once and simplify to derive the following
-    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]
+    suffices ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, - (g.partNums.get? i).getD 0 by
+      rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
+      subst conts
+      rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
       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
 
-/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`. -/
+/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ)`. -/
+theorem determinant :
+    g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) =
+      ∏ i ∈ Finset.range (n + 1), - (g.partNums.get? i).getD 0 := by
+  rcases em <| TerminatedAt g n with terminatedAt_n | not_terminatedAt_n
+  · rw [dens_stable_of_terminated n.le_succ terminatedAt_n,
+      nums_stable_of_terminated n.le_succ terminatedAt_n, Finset.prod_range_succ,
+      partNum_none_iff_s_none.mpr terminatedAt_n]
+    grind
+  · exact determinant_aux <| Or.inr <| not_terminatedAt_n
+end GenContFract
+
+namespace SimpContFract
+
+variable {s : SimpContFract K} {n : ℕ}
+
+/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1) ^ (n + 1)` for `SimpContFract`. -/
 theorem determinant (not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n) :
     (↑s : GenContFract K).nums n * (↑s : GenContFract K).dens (n + 1) -
-      (↑s : GenContFract K).dens n * (↑s : GenContFract K).nums (n + 1) = (-1) ^ (n + 1) :=
-  determinant_aux <| Or.inr <| not_terminatedAt_n
+      (↑s : GenContFract K).dens n * (↑s : GenContFract K).nums (n + 1) = (-1) ^ (n + 1) := calc
+  _ = ∏ i ∈ Finset.range (n + 1), - ((↑s : GenContFract K).partNums.get? i).getD 0 :=
+    (↑s : GenContFract K).determinant
+  _ = ∏ i ∈ Finset.range (n + 1), -1 := Finset.prod_congr rfl fun i hi ↦ by
+    rw [Finset.mem_range] at hi
+    obtain ⟨gp, s_ith_eq⟩ : ∃ gp, (↑s : GenContFract K).s.get? i = some gp :=
+      Option.ne_none_iff_exists'.1 <| mt (terminated_stable <| Nat.le_of_succ_le_succ hi) ‹_›
+    rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]
+  _ = (-1) ^ (n + 1) := by rw [Finset.prod_const, Finset.card_range]
 
 end SimpContFract