REAL_3: Simple Continued Fractions and Their Convergents

:: 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

Lm1: for a, b, c, d being Real st (a / b) - c <> 0 & d <> 0 & b <> 0 & a = (b * c) + d holds
1 / ((a / b) - c) = b / d

proof end;

registration

let n be Nat;

cluster n div 0 -> zero ;

coherence by NAT_D:def 1;

cluster n mod 0 -> zero ;

coherence by NAT_D:def 2;

cluster 0 div n -> zero ;

coherence by NAT_2:2;

cluster 0 mod n -> zero ;

coherence by NAT_D:26;

end;

registration

let c be Complex;

cluster c - c -> zero ;

coherence by XCMPLX_1:14;

cluster c / 0 -> zero ;

coherence ;

end;

registration

cluster [\0/] -> zero ;

coherence by INT_1:25;

end;

theorem Th1: :: REAL_3:1

for r being Real st 0 < r & r < 1 holds
1 < 1 / r

proof end;

theorem Th2: :: REAL_3:2

for i being Integer
for r being Real st i <= r & r < i + 1 holds
[\r/] = i

proof end;

theorem :: REAL_3:3

for n, m being Nat holds [\(m / n)/] = m div n ;

theorem Th4: :: REAL_3:4

for n, m being Nat st m mod n = 0 holds
m / n = m div n

proof end;

theorem Th5: :: REAL_3:5

for n, m being Nat st m / n = m div n holds
m mod n = 0

proof end;

theorem Th6: :: REAL_3:6

for n, m being Nat holds frac (m / n) = (m mod n) / n

proof end;

theorem Th7: :: REAL_3:7

for p being Rational st p >= 0 holds
ex m, n being Nat st
( n <> 0 & p = m / n )

proof end;

registration

cluster Relation-like omega -defined REAL -valued INT -valued V6() Function-like V29( omega ) V33( omega , REAL ) V67() V68() V69() for Element of K16(K17(omega,REAL));

existence

proof end;

end;

definition

mode Integer_Sequence is INT -valued Real_Sequence;

end;

theorem Th8: :: REAL_3:8

for f being Function holds
( f is Integer_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is integer ) ) )

proof end;

theorem Th9: :: REAL_3:9

for f being Function holds
( f is sequence of INT iff f is Integer_Sequence )

proof end;

theorem :: REAL_3:10

for f being Function holds
( f is sequence of NAT iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is natural ) ) )

proof end;

theorem :: REAL_3:11

for f being Function holds
( f is sequence of NAT iff f is sequence of NAT ) ;

definition

deffunc H₁( Nat, Nat, Nat) -> Element of omega = $2 mod $3;
let m, n be Nat;
set a = m mod n;
set b = n mod (m mod n);

func modSeq (m,n) -> sequence of NAT means :Def1: :: 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)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines modSeq REAL_3:def 1 :

definition

let m, n be Nat;
set a = m div n;
set b = n div (m mod n);
deffunc H₁( Nat, Nat, Nat) -> Element of omega = ((modSeq (m,n)) . $1) div ((modSeq (m,n)) . ($1 + 1));

func divSeq (m,n) -> sequence of NAT means :Def2: :: 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)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines divSeq REAL_3:def 2 :

theorem Th12: :: REAL_3:12

for n, m being Nat holds (divSeq (m,n)) . 1 = n div ((modSeq (m,n)) . 0)

proof end;

theorem Th13: :: REAL_3:13

for n, m being Nat holds (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0)

proof end;

theorem Th14: :: REAL_3:14

for a, b, n, m being Nat st a <= b & (modSeq (m,n)) . a = 0 holds
(modSeq (m,n)) . b = 0

proof end;

Lm2: for a, n, m being Nat holds
( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )

proof end;

theorem Th15: :: REAL_3:15

for a, b, n, m being Nat holds
( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 )

proof end;

theorem Th16: :: REAL_3:16

for a, n, m being Nat st (divSeq (m,n)) . (a + 1) = 0 holds
(modSeq (m,n)) . a = 0

proof end;

Lm3: for a, n, m being Nat st (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . (a + 1) = 0

proof end;

theorem Th17: :: REAL_3:17

for a, b, n, m being Nat st a <> 0 & a <= b & (divSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0

proof end;

theorem Th18: :: REAL_3:18

for a, b, n, m being Nat st a < b & (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0

proof end;

theorem Th19: :: REAL_3:19

for n, m being Nat st n <> 0 holds
m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0)

proof end;

theorem :: REAL_3:20

for n, m being Nat st n <> 0 holds
m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0)))

proof end;

set g = NAT --> 0;

theorem Th21: :: REAL_3:21

for m being Nat holds divSeq (m,0) = NAT --> 0

proof end;

theorem Th22: :: REAL_3:22

for m being Nat holds modSeq (m,0) = NAT --> 0

proof end;

theorem :: REAL_3:23

for n being Nat holds divSeq (0,n) = NAT --> 0

proof end;

theorem :: REAL_3:24

for n being Nat holds modSeq (0,n) = NAT --> 0

proof end;

Lm4: for n, m being Nat ex k being Nat st (modSeq (m,n)) . k = 0

proof end;

theorem Th25: :: REAL_3:25

for n, m being Nat ex k being Nat st
( (divSeq (m,n)) . k = 0 & (modSeq (m,n)) . k = 0 )

proof end;

defpred S₁[ set , Element of REAL , object ] means $3 = 1 / (frac $2);

definition

let r be Real;

func remainders_for_scf r -> Real_Sequence means :Def3: :: REAL_3:def 3
( it . 0 = r & ( for n being Nat holds it . (n + 1) = 1 / (frac (it . n)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines remainders_for_scf REAL_3:def 3 :

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 :Def4: :: REAL_3:def 4
for n being Nat holds it . n = [\((rfs r) . n)/];

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines SimpleContinuedFraction REAL_3:def 4 :

notation

let r be Real;
synonym scf r for SimpleContinuedFraction r;

end;

theorem Th26: :: REAL_3:26

for n being Nat
for r being Real holds (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n))

proof end;

theorem Th27: :: REAL_3:27

for n, m being Nat
for r being Real st (rfs r) . n = 0 & n <= m holds
(rfs r) . m = 0

proof end;

theorem :: REAL_3:28

for n, m being Nat
for r being Real st (rfs r) . n = 0 & n <= m holds
(scf r) . m = 0

proof end;

theorem Th29: :: REAL_3:29

for n being Nat
for i being Integer holds (rfs i) . (n + 1) = 0

proof end;

theorem Th30: :: REAL_3:30

for n being Nat
for i being Integer holds
( (scf i) . 0 = i & (scf i) . (n + 1) = 0 )

proof end;

Lm5: for n being Nat
for i being Integer st i > 1 holds
( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 )

proof end;

theorem :: REAL_3:31

for n being Nat
for i being Integer st i > 1 holds
( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 ) by Lm5;

theorem :: REAL_3:32

for n being Nat
for i being Integer st i > 1 holds
( (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by Lm5;

theorem Th33: :: REAL_3:33

for n being Nat
for r being Real st ( for n being Nat holds (scf r) . n = 0 ) holds
(rfs r) . n = 0

proof end;

theorem Th34: :: REAL_3:34

for r being Real st ( for n being Nat holds (scf r) . n = 0 ) holds
r = 0

proof end;

Lm6: for n being Nat
for r being Real holds
( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) )

proof end;

theorem Th35: :: REAL_3:35

for r being Real holds frac r = r - ((scf r) . 0)

proof end;

theorem :: REAL_3:36

for n being Nat
for r being Real holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n

proof end;

theorem Th37: :: REAL_3:37

for n being Nat
for r being Real holds (scf r) . (n + 1) = (scf (1 / (frac r))) . n

proof end;

theorem Th38: :: REAL_3:38

for n being Nat
for r being Real st n >= 1 holds
(scf r) . n >= 0

proof end;

theorem :: REAL_3:39

for n being Nat
for r being Real st n >= 1 holds
(scf r) . n in NAT by Th38, INT_1:3;

theorem Th40: :: REAL_3:40

for n being Nat
for r being Real st n >= 1 & (scf r) . n <> 0 holds
(scf r) . n >= 1

proof end;

theorem Th41: :: REAL_3:41

for k, n, m being Nat holds
( (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)) )

proof end;

theorem Th42: :: REAL_3:42

for r being Real holds
( r is rational iff ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 )

proof end;

theorem :: REAL_3:43

for r being Real st ( for n being Nat holds (scf r) . n <> 0 ) holds
r is irrational

proof end;

definition

let r be Real;

func convergent_numerators r -> Real_Sequence means :Def5: :: 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) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines convergent_numerators REAL_3:def 5 :

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

definition

let r be Real;
set s = scf r;

func convergent_denominators r -> Real_Sequence means :Def6: :: 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) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines convergent_denominators REAL_3:def 6 :

notation

let r be Real;
synonym c_n r for convergent_numerators r;
synonym c_d r for convergent_denominators r;

end;

theorem Th44: :: REAL_3:44

for r being Real st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . n in NAT

proof end;

theorem Th45: :: REAL_3:45

for r being Real st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . n > 0

proof end;

theorem :: REAL_3:46

for r being Real st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1))

proof end;

theorem :: REAL_3:47

for r being Real
for n1, n2 being Nat st (scf r) . 0 > 0 holds
for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1

proof end;

theorem :: REAL_3:48

for r being Real st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds (c_n r) . n >= tau |^ n

proof end;

theorem :: REAL_3:49

for b being Nat
for r being Real st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)

proof end;

theorem Th50: :: REAL_3:50

for n being Nat
for r being Real holds (c_d r) . n in NAT

proof end;

theorem Th51: :: REAL_3:51

for n being Nat
for r being Real holds (c_d r) . n >= 0

proof end;

theorem Th52: :: REAL_3:52

for r being Real st (scf r) . 1 > 0 holds
for n being Nat holds (c_d r) . n > 0

proof end;

theorem :: REAL_3:53

for n being Nat
for r being Real holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1))

proof end;

theorem :: REAL_3:54

for r being Real st (scf r) . 1 > 0 holds
for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1))

proof end;

theorem :: REAL_3:55

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat st n >= 1 holds
1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2))

proof end;

theorem :: REAL_3:56

for b being Nat
for r being Real st ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)

proof end;

theorem :: REAL_3:57

for n being Nat
for r being Real
for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds
n1 gcd n2 = 1

proof end;

theorem Th58: :: REAL_3:58

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2))

proof end;

theorem :: REAL_3:59

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1))

proof end;

theorem :: REAL_3:60

for r being Real st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2)

proof end;

theorem :: REAL_3:61

for r being Real st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds (c_d r) . (n + 1) >= tau |^ n

proof end;

theorem :: REAL_3:62

for a being Nat
for r being Real st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds
for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n

proof end;

theorem :: REAL_3:63

for n being Nat
for r being Real holds ((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))

proof end;

theorem Th64: :: REAL_3:64

for n being Nat
for r being Real holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n

proof end;

theorem Th65: :: REAL_3:65

for n being Nat
for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((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))

proof end;

theorem Th66: :: REAL_3:66

for n being Nat
for r being Real holds (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2))

proof end;

theorem :: REAL_3:67

for n being Nat
for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((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))

proof end;

theorem :: REAL_3:68

for r being Real st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat 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)))

proof end;

theorem :: REAL_3:69

for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
for n being Nat 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)).|

proof end;

theorem :: REAL_3:70

for r being Real st (scf r) . 1 > 0 holds
for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n))

proof end;

definition

let r be Real;

Convergents of continued fraction

func convergents_of_continued_fractions r -> Real_Sequence equals :: REAL_3:def 7
(c_n r) /" (c_d r);

coherence ;

end;

:: deftheorem defines convergents_of_continued_fractions REAL_3:def 7 :

notation

let r be Real;
synonym cocf r for convergents_of_continued_fractions r;

end;

theorem :: REAL_3:71

for r being Real holds (cocf r) . 0 = (scf r) . 0

proof end;

theorem Th72: :: REAL_3:72

for r being Real st (scf r) . 1 <> 0 holds
(cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1))

proof end;

theorem Th73: :: REAL_3:73

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
(cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))

proof end;

theorem Th74: :: REAL_3:74

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
(cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3))))))

proof end;

theorem :: REAL_3:75

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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))

proof end;

theorem :: REAL_3:76

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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))

proof end;

theorem :: REAL_3:77

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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))

proof end;

definition

let r be Real;
set s = scf r;

func backContinued_fraction r -> Real_Sequence means :Def8: :: REAL_3:def 8
( it . 0 = (scf r) . 0 & ( for n being Nat holds it . (n + 1) = (1 / (it . n)) + ((scf r) . (n + 1)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines backContinued_fraction REAL_3:def 8 :

notation

let r be Real;
synonym bcf r for backContinued_fraction r;

end;

theorem :: REAL_3:78

for r being Real st (scf r) . 0 > 0 holds
for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n)

proof end;