:: Simple Continued Fractions and Their Convergents :: by Bo Li , Yan Zhang and Artur Korni{\l}owicz :: :: Received August 18, 2006 :: Copyright (c) 2006-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, INT_1, XREAL_0, ORDINAL1, RAT_1, XCMPLX_0, FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, SUBSET_1, SEQ_1, FUNCOP_1, TARSKI, IRRAT_1, REAL_1, INT_2, FIB_NUM, NEWTON, SQUARE_1, COMPLEX1, POWER, VALUED_1, REAL_3, FUNCT_7; notations TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, VALUED_0, XCMPLX_0, COMPLEX1, REAL_1, XXREAL_0, XREAL_0, RAT_1, SQUARE_1, INT_1, NAT_D, RELAT_1, RELSET_1, FUNCOP_1, VALUED_1, SEQ_1, FUNCT_2, NEWTON, NAT_1, FIB_NUM, POWER, IRRAT_1; constructors REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, POWER, FUNCOP_1, BINARITH, FIB_NUM, VALUED_1, PARTFUN1, RELSET_1, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, VALUED_0, VALUED_1, FUNCT_2; requirements BOOLE, REAL, SUBSET, NUMERALS, ARITHM; begin :: Preliminaries reserve a, b, k, n, m for Nat, i for Integer, r for Real, p for Rational, c for Complex, x for object, f for Function; registration let n; cluster n div 0 -> zero; cluster n mod 0 -> zero; cluster 0 div n -> zero; cluster 0 mod n -> zero; end; registration let c; cluster c-c -> zero; cluster c/0 -> zero; end; registration cluster [\ 0 /] -> zero; end; theorem :: REAL_3:1 0 < r & r < 1 implies 1 < 1/r; theorem :: REAL_3:2 i <= r & r < i+1 implies [\ r /] = i; theorem :: REAL_3:3 [\ m/n /] = m div n; theorem :: REAL_3:4 m mod n = 0 implies m / n = m div n; theorem :: REAL_3:5 m / n = m div n implies m mod n = 0; theorem :: REAL_3:6 frac(m/n) = (m mod n) / n; theorem :: REAL_3:7 p >= 0 implies ex m,n being Nat st n <> 0 & p = m/n; registration cluster INT-valued for Real_Sequence; end; definition mode Integer_Sequence is INT-valued Real_Sequence; end; theorem :: REAL_3:8 f is Integer_Sequence iff dom f=NAT & for x st x in NAT holds f.x is integer; theorem :: REAL_3:9 f is sequence of INT iff f is Integer_Sequence; theorem :: REAL_3:10 f is sequence of NAT iff dom f=NAT & for x st x in NAT holds f.x is natural; theorem :: REAL_3:11 f is sequence of NAT iff f is sequence of NAT; begin :: On the Euclidean algorithm definition let m, n be Nat; func modSeq(m,n) -> sequence of NAT means :: REAL_3:def 1 it.0 = m mod n & it.1 = n mod (m mod n) & for k being Nat holds it.(k+2) = it.k mod it.(k+1); end; definition let m, n be Nat; func divSeq(m,n) -> sequence of NAT means :: REAL_3:def 2 it.0 = m div n & it.1 = n div (m mod n) & for k being Nat holds it.(k+2) = modSeq(m,n).k div modSeq(m,n). (k+1); end; theorem :: REAL_3:12 divSeq(m,n).1 = n div modSeq(m,n).0; theorem :: REAL_3:13 modSeq(m,n).1 = n mod modSeq(m,n).0; theorem :: REAL_3:14 a <= b & modSeq(m,n).a = 0 implies modSeq(m,n).b = 0; theorem :: REAL_3:15 a < b implies modSeq(m,n).a > modSeq(m,n).b or modSeq(m,n).a = 0; theorem :: REAL_3:16 divSeq(m,n).(a+1) = 0 implies modSeq(m,n).a = 0; theorem :: REAL_3:17 a <> 0 & a <= b & divSeq(m,n).a = 0 implies divSeq(m,n).b = 0; theorem :: REAL_3:18 a < b & modSeq(m,n).a = 0 implies divSeq(m,n).b = 0; theorem :: REAL_3:19 n <> 0 implies m = divSeq(m,n).0 * n + modSeq(m,n).0; theorem :: REAL_3:20 n <> 0 implies m / n = divSeq(m,n).0 + 1 / (n / modSeq(m,n).0); theorem :: REAL_3:21 divSeq(m,0) = NAT --> 0; theorem :: REAL_3:22 modSeq(m,0) = NAT --> 0; theorem :: REAL_3:23 divSeq(0,n) = NAT --> 0; theorem :: REAL_3:24 modSeq(0,n) = NAT --> 0; theorem :: REAL_3:25 ex k being Nat st divSeq(m,n).k = 0 & modSeq(m,n).k = 0; begin definition let r be Real; func remainders_for_scf r -> Real_Sequence means :: REAL_3:def 3 it.0 = r & for n being Nat holds it.(n+1) = 1 / frac(it.n); end; notation let r be Real; synonym rfs r for remainders_for_scf r; end; definition let r be Real; func SimpleContinuedFraction r -> Integer_Sequence means :: REAL_3:def 4 for n being Nat holds it.n = [\ rfs(r).n /]; end; notation let r be Real; synonym scf r for SimpleContinuedFraction r; end; theorem :: REAL_3:26 rfs(r).(n+1) = 1 / (rfs(r).n-scf(r).n); theorem :: REAL_3:27 rfs(r).n = 0 & n <= m implies rfs(r).m = 0; theorem :: REAL_3:28 rfs(r).n = 0 & n <= m implies scf(r).m = 0; theorem :: REAL_3:29 rfs(i).(n+1) = 0; theorem :: REAL_3:30 scf(i).0 = i & scf(i).(n+1) = 0; theorem :: REAL_3:31 i > 1 implies rfs(1/i).1 = i & rfs(1/i).(n+2) = 0; theorem :: REAL_3:32 i > 1 implies scf(1/i).0 = 0 & scf(1/i).1 = i & scf(1/i).(n+2) = 0; theorem :: REAL_3:33 (for n holds scf(r).n = 0) implies rfs(r).n = 0; theorem :: REAL_3:34 (for n holds scf(r).n = 0) implies r = 0; theorem :: REAL_3:35 frac(r) = r - scf(r).0; theorem :: REAL_3:36 rfs(r).(n+1) = rfs(1/frac(r)).n; theorem :: REAL_3:37 scf(r).(n+1) = scf(1/frac(r)).n; theorem :: REAL_3:38 n >= 1 implies scf(r).n >= 0; theorem :: REAL_3:39 n >= 1 implies scf(r).n in NAT; theorem :: REAL_3:40 n >= 1 & scf(r).n <> 0 implies scf(r).n >= 1; theorem :: REAL_3:41 scf(m/n).k = divSeq(m,n).k & rfs(m/n).1 = n / modSeq(m,n).0 & rfs(m/n).(k+2) = (modSeq(m,n).k) / (modSeq(m,n).(k+1)); theorem :: REAL_3:42 r is rational iff ex n st for m st m >= n holds scf(r).m = 0; theorem :: REAL_3:43 (for n holds scf(r).n <> 0) implies r is irrational; begin :: Convergents of simple continued fractions reserve l, n1, n2 for Nat; reserve s1, s2 for Real_Sequence; definition let r be Real; func convergent_numerators(r) -> Real_Sequence means :: REAL_3:def 5 it.0 = scf(r).0 & it.1 = scf(r).1 * scf(r).0 + 1 & for n being Nat holds it.(n+2) = scf(r).(n+2 ) * it.(n+1) + it.n; end; definition let r be Real; func convergent_denominators(r) -> Real_Sequence means :: REAL_3:def 6 it.0 = 1 & it. 1 = scf(r).1 & for n being Nat holds it.(n+2) = scf(r).(n+2) * it.(n+1) + it.n; end; notation let r be Real; synonym c_n(r) for convergent_numerators(r); synonym c_d(r) for convergent_denominators(r); end; theorem :: REAL_3:44 scf(r).0 > 0 implies for n holds c_n(r).n in NAT; theorem :: REAL_3:45 scf(r).0 > 0 implies for n holds c_n(r).n > 0; theorem :: REAL_3:46 scf(r).0 > 0 implies for n holds c_n(r).(n+2) > scf(r).(n+2) * c_n(r). (n+1); theorem :: REAL_3:47 scf(r).0 > 0 implies for n st n1=c_n(r).(n+1) & n2=c_n(r).n holds n1 gcd n2 = 1; theorem :: REAL_3:48 scf(r).0 > 0 & (for n holds scf(r).n <> 0) implies for n holds c_n(r). n >= tau |^ n; theorem :: REAL_3:49 scf(r).0 > 0 & (for n holds scf(r).n <= b) implies for n holds c_n(r). n <= ((b+sqrt (b^2+4))/2)|^(n+1); theorem :: REAL_3:50 c_d(r).n in NAT; theorem :: REAL_3:51 c_d(r).n >= 0; theorem :: REAL_3:52 scf(r).1 > 0 implies for n holds c_d(r).n > 0; theorem :: REAL_3:53 c_d(r).(n+2) >= scf(r).(n+2) * c_d(r).(n+1); theorem :: REAL_3:54 scf(r).1 > 0 implies for n holds c_d(r).(n+2) > scf(r).(n+2) * c_d(r). (n+1); theorem :: REAL_3:55 (for n holds scf(r).n>0) implies for n st n>=1 holds 1 / (c_d(r).n*c_d (r).(n+1)) < 1 / (scf(r).(n+1)*(c_d(r).n)^2); theorem :: REAL_3:56 (for n holds scf(r).n <= b) implies for n holds c_d(r).(n+1) <= ((b+ sqrt (b^2+4))/2)|^(n+1); theorem :: REAL_3:57 n1=c_d(r).(n+1) & n2=c_d(r).n implies n1 gcd n2 = 1; theorem :: REAL_3:58 (for n holds scf(r).n > 0) implies for n holds c_d(r).(n+1)/c_d( r).n >= 1/scf(r).(n+2); theorem :: REAL_3:59 (for n holds scf(r).n > 0) implies for n holds c_d(r).(n+2) <= 2*scf(r ).(n+2) * c_d(r).(n+1); theorem :: REAL_3:60 (for n holds scf(r).n<>0) implies for n holds 1/(scf(r).(n+1)*(c_d(r). n)^2) <= 1/(c_d(r).n)^2; theorem :: REAL_3:61 (for n holds scf(r).n<>0) implies for n holds c_d(r).(n+1) >= tau |^ n; theorem :: REAL_3:62 a > 0 & (for n holds scf(r).n >= a) implies for n holds c_d(r).(n+1) >= ((a+sqrt (a^2+4))/2)|^n; theorem :: REAL_3:63 c_n(r).(n+2) / c_d(r).(n+2) = (scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n) / (scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n); theorem :: REAL_3:64 c_n(r).(n+1)*c_d(r).n - c_n(r).n*c_d(r).(n+1) = (-1)|^n; theorem :: REAL_3:65 (for n holds c_d(r).n<>0) implies c_n(r).(n+1)/c_d(r).(n+1) - c_n(r).n/c_d(r).n = (-1)|^n / (c_d(r).(n+1)*c_d(r).n); theorem :: REAL_3:66 c_n(r).(n+2)*c_d(r).n - c_n(r).n*c_d(r).(n+2) = (-1)|^n * scf(r) .(n+2); theorem :: REAL_3:67 (for n holds c_d(r).n<>0) implies c_n(r).(n+2)/c_d(r).(n+2) - c_n(r).n /c_d(r).n = (-1)|^n * scf(r).(n+2) / (c_d(r).(n+2) * c_d(r).n); theorem :: REAL_3:68 (for n holds scf(r).n<>0) implies for n st n >= 1 holds c_n(r).n / c_d (r).n = (c_n(r).(n+1)-c_n(r).(n-1)) / (c_d(r).(n+1)-c_d(r).(n-1)); theorem :: REAL_3:69 (for n holds c_d(r).n<>0) implies for n holds |.c_n(r).(n+1)/c_d(r) .(n+1) - c_n(r).n/c_d(r).n.| = 1 / |.c_d(r).(n+1)*c_d(r).n.|; theorem :: REAL_3:70 scf(r).1 > 0 implies for n holds c_n(r).(2*n+1) / c_d(r).(2*n+1) > c_n (r).(2*n) / c_d(r).(2*n); definition let r be Real; ::$N Convergents of continued fraction func convergents_of_continued_fractions(r) -> Real_Sequence equals :: REAL_3:def 7 c_n(r) /" c_d(r); end; notation let r be Real; synonym cocf(r) for convergents_of_continued_fractions(r); end; theorem :: REAL_3:71 cocf(r).0 = scf(r).0; theorem :: REAL_3:72 scf(r).1 <> 0 implies cocf(r).1 = scf(r).0 + 1 / scf(r).1; theorem :: REAL_3:73 (for n holds scf(r).n>0) implies cocf(r).2 = scf(r).0 + 1 / (scf (r).1 + 1/scf(r).2); theorem :: REAL_3:74 (for n holds scf(r).n>0) implies cocf(r).3 = scf(r).0 + 1/(scf(r ).1 + 1/(scf(r).2 + 1/scf(r).3)); theorem :: REAL_3:75 (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n+1) / c_d(r).(2*n+1) < c_n(r).(2*n-1) / c_d(r).(2*n-1); theorem :: REAL_3:76 (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n) / c_d(r).(2*n) > c_n(r).(2*n-2) / c_d(r).(2*n-2); theorem :: REAL_3:77 (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n) / c_d(r).(2*n) < c_n(r).(2*n-1) / c_d(r).(2*n-1); definition let r be Real; func backContinued_fraction r -> Real_Sequence means :: REAL_3:def 8 it.0 = scf(r).0 & for n being Nat holds it.(n+1) = 1/it.n + scf(r).(n+1); end; notation let r be Real; synonym bcf r for backContinued_fraction r; end; theorem :: REAL_3:78 scf(r).0 > 0 implies for n holds bcf(r).(n+1)=c_n(r).(n+1)/c_n(r).n;