:: Simple Continued Fractions and Their Convergents
:: by Bo Li , Yan Zhang and Artur Korni{\l}owicz
::
:: Received August 18, 2006
:: Copyright (c) 2006-2016 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;