:: Introduction to {D}iophantine Approximation
:: by Yasushige Watase
::
:: Received April 19, 2015
:: Copyright (c) 2015-2026 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 ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, FINANCE1, FINSEQ_1, FUNCT_1,
INT_1, IRRAT_1, NAT_1, NEWTON, NUMBERS, PROB_1, PROB_3, RAT_1, REAL_1,
REAL_3, RELAT_1, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, XXREAL_1, INT_2,
ORDINAL1, SQUARE_1, ABIAN, FINSET_1, SEQ_1, ORDINAL2, SEQ_2, VALUED_1,
DIOPHAN1, NAT_6;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, XREAL_0, COMPLEX1,
FINSEQ_1, XXREAL_1, PROB_1, FINANCE1, PROB_3, IRRAT_1, REAL_3, NEWTON,
SQUARE_1, REAL_1, ABIAN, INT_2, FINSET_1, RAT_1, COMSEQ_2, SEQ_1, SEQ_2,
VALUED_1, NAT_D, FUNCOP_1, NAT_6;
constructors REAL_1, SQUARE_1, SEQ_2, NEWTON, RELSET_1, COMSEQ_2, ABIAN,
REAL_3, PROB_3, FINANCE1, NAT_6;
registrations XREAL_0, NAT_1, INT_1, FINSET_1, XXREAL_0, NEWTON, CARD_1,
VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, FUNCT_2, ABIAN, NAT_3, SQUARE_1,
ZFMISC_1, RAT_1, MEMBERED, VALUED_1, NAT_6;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ORDINAL1, FINSEQ_1, XBOOLE_0, VALUED_1, XCMPLX_0;
expansions TARSKI, XBOOLE_0, PBOOLE, NAT_6, FUNCT_1;
theorems AXIOMS, INT_1, INT_2, NAT_1, XXREAL_0, XREAL_1, FINSEQ_1, ORDINAL1,
XBOOLE_1, FUNCT_1, FUNCT_2, ABSVALUE, NEWTON, XXREAL_1, CARD_1, FINSEQ_4,
COMPLEX1, XCMPLX_0, XCMPLX_1, PROB_3, CARD_2, REAL_3, SERIES_2, SQUARE_1,
WSIERP_1, RAT_1, SEQ_1, VALUED_1, SEQ_2;
schemes FUNCT_2, FINSEQ_1, NAT_1, FIB_NUM, SEQ_1;
begin :: Irrational & Continued Fraction
reserve i,j,k,m,n,m1,n1 for Nat;
reserve a,r,r1,r2 for Real;
reserve m0,cn,cd for Integer;
reserve x1,x2,o for object;
:: Approximation an irrational by its simple continued fraction
theorem Th1:
r = rfs(r).0 & r = scf(r).0 + 1/rfs(r).1 &
rfs(r).n = scf(r).n + 1/rfs(r).(n+1)
proof
A1: rfs(r).1 = rfs(r).(0+1) .= 1/frac(rfs(r).0) by REAL_3:def 3;
A2: frac(rfs(r).0) = frac(r) by REAL_3:def 3 .= r - scf(r).0 by REAL_3:35;
A4: frac(rfs(r).n) = rfs(r).n - [\ rfs(r).n /] by INT_1:def 8;
1/rfs(r).(n+1) = 1/(1/frac(rfs(r).n)) by REAL_3:def 3
.= frac(rfs(r).n); then
scf(r).n + 1/rfs(r).(n+1) = scf(r).n + rfs(r).n - [\ rfs(r).n /] by A4
.= scf(r).n + rfs(r).n - scf(r).n by REAL_3:def 4 .= rfs(r).n;
hence thesis by REAL_3:def 3,A2,A1;
end;
theorem Th2:
r is irrational implies
rfs(r).n is irrational
proof
assume
A1: r is irrational;
set rn = rfs(r).n;
A3: scf(rn).0 = [\ rfs(rn).0 /] by REAL_3:def 4
.= [\ rfs(r).n /] by REAL_3:def 3
.= scf(r).n by REAL_3:def 4;
A4: scf(rn).m = scf(r).(n+m) & rfs(rn).m = rfs(r).(n+m)
proof
defpred P[Nat] means
scf(rn).$1 = scf(r).(n+$1) & rfs(rn).$1 = rfs(r).(n+$1);
A5: P[0] by REAL_3:def 3,A3;
A6: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A7: P[m];
A9: rfs(rn).(m+1) = 1 / frac(rfs(rn).m) by REAL_3:def 3
.= rfs(r).(n+m+1) by A7,REAL_3:def 3;
scf(rn).(m+1)= [\ rfs(rn).(m+1) /] by REAL_3:def 4
.= scf(r).(n+m+1) by A9,REAL_3:def 4;
hence thesis by A9;
end;
for m be Nat holds P[m] from NAT_1:sch 2(A5,A6);
hence thesis;
end;
assume
A10:rfs(r).n is rational;
consider n1 such that
A12:for m1 st m1 >= n1 holds scf(rn).m1 = 0 by A10,REAL_3:42;
A13:for m1 st m1 >= n1 holds scf(r).(n+m1) = 0
proof
let m1;
assume
A14: m1 >= n1;
scf(r).(n+m1)=scf(rn).m1 by A4 .= 0 by A12,A14;
hence thesis;
end;
for m st m >= n1+n holds scf(r).m = 0
proof
let m;
assume
A15: m >= n1+n;
A16: m -n >= n1+n - n by A15,XREAL_1:9;
m - n in NAT by A16,INT_1:3; then
reconsider l = m - n as Nat;
scf(r).(n+l) = 0 by A13,A16;
hence thesis;
end;
hence contradiction by A1,REAL_3:42;
end;
theorem Th3:
r is irrational implies rfs(r).n <> 0 &
rfs(r).1*rfs(r).2 <> 0 &
scf(r).1*rfs(r).2 + 1 <> 0
proof
assume
A1: r is irrational;
A2: rfs(r).n <> 0
proof
assume rfs(r).n = 0; then
consider n1 be Nat such that
A4: rfs(r).n1 = 0;
n1 <= m implies scf(r).m = 0 by A4,REAL_3:28;
hence contradiction by A1,REAL_3:42;
end;
A5: rfs(r).1 <> 0 & rfs(r).2 <> 0 by A1,Th2;
rfs(r).1 = scf(r).1 + 1/rfs(r).(1+1) by Th1; then
rfs(r).1*rfs(r).2 = scf(r).1*rfs(r).2 + (1/rfs(r).2)*rfs(r).2
.= scf(r).1*rfs(r).2 + 1 by XCMPLX_1:106,A5;
hence thesis by A2,A5;
end;
theorem Th4:
r is irrational implies
scf(r).n < rfs(r).n & rfs(r).n < scf(r).n + 1 & 1 < rfs(r).(n+1)
proof
assume r is irrational; then
A2: rfs(r).n is not integer by Th2;
A3: 1/rfs(r).(n+1) = 1/(1/frac(rfs(r).n)) by REAL_3:def 3
.= frac(rfs(r).n);
A4: 1/rfs(r).(n +1)> 0 by A2,A3,INT_1:46;
A5: rfs(r).n = scf(r).n + 1/rfs(r).(n+1) by Th1;
A6: rfs(r).n - scf(r).n + scf(r).n > 0 + scf(r).n
by A2,A3,A5,INT_1:46,XREAL_1:8;
1" < ((rfs(r).(n +1))")" by A3,INT_1:43,A4,XREAL_1:88;
hence thesis by A6,A5,A3,INT_1:43,XREAL_1:8;
end;
theorem Th5:
r is irrational implies 0 < scf(r).(n+1)
proof
assume
A1: r is irrational;
A2: rfs(r).(n +1)-1 > 1-1 by A1,Th4,XREAL_1:14;
rfs(r).(n +1) < scf(r).(n +1) + 1 by A1,Th4; then
rfs(r).(n +1) -1 < scf(r).(n +1) + 1 -1 by XREAL_1:14;
hence thesis by A2;
end;
Th6:
for n holds c_n(r).n is Integer
proof
defpred P[Nat] means
c_n(r).$1 is Integer;
A1: for n being Nat st P[n] & P[n+1] holds P[n+2]
proof
let n be Nat;
assume that
A2: c_n(r).n is Integer and
A3: c_n(r).(n+1) is Integer;
c_n(r).(n+2) = scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n by REAL_3:def 5;
hence thesis by A2,A3;
end;
A5: P[1]
proof
c_n(r).1 = scf(r).1 * scf(r).0 + 1 by REAL_3:def 5;
hence thesis;
end;
A6: P[0]
proof
c_n(r).0 = scf(r).0 by REAL_3:def 5;
hence thesis;
end;
for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A5,A1);
hence thesis;
end;
registration let r,n;
cluster c_n(r).n -> integer;
coherence by Th6;
end;
theorem Th7:
:: [Hardy&Wright] Ch.10 Th155
r is irrational implies for n holds c_d(r).(n+1) >= c_d(r).n
proof
assume
A1: r is irrational;
defpred P[Nat] means c_d(r).$1 <= c_d(r).($1+1);
A2: P[0]
proof
A3: c_d(r).0 = 1 by REAL_3:def 6;
rfs(r).(0+1) > 1 by A1,Th4; then
rfs(r).1 - 1 > 1 -1 by XREAL_1:14; then
[\ rfs(r).1 /] > 0 by INT_1:def 6; then
scf(r).1 > 0 by REAL_3:def 4; then
0+1 <= scf(r).1 by INT_1:7;
hence thesis by A3,REAL_3:def 6;
end;
A8: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
A9: c_d(r).(n+2) - c_d(r).(n+1)
= scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n - c_d(r).(n+1) by REAL_3:def 6
.= (scf(r).(n+2) -1) * c_d(r).(n+1) + c_d(r).n;
A10: scf(r).(n+2) = [\ rfs(r).(n+2) /] by REAL_3:def 4;
rfs(r).(n+1+1) > 1 by A1,Th4; then
rfs(r).(n+2) - 1 > 1 -1 by XREAL_1:14; then
scf(r).(n+2) > 0 by A10,INT_1:def 6; then
0+1 <= scf(r).(n+2) by INT_1:7; then
A12: scf(r).(n+2) -1 >= 1 -1 by XREAL_1:13;
c_d(r).(n+1) >= 0 & c_d(r).n >= 0 by REAL_3:51; then
c_d(r).(n+2) - c_d(r).(n+1) + c_d(r).(n+1) >= 0 + c_d(r).(n+1)
by A9,A12,XREAL_1:6;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A8);
hence thesis;
end;
theorem Th8:
r is irrational implies c_d(r).n >=1
proof
assume
A1: r is irrational;
defpred P[Nat] means c_d(r).$1 >=1;
A2: P[0] by REAL_3:def 6;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
c_d(r).(n+1) >= c_d(r).n by A1,Th7;
hence thesis by A4,XXREAL_0:2;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
::[Hardy&Wright] Irrational case of Ch. 10 Th155
theorem
r is irrational implies c_d(r).(n+2) > c_d(r).(n+1)
proof
assume
A1: r is irrational; then
A2: scf(r).(n+1+1) > 0 by Th5;
A3: n+2 >= 0+1 by XREAL_1:8;
A4: c_d(r).(n+2) = scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n by REAL_3:def 6;
c_d(r).n > 0 by A1,Th8; then
A5: c_d(r).(n+2) -0 > scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n - c_d(r).n
by A4,XREAL_1:15;
c_d(r).(n+1) >= 1 by A1,Th8; then
scf(r).(n+2)*c_d(r).(n+1) >= c_d(r).(n+1) by A2,A3,REAL_3:40,XREAL_1:151;
hence thesis by A5,XXREAL_0:2;
end;
::[Hardy&Wright] Ch.10 Th156
theorem Th10:
r is irrational implies c_d(r).n >= n
proof
assume
A1: r is irrational;
defpred P[Nat] means c_d(r).$1 >= $1;
A2: P[0] by REAL_3:def 6;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
set m = n -1;
per cases;
suppose n=0;
hence thesis by A1,Th8;
end;
suppose n > 0; then
reconsider m as Nat;
A7: scf(r).(m+1+1) > 0 by A1,Th5;
A8: m+2 >= 0+1 by XREAL_1:8;
c_d(r).(m+1) >= 1 by A1,Th8; then
A9: scf(r).(m+2)*c_d(r).(m+1) >= c_d(r).(m+1)
by A7,A8,REAL_3:40,XREAL_1:151;
scf(r).(m+2)*c_d(r).(m+1) + c_d(r).m >= c_d(r).(m+1) +c_d(r).m
by A9,XREAL_1:6; then
A12: c_d(r).(m+2) >= c_d(r).(m+1) + c_d(r).m by REAL_3:def 6;
A13: c_d(r).(m+1) + c_d(r).m >= n+c_d(r).m by A4,XREAL_1:6;
n+c_d(r).m >= n + 1 by A1,Th8,XREAL_1:6; then
c_d(r).(m+1) + c_d(r).m >= n + 1 by A13,XXREAL_0:2;
hence thesis by A12,XXREAL_0:2;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
::[Hardy&Wright] Ch.10 Th157
theorem
cn = c_n(r).n & cd = c_d(r).n & cn <> 0 implies
cn,cd are_coprime
proof
c_d(r).(n+1) in NAT by REAL_3:50; then
reconsider cd2 = c_d(r).(n+1) as Integer;
reconsider cn2 = c_n(r).(n+1) as Integer;
assume that
A2: cn = c_n(r).n and
A3: cd = c_d(r).n and
A4: cn <> 0;
assume
A5: not (cn,cd are_coprime);
A6: cn2*cd -cn*cd2 = (-1)|^n by A2,A3,REAL_3:64;
consider cn0,cd0 be Integer such that
A8: cn = (cn gcd cd)*cn0 and
A9: cd = (cn gcd cd)*cd0 and
cn0,cd0 are_coprime by A4,INT_2:23;
cn gcd cd <> 0 by A4,INT_2:5; then
cn gcd cd >= 0 +1 by INT_1:7; then
A11:cn gcd cd > 1 by A5,INT_2:def 3,XXREAL_0:1;
A12:(-1)|^n = cn2*(cn gcd cd)*cd0 -cn*cd2 by A6,A9
.= (cn gcd cd)*(cn2*cd0 - cn0*cd2) by A8;
A13:1=|.(-1)|^n.| by SERIES_2:1 .=|.(cn gcd cd)*(cn2*cd0-cn0*cd2).| by A12
.=|.(cn gcd cd).|*|.(cn2*cd0-cn0*cd2).| by COMPLEX1:65
.=(cn gcd cd)*|.(cn2*cd0-cn0*cd2).| by ABSVALUE:def 1;
(cn gcd cd)" < 1 by A11,XREAL_1:212; then
|.(cn2*cd0-cn0*cd2).| < 1 by A13,XCMPLX_1:210; then
|.(cn2*cd0-cn0*cd2).| = 0 by NAT_1:14;
hence contradiction by A13;
end;
theorem Th12:
r is irrational implies
(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) > 0 &
(c_d(r).(n+1)*rfs(r).(n+2) - c_d(r).n) > 0
proof
assume
A1: r is irrational; then
A2: c_d(r).(n+1) >= 1 by Th8;
rfs(r).(n+1+1) > 1 by A1,Th4; then
A4: rfs(r).(n+2)*c_d(r).(n+1) > 1*c_d(r).(n+1) by A2,XREAL_1:68; then
A5: c_d(r).(n+1)*rfs(r).(n+2) > 1 by A2,XXREAL_0:2;
A6: c_d(r).n + 1 >= 1 + 1 by A1,Th8,XREAL_1:6;
c_d(r).(n+1) >= c_d(r).n by A1,Th7; then
c_d(r).(n+1)*rfs(r).(n+2) > c_d(r).n by A4,XXREAL_0:2; then
c_d(r).(n+1)*rfs(r).(n+2)-c_d(r).n > c_d(r).n-c_d(r).n by XREAL_1:14;
hence thesis by A5,A6,XREAL_1:6;
end;
theorem Th13:
r is irrational implies
(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) > 0
proof
assume
A1: r is irrational; then
A2: c_d(r).(n+1) >=1 by Th8;
(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) > 0 by A1,Th12;
hence thesis by A2;
end;
theorem Th14:
r is irrational implies
r = (c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)/
(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)
proof
assume
A1: r is irrational;
defpred P[Nat] means
r = (c_n(r).($1+1)*rfs(r).($1+2)+c_n(r).$1)
/(c_d(r).($1+1)*rfs(r).($1+2)+c_d(r).$1);
A2: P[0]
proof
A3: rfs(r).1 = scf(r).1 + 1/rfs(r).(1+1) by Th1;
A4: (c_n(r).1*rfs(r).2+c_n(r).0)
= (scf(r).1 * scf(r).0 + 1) *rfs(r).2+c_n(r).0 by REAL_3:def 5
.= (scf(r).1 * scf(r).0 + 1) *rfs(r).2 + scf(r).0 by REAL_3:def 5
.= scf(r).0*(scf(r).1 *rfs(r).2 + 1) + rfs(r).2;
A5: (c_d(r).1*rfs(r).2+c_d(r).0)=scf(r).1*rfs(r).2+c_d(r).0 by REAL_3:def 6
.= scf(r).1*rfs(r).2 + 1 by REAL_3:def 6;
A6: rfs(r).2 <> 0 & scf(r).1*rfs(r).2 + 1 <> 0 by A1,Th3;
(c_n(r).1*rfs(r).2+c_n(r).0)/(c_d(r).1*rfs(r).2+c_d(r).0)=
(scf(r).0*(scf(r).1*rfs(r).2+1)+rfs(r).2)/(c_d(r).1*rfs(r).2+c_d(r).0)
by A4
.= scf(r).0*((scf(r).1 *rfs(r).2 + 1)/( (scf(r).1*rfs(r).2 + 1)))
+ rfs(r).2 /(scf(r).1*rfs(r).2 + 1) by A5
.= scf(r).0 *1 + rfs(r).2 /(scf(r).1*rfs(r).2 + 1) by A6,XCMPLX_1:60
.= scf(r).0+(rfs(r).2/rfs(r).2)/((scf(r).1*rfs(r).2+1)/rfs(r).2)
by A6,XCMPLX_1:55
.= scf(r).0+1/((scf(r).1*rfs(r).2+1)/rfs(r).2) by A6,XCMPLX_1:60
.= scf(r).0 + 1/(scf(r).1*(rfs(r).2/rfs(r).2)+1/rfs(r).2)
.= scf(r).0 + 1/(scf(r).1*1+1/rfs(r).2) by A1,Th3,XCMPLX_1:60
.= r by Th1,A3;
hence thesis;
end;
A7: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A8: P[n];
A9: rfs(r).(n+2) = scf(r).(n+2) + 1/rfs(r).(n+2 +1) by Th1
.= scf(r).(n+2) + 1/rfs(r).(n+3);
A10: 1 = (rfs(r).(n+3))/(rfs(r).(n+3)) by A1,Th3,XCMPLX_1:60;
A11: c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n
= c_n(r).(n+1)*(scf(r).(n+2) + 1/rfs(r).(n+3))+c_n(r).n by A9
.= scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n + c_n(r).(n+1)* (1/rfs(r).(n+3))
.= c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3)) by REAL_3:def 5;
A12: c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n
= c_d(r).(n+1)*(scf(r).(n+2) + 1/rfs(r).(n+3))+c_d(r).n by A9
.= scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n + c_d(r).(n+1)* (1/rfs(r).(n+3))
.= c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3)) by REAL_3:def 6;
r=(c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)
by A8
.= (c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3)))/
(c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3))) by A11,A12
.= ((c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3)))
/(c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3))))
*(rfs(r).(n+3)/rfs(r).(n+3)) by A10
.= ((c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3))) * rfs(r).(n+3))
/((c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3))) * rfs(r).(n+3))
by XCMPLX_1:76
.= ((c_n(r).(n+2)*rfs(r).(n+3)
+c_n(r).(n+1)* ((1/rfs(r).(n+3))*rfs(r).(n+3)) ))
/((c_d(r).(n+2)*rfs(r).(n+3)
+c_d(r).(n+1)* ((1/rfs(r).(n+3))*rfs(r).(n+3)) ))
.= ((c_n(r).(n+2)*rfs(r).(n+3) +c_n(r).(n+1)*1))
/((c_d(r).(n+2)*rfs(r).(n+3)
+c_d(r).(n+1)*((1/rfs(r).(n+3))*rfs(r).(n+3)) )) by XCMPLX_1:106,A1,Th3
.= ((c_n(r).(n+2)*rfs(r).(n+3) +c_n(r).(n+1)*1))
/((c_d(r).(n+2)*rfs(r).(n+3) +c_d(r).(n+1)*1)) by XCMPLX_1:106,A1,Th3
.= (c_n(r).(n+1+1)*rfs(r).(n+1+2) +c_n(r).(n+1))
/(c_d(r).(n+1+1)*rfs(r).(n+1+2) +c_d(r).(n+1));
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A7);
hence thesis;
end;
::[Hardy&Wright] Ch.10 Th158
theorem Th15:
r is irrational implies
c_n(r).(n+1)/c_d(r).(n+1) - r
= (-1)|^n /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n))
proof
assume
A1: r is irrational; then
A3: c_d(r).(n+1) <> 0 by Th8;
A4: c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n <> 0 by A1,Th12;
A5: c_n(r).(n+1)/c_d(r).(n+1) - r
= c_n(r).(n+1)/c_d(r).(n+1) - (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n)
/(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) by A1,Th14
.= (c_n(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)
- (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n)*c_d(r).(n+1) )
/(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n))
by A3,A4,XCMPLX_1:130;
(c_n(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)
- (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n)*c_d(r).(n+1))
= c_n(r).(n+1)*c_d(r).(n+1)*rfs(r).(n+2) + c_n(r).(n+1)*c_d(r).n
- c_n(r).(n+1)*c_d(r).(n+1)*rfs(r).(n+2) - c_n(r).n*c_d(r).(n+1)
.= (-1)|^n by REAL_3:64;
hence thesis by A5;
end;
theorem Th16:
r is irrational & n is even & n > 0 implies
r > c_n(r).n/c_d(r).n
proof
assume
A1: r is irrational;
assume
A2: n is even;
assume n > 0; then
reconsider m = n -1 as odd natural number by A2;
(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0 by A1,Th13;
then (-1)|^m
/(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) < 0; then
c_n(r).(m+1)/c_d(r).(m+1) - r < 0 by A1,Th15; then
c_n(r).(n-1+1)/c_d(r).(n-1+1) -r + r < 0 + r by XREAL_1:8;
hence thesis;
end;
theorem Th17:
r is irrational & n is odd implies
r < c_n(r).n/c_d(r).n
proof
assume
A1: r is irrational;
assume n is odd; then
reconsider m = n -1 as even natural number;
(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0
by A1,Th13; then
(-1)|^m /(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0; then
c_n(r).(m+1)/c_d(r).(m+1) - r > 0 by A1,Th15; then
c_n(r).(m+1)/c_d(r).(m+1) - r + r > 0 + r by XREAL_1:8;
hence thesis;
end;
theorem
r is irrational & n > 0 implies
|. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .|
= |. c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1) .|
proof
assume that
A1: r is irrational and
A2: n > 0;
per cases;
suppose
A3: n is even;
r > c_n(r).n/c_d(r).n by A1,A2,A3,Th16; then
A4: r - c_n(r).n/c_d(r).n > c_n(r).n/c_d(r).n - c_n(r).n/c_d(r).n
by XREAL_1:14;
r - c_n(r).n/c_d(r).n <> 0 by A1,A2,A3,Th16; then
|. r - c_n(r).n/c_d(r).n.| <> 0 by ABSVALUE:2; then
A5: |. r - c_n(r).n/c_d(r).n .| > 0 by COMPLEX1:46;
A8: r - c_n(r).(n+1)/c_d(r).(n+1) <
c_n(r).(n+1)/c_d(r).(n+1) -c_n(r).(n+1)/c_d(r).(n+1)
by A1,A3,Th17,XREAL_1:14;then
|. r - c_n(r).(n+1)/c_d(r).(n+1).| <> 0 by ABSVALUE:2; then
A9: |. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by COMPLEX1:46;
A10: |. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| =
r - c_n(r).n/c_d(r).n + |. r - c_n(r).(n+1)/c_d(r).(n+1) .|
by A4,ABSVALUE:def 1 .= r - c_n(r).n/c_d(r).n +
-(r - c_n(r).(n+1)/c_d(r).(n+1)) by A8,ABSVALUE:def 1
.= - (c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1));
c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1) < 0 by A5,A9,A10;
hence thesis by A10,ABSVALUE:def 1;
end;
suppose
A11: n is odd; then
A13: r - c_n(r).n/c_d(r).n < c_n(r).n/c_d(r).n - c_n(r).n/c_d(r).n
by XREAL_1:14,A1,Th17;
r - c_n(r).n/c_d(r).n <> 0 by A1,A11,Th17; then
|. r - c_n(r).n/c_d(r).n.| <> 0 by ABSVALUE:2; then
A14: |. r - c_n(r).n/c_d(r).n .| > 0 by COMPLEX1:46;
r > c_n(r).(n+1)/c_d(r).(n+1) by A1,A11,Th16; then
A18: r - c_n(r).(n+1)/c_d(r).(n+1) >
c_n(r).(n+1)/c_d(r).(n+1)-c_n(r).(n+1)/c_d(r).(n+1) by XREAL_1:14;
|. r - c_n(r).(n+1)/c_d(r).(n+1).| <> 0 by A18,ABSVALUE:2; then
A19: |. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by COMPLEX1:46;
|. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| =
-(r - c_n(r).n/c_d(r).n) + |. r - c_n(r).(n+1)/c_d(r).(n+1) .|
by A13,ABSVALUE:def 1 .=
-r + c_n(r).n/c_d(r).n + (r - c_n(r).(n+1)/c_d(r).(n+1))
by A18,ABSVALUE:def 1
.= c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1);
hence thesis by A14,A19,ABSVALUE:def 1;
end;
end;
theorem Th19:
r is irrational implies |. r - c_n(r).n/c_d(r).n .| > 0
proof
assume
A1: r is irrational;
assume not |. r - c_n(r).n/c_d(r).n .| > 0; then
|. r - c_n(r).n/c_d(r).n .| = 0 by COMPLEX1:46; then
A3: r - c_n(r).n/c_d(r).n = 0 by COMPLEX1:45;
c_d(r).n in NAT by REAL_3:50;
hence contradiction by A1,A3;
end;
theorem
r is irrational implies c_d(r).(n+2) >= 2*c_d(r).n
proof
assume
A1: r is irrational; then
scf(r).(n+1+1) > 0 by Th5; then
A4: scf(r).(n+2) >=0+1 by INT_1:7;
A5: 0 < c_d(r).n by A1,Th8;
c_d(r).n <= c_d(r).(n+1) by A1,Th7; then
scf(r).(n+2) * c_d(r).(n+1) >= 1*c_d(r).n by A4,A5,XREAL_1:66; then
scf(r).(n+2)*c_d(r).(n+1) + c_d(r).n >= 1*c_d(r).n + c_d(r).n by XREAL_1:6;
hence thesis by REAL_3:def 6;
end;
theorem Th21:
r is irrational implies
|. r - c_n(r).(n+1)/c_d(r).(n+1) .| < 1/(c_d(r).(n+1)*c_d(r).(n+2))
proof
assume
A1: r is irrational; then
A2: c_d(r).(n+1) >= 1 by Th8;
A3: c_d(r).(n+1+1) >= 1 by A1,Th8;
scf(r).(n+2)*c_d(r).(n+1) < rfs(r).(n+2)*c_d(r).(n+1)
by A1,Th4,A2,XREAL_1:68; then
scf(r).(n+2)*c_d(r).(n+1)+c_d(r).n < rfs(r).(n+2)*c_d(r).(n+1)+c_d(r).n
by XREAL_1:8; then
A5: c_d(r).(n+2)<c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n by REAL_3:def 6; then
A6: c_d(r).(n+1)*c_d(r).(n+2) <
c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n) by A2,XREAL_1:68;
|. r - c_n(r).(n+1)/c_d(r).(n+1) .|
= |. (-1)*(c_n(r).(n+1)/c_d(r).(n+1) - r) .|
.= |. (-1)*((-1)|^n /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n))).|
by A1,Th15
.= |. (-1)*(-1)|^n /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)).|
.= |. (-1)|^(n+1) /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)).|
by NEWTON:6
.= |.(-1)|^(n+1).|/|.(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)).|
by COMPLEX1:67
.= 1/|.(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)).| by SERIES_2:1
.= 1/(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n))
by A2,A3,A5,COMPLEX1:43;
hence thesis by A6,A2,A3,XREAL_1:88;
end;
theorem Th22:
r is irrational implies
|. r*c_d(r).(n+1) - c_n(r).(n+1) .| < |. r*c_d(r).n - c_n(r).n .|
& |. r - c_n(r).(n+1)/c_d(r).(n+1) .| < |. r - c_n(r).n/c_d(r).n .|
proof
assume
A1: r is irrational; then
A2: r=(c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)
by Th14 .=(c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)*
(1/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n));
A3: c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n <> 0 by A1,Th12;
A4: r*c_d(r).(n+1)*rfs(r).(n+2) + r*c_d(r).n =
(c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)
*((1/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n))
*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) by A2
.= (c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n) * 1 by A3,XCMPLX_1:106
.= c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n;
A6: -(r*c_d(r).n - c_n(r).n)
= r*c_d(r).(n+1)*rfs(r).(n+2) - c_n(r).(n+1)*rfs(r).(n+2) by A4
.= rfs(r).(n+2)*(r*c_d(r).(n+1) - c_n(r).(n+1));
A7: 1 < rfs(r).(n+1+1) by A1,Th4;
A8: |. r*c_d(r).n-c_n(r).n .| = |.-(r*c_d(r).n-c_n(r).n).| by COMPLEX1:52
.= |. rfs(r).(n+2)*(r*c_d(r).(n+1) - c_n(r).(n+1)) .| by A6
.= |. rfs(r).(n+2) .|*|.(r*c_d(r).(n+1) - c_n(r).(n+1)) .| by COMPLEX1:65
.= rfs(r).(n+2) *|. r*c_d(r).(n+1) - c_n(r).(n+1) .| by A7,COMPLEX1:43;
A9: c_d(r).(n+1) >= 1 & c_d(r).n >=1 by A1,Th8;
|. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by A1,Th19; then
A11: r-c_n(r).(n+1)/c_d(r).(n+1) <> 0 by COMPLEX1:47;
A12: (r-c_n(r).(n+1)/c_d(r).(n+1)) * c_d(r).(n+1) =
r*c_d(r).(n+1) - c_n(r).(n+1)/c_d(r).(n+1) * c_d(r).(n+1)
.= r*c_d(r).(n+1) - c_n(r).(n+1) by A9,XCMPLX_1:87; then
A13: |. r*c_d(r).n-c_n(r).n .| > |. r*c_d(r).(n+1) - c_n(r).(n+1) .|
by A7,A8,A9,A11,COMPLEX1:47,XREAL_1:155;
A14: |. r - c_n(r).(n+1)/c_d(r).(n+1) .|
= |. r*c_d(r).(n+1)/c_d(r).(n+1)-c_n(r).(n+1)/c_d(r).(n+1) .|
by A9,XCMPLX_1:89
.= |. (r*c_d(r).(n+1)-c_n(r).(n+1))/c_d(r).(n+1) .|
.= |. (r*c_d(r).(n+1)-c_n(r).(n+1)).|/|.c_d(r).(n+1) .| by COMPLEX1:67
.= |. r*c_d(r).(n+1)-c_n(r).(n+1).|/c_d(r).(n+1) by A9,COMPLEX1:43;
A15: |. r - c_n(r).n/c_d(r).n .|
= |. r*c_d(r).n/c_d(r).n-c_n(r).n/c_d(r).n .| by A9,XCMPLX_1:89
.= |. (r*c_d(r).n-c_n(r).n)/c_d(r).n .|
.= |. (r*c_d(r).n-c_n(r).n).|/|.c_d(r).n .| by COMPLEX1:67
.= |. r*c_d(r).n-c_n(r).n.|/c_d(r).n by A9,COMPLEX1:43;
A16: |. r*c_d(r).(n+1)-c_n(r).(n+1).|/c_d(r).(n+1) <
|. r*c_d(r).n - c_n(r).n .| / c_d(r).(n+1) by A9,A13,XREAL_1:74;
|. r*c_d(r).n - c_n(r).n .| >= 0 by COMPLEX1:46; then
|. r*c_d(r).n - c_n(r).n .| / c_d(r).(n+1) <=
|. r*c_d(r).n - c_n(r).n .| / c_d(r).n by A1,Th7,A9,XREAL_1:118;
hence thesis by A7,A8,A9,A11,A12,A14,A15,A16,COMPLEX1:47,
XREAL_1:155,XXREAL_0:2;
end;
theorem Th23:
r is irrational & m > n implies
|. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).m/c_d(r).m .|
proof
assume that
A1: r is irrational and
A3: m > n;
defpred P[Nat] means
|. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).(n+1+$1)/c_d(r).(n+1+$1) .|;
A4: P[0] by A1,Th22;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
|.r-c_n(r).n/c_d(r).n.|
> |.r-c_n(r).(n+1+k+1)/c_d(r).(n+1+k+1).| by A1,Th22,XXREAL_0:2;
hence thesis;
end;
A8: for k be Nat holds P[k] from NAT_1:sch 2(A4,A5);
m - n > n-n by A3,XREAL_1:14; then
m - n >= 0+1 by INT_1:7; then
A9: (m - n) - 1 >= 1 - 1 by XREAL_1:9;
reconsider i = m - n - 1 as Integer;
i in NAT by A9,INT_1:3; then
reconsider i as Nat;
|. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).(n+1+i)/c_d(r).(n+1+i) .|
by A8;
hence thesis;
end;
::[Hardy&Wright] Ch.10 Th164
theorem Th24:
r is irrational implies
|. r - c_n(r).n/c_d(r).n .| < 1/c_d(r).n|^2
proof
assume
A1: r is irrational;
|. r - c_n(r).n/c_d(r).n .| < 1/c_d(r).n|^2
proof
per cases;
suppose
A3: n = 0; then
A6: |. r - c_n(r).n/c_d(r).n .| = |. r - c_n(r).0/1 .| by REAL_3:def 6
.= |. r - scf(r).0 .| by REAL_3:def 5 .= |.r-[\ rfs(r).0 /].|
by REAL_3:def 4
.= |.r-[\ r /].| by REAL_3:def 3 .= |. frac r .| by INT_1:def 8
.= frac r by ABSVALUE:def 1,INT_1:43;
1/c_d(r).n|^2 = 1/c_d(r).0|^2 by A3 .= 1/1|^2 by REAL_3:def 6
.= 1;
hence thesis by A6,INT_1:43;
end;
suppose
A8: n > 0;
set m = n - 1;
reconsider m as Nat by A8;
A10: c_d(r).(m+1) >= 1 by A1,Th8; then
c_d(r).(m+1)*c_d(r).(m+1) >= 1 by XREAL_1:159; then
A12: c_d(r).(m+1)|^2 >=1 by WSIERP_1:1;
c_d(r).(m+1+1)*c_d(r).(m+1)>=c_d(r).(m+1)*c_d(r).(m+1)
by A1,A10,Th7,XREAL_1:64; then
c_d(r).(m+1)*c_d(r).(m+2)>=c_d(r).(m+1)|^2 by WSIERP_1:1; then
1/(c_d(r).(m+1)*c_d(r).(m+2)) <= 1/c_d(r).(m+1)|^2
by A12,XREAL_1:85;
hence thesis by A1,XXREAL_0:2,Th21;
end;
end;
hence thesis;
end;
theorem
for S be Subset of RAT, r st r is irrational &
S = {p where p is Element of RAT:
|. r - p .| < 1/denominator(p)|^2 } holds
S is infinite
proof
let S be Subset of RAT, r;
assume that
A1: r is irrational and
A2: S = {p where p is Element of RAT:
|. r - p .| < 1/denominator(p)|^2 };
deffunc F(Nat) = c_n(r).($1 +1)/c_d(r).($1 +1);
consider f being Real_Sequence such that
A3: for n being Nat holds f.n = F(n) from SEQ_1:sch 1;
for o be Real st o in rng f holds o in S
proof
let o be Real;
assume o in rng f; then
consider i being object such that
A6: i in dom f and
A7: o = f.i by FUNCT_1:def 3;
reconsider i as Nat by A6;
A8: o = F(i) by A7,A3 .= c_n(r).(i+1)/c_d(r).(i +1);
A9: c_d(r).(i+1) in NAT by REAL_3:50;
A11: o in RAT by A8,A9,RAT_1:def 1;
reconsider o as Rational by A8,A9;
set cn = c_n(r).(i+1);
set cd = c_d(r).(i+1);
reconsider cd as Integer by A9;
o = cn/cd & cd <> 0 by A1,Th8,A8; then
consider m0 such that
cn = numerator(o)*m0 and
A14: cd = denominator(o)*m0 by RAT_1:28;
A19: cd|^2 = cd*cd by WSIERP_1:1 .= cd*(denominator(o)*m0) by A14
.= denominator(o)*denominator(o)*m0*m0 by A14
.= denominator(o)|^2*m0*m0 by WSIERP_1:1 .= denominator(o)|^2 * (m0*m0)
.= denominator(o)|^2 * m0|^2 by WSIERP_1:1;
A20: m0 <> 0 by A14,A1,Th8;
m0 * m0 = m0^2 by SQUARE_1:def 1; then
A22: m0^2 >= 0+ 1 by A20,SQUARE_1:12,INT_1:7;
A23: m0|^2 = m0*m0 by WSIERP_1:1 .= m0^2 by SQUARE_1:def 1;
denominator(o)|^2 <= denominator(o)|^2*m0^2 by A22,XREAL_1:151; then
1/denominator(o)|^2 >= 1/(denominator(o)|^2*m0^2) by XREAL_1:85; then
|.r-o.| < 1/denominator(o)|^2 by A1,A8,A19,Th24,A23,XXREAL_0:2;
hence thesis by A2,A11;
end; then
A28:rng f c= S;
reconsider f as Function of NAT, REAL;
A29:f is one-to-one
proof
for n1, n2 be object st n1 in dom f & n2 in dom f
& f.n1 = f.n2 holds n1 = n2
proof
let n1, n2 be object such that
A31: n1 in dom f and
A32: n2 in dom f and
A33: f.n1 = f.n2;
consider m1 be Nat such that
A34: n1 = m1 by A31;
consider m2 be Nat such that
A35: n2 = m2 by A32;
A36: f.m1 = f.n1 by A34 .= f.m2 by A33,A35;
A37: c_n(r).(m1 +1)/c_d(r).(m1 +1) = f.m1 by A3
.= F(m2) by A36,A3 .= c_n(r).(m2 +1)/c_d(r).(m2 +1);
assume n1 <> n2; then
per cases by A34,A35,XXREAL_0:1;
suppose m1 > m2; then
m1+1 > m2+1 by XREAL_1:8; then
|.r-c_n(r).(m1 +1)/c_d(r).(m1 +1).|
< |.r-c_n(r).(m2 +1)/c_d(r).(m2 +1).| by A1,Th23;
hence contradiction by A37;
end;
suppose m1 < m2; then
m1+1 < m2+1 by XREAL_1:8; then
|.r-c_n(r).(m1 +1)/c_d(r).(m1 +1).|
> |.r-c_n(r).(m2 +1)/c_d(r).(m2 +1).| by A1,Th23;
hence contradiction by A37;
end;
end;
hence thesis;
end;
dom f is infinite by FUNCT_2:def 1;
hence thesis by A28,A29,CARD_1:59;
end;
theorem
r is irrational implies cocf(r) is convergent & lim (cocf(r)) = r
proof
assume
A1: r is irrational;
A2: for p be Real st 0<p ex n st for m st n<=m holds |. cocf(r).m-r.| < p
proof
let p be Real;
assume
A3: p>0; then
A4: sqrt p > 0 by SQUARE_1:25;
A7: [/ 1/ sqrt p \] >= 1/sqrt p by INT_1:def 7;
[/ 1/ sqrt p \] > 0 by A4; then
[/ 1/ sqrt p \] in NAT by INT_1:3; then
consider n such that
A9: n = [/ 1/ sqrt p \];
A10: n > 0 by A4,A9;
for k be Nat st k >= n holds |. cocf(r).k-r.| < p
proof
let k be Nat;
assume
A12: k >= n;
A13: cocf(r).k =( c_n(r) /" c_d(r)).k by REAL_3:def 7
.= c_n(r).k * ((c_d(r))").k by SEQ_1:8
.= c_n(r).k /c_d(r).k by VALUED_1:10;
A14: |.cocf(r).k - r.| = |.-(cocf(r).k - r).| by COMPLEX1:52
.= |.r - c_n(r).k /c_d(r).k.| by A13;
(1/sqrt p)^2 = (sqrt p)"*(sqrt p)" by SQUARE_1:def 1
.= (sqrt p*sqrt p)" by XCMPLX_1:204 .= (sqrt p)^2" by SQUARE_1:def 1
.= p" by A3,SQUARE_1:def 2; then
n^2 >= p" by A4,A7,SQUARE_1:15,A9; then
A16: (n^2)" <= (p")" by A3,XREAL_1:85;
k^2 >= n^2 by A12,SQUARE_1:15; then
A18: (k^2)" <= (n^2)" by A10,SQUARE_1:12,XREAL_1:85;
A19: (c_d(r).k)^2 =(c_d(r).k)*(c_d(r).k) by SQUARE_1:def 1
.= c_d(r).k|^2 by WSIERP_1:1;
A20: (c_d(r).k)^2 >= k^2 by A1,Th10,SQUARE_1:15;
((c_d(r).k)^2)"=(c_d(r).k|^2)" by A19 .= 1/c_d(r).k|^2; then
1/c_d(r).k|^2 <= (k^2)"
by A12,A10,SQUARE_1:12,XREAL_1:85,A20; then
1/c_d(r).k|^2 <= (n^2)" by A18,XXREAL_0:2;
then 1/c_d(r).k|^2 <= p by A16,XXREAL_0:2;
hence thesis by XXREAL_0:2,A1,Th24,A14;
end;
hence thesis;
end;
cocf(r) is convergent by A2,SEQ_2:def 6;
hence thesis by A2,SEQ_2:def 7;
end;
begin
:: Proof of an existence of a solution of |. x*a -y .| < 1/t x < t
:: Dirichlet's argument
registration
cluster 1_greater for Nat;
existence
proof
take 2;
thus thesis;
end;
end;
reserve t for 1_greater Nat;
Lm1:
t > 0 & t > 1 & t" > 0 & t*t" = 1
proof
t is 1_greater;
hence thesis by XCMPLX_0:def 7;
end;
definition
let t;
func Equal_Div_interval(t) -> SetSequence of REAL means :Def1:
for n be Nat holds it.n = [. n/t, n/t + t" .[;
existence
proof
deffunc F(Element of NAT) = halfline_fin( $1 / t, $1 / t +t");
consider g be SetSequence of REAL such that
A1: for x be Element of NAT holds g.x = F(x) from FUNCT_2:sch 4;
take g;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let i1,i2 be SetSequence of REAL;
assume
A2: for n be Nat holds i1.n = [. n/t, n/t + t" .[;
assume
A3: for n be Nat holds i2.n = [. n/t, n/t + t" .[;
now
let n be Element of NAT;
i1.n = [. n/t, n/t + t" .[ by A2;
hence i1.n=i2.n by A3;
end;
hence i1=i2;
end;
end;
theorem Lm2:
[.0, (k+1)/t .[ \/ [. (k+1)/t, (k+2)/t .[ = [. 0, (k+2)/t .[
proof
0 <= (k+1)/t & (k+1)/t <= (k+2)/t
proof
k+1 <= (k+1) + 1 by XREAL_1:31;
hence thesis by XREAL_1:64;
end;
hence thesis by XXREAL_1:168;
end;
theorem Lm3:
(Partial_Union Equal_Div_interval(t)).i = [.0, (i+1)/t .[
proof
defpred P[Nat] means
(Partial_Union Equal_Div_interval(t)).$1 = [.0, ($1 +1)/t .[;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: (Partial_Union Equal_Div_interval(t)).k = [.0, (k+1)/t .[;
(Partial_Union Equal_Div_interval(t)).(k+1) =
(Partial_Union Equal_Div_interval(t)).k \/ (Equal_Div_interval(t)).(k+1)
by PROB_3:def 2 .=
[.0, (k+1)/t .[ \/ [. (k+1)/t, (k+1)/t + t" .[ by Def1,A2
.= [. 0, (k+2)/t .[ by Lm2;
hence thesis;
end;
(Partial_Union Equal_Div_interval(t)).0 = (Equal_Div_interval(t)).0
by PROB_3:def 2
.= [. 0/t,0/t + t" .[ by Def1
.= [. 0 ,t" .[; then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Lm4:
for r be Real, i be Nat st [\ r*t /] = i holds
r in (Equal_Div_interval(t)).i
proof
let r be Real;
let i be Nat;
assume [\ r*t /] = i; then
A3: i <= r*t & r*t -1 < i by INT_1:def 6; then
i/t <= r*t/t by XREAL_1:64; then
i*t" <= r*(t*t"); then
A6: i*t" <= r*1 by Lm1;
A7: r*t-1 + 1 < i + 1 by A3,XREAL_1:8;
0 < t" by Lm1; then
(r*t)*t" < (i+1)*t" by A7,XREAL_1:68;then
r*(t*t") < (i+1)*t"; then
r*1 < (i+1)/t by Lm1; then
r in [. i/t, i/t + t" .[ by A6,XXREAL_1:3;
hence thesis by Def1;
end;
theorem Lm5:
r1 in (Equal_Div_interval(t)).i & r2 in (Equal_Div_interval(t)).i
implies |. r1 - r2 .| < t"
proof
assume that
A2: r1 in (Equal_Div_interval(t)).i and
A3: r2 in (Equal_Div_interval(t)).i;
A5: r1 in [. i/t, i/t + t" .[ &
r1 in [. i/t, i/t + t" .[ & r2 in [. i/t, i/t + t" .[ by A2,A3,Def1;
then
A6: i/t <= r1 & i/t <= r2 & r1 < i/t +t" & r2 < i/t + t" by XXREAL_1:3;
per cases by XXREAL_0:1;
suppose r1=r2; then
|. r1 - r2 .| = 0 by ABSVALUE:2;
hence thesis by Lm1;
end;
suppose r1 > r2; then
A9: r1 - r2 > 0 by XREAL_1:50;
i*t" + t" - i*t" > r1 - r2 by A6,XREAL_1:14;
hence thesis by A9,ABSVALUE:def 1;
end;
suppose
A10: r2 > r1;
r2< i*t" + t" by A5,XXREAL_1:3; then
A12: i*t" + t" - r1 > r2 - r1 by XREAL_1:14;
i*t" <= r1 by A5,XXREAL_1:3; then
A13: i*t" + t" - i*t" >= i*t" + t" - r1 by XREAL_1:13;
|. r1 - r2 .| = -(r1 - r2) by A10,XREAL_1:49,ABSVALUE:def 1;
hence thesis by A13,A12,XXREAL_0:2;
end;
end;
theorem Lm6:
(Partial_Union Equal_Div_interval(t)).(t-1) = [.0,1.[
proof
A0: 0 <= t-1 by Lm1,XREAL_1:50;
(Partial_Union Equal_Div_interval(t)).(t-1)
= [. 0, (t-1 + 1)/t.[ by A0,Lm3
.= [. 0, 1 .[ by Lm1;
hence thesis;
end;
theorem Lm7:
for r be Real st r in [.0,1.[ holds
ex i be Nat st i <= t-1 & r in (Equal_Div_interval(t)).i
proof
let r be Real;
assume r in [.0,1.[; then
A2: r in (Partial_Union Equal_Div_interval(t)).(t-1) by Lm6;
A3: t-1 > 0 by Lm1,XREAL_1:50;
t -1 in NAT by A3,INT_1:3;
hence thesis by A2,PROB_3:13;
end;
theorem Lm8:
for r be Real, i be Nat st r in (Equal_Div_interval(t)).i holds
[\ r*t /] = i
proof
let r be Real;
let i be Nat;
assume
A1: r in (Equal_Div_interval(t)).i;
r in [. i/t, i/t + t" .[ by A1,Def1; then
A3: i/t <= r & r < i/t + t" by XXREAL_1:3; then
i*t"*t <= r*t by XREAL_1:64; then
i*(t"*t) <= r*t;then
A4: i*1 <= r*t by Lm1;
t > 0 by Lm1; then
r*t < (i + 1)*t" * t by A3,XREAL_1:68; then
r*t < (i + 1)*(t" * t); then
A6: r*t < (i + 1)*1 by Lm1;
i <= r*t & r*t - 1 < i + 1 - 1 by A4,A6,XREAL_1:9;
hence thesis by INT_1:def 6;
end;
theorem Lm9:
for r be Real st r in [.0,1.[ holds
ex i be Nat st i <= t-1 & [\ r*t /] = i
proof
let r be Real;
assume r in [.0,1.[; then
consider i be Nat such that
A2: i <= t-1 and
A3: r in (Equal_Div_interval(t)).i by Lm7;
thus thesis by A2,Lm8,A3;
end;
definition
let t,a;
func F_dp1(t,a) -> FinSequence of Segm t means :Def4:
len it = t+1 & for i st i in dom it holds
it.i = [\ (frac ((i -1)*a))*t /];
existence
proof
deffunc F(Nat) = [\ (frac (($1 -1)*a))*t /];
consider z being FinSequence such that
A1: len z = t+1 & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of Segm t
proof
A2: for y be object st y in rng z holds y in Segm t
proof
let y be object;
assume y in rng z; then
consider i be object such that
A4: i in dom z and
A5: y = z.i by FUNCT_1:def 3;
dom z = Seg len z by FINSEQ_1:def 3 .= Seg (t+1) by A1; then
consider i0 be Nat such that
A7: i0 = i and 1 <= i0 and i0 <= t+ 1 by A4;
reconsider i as Nat by A7;
A8: z.i = F(i) by A1,A4 .= [\ (frac ((i -1)*a))*t /];
0 <= frac ((i -1)*a) & frac ((i -1)*a) < 1 by INT_1:43; then
consider j be Nat such that
A10: j <= t-1 and
A11: [\ (frac ((i -1)*a))*t /] = j by Lm9,XXREAL_1:3;
j < t -1 + 1 by A10,XREAL_1:39;
hence thesis by A5,NAT_1:44,A11,A8;
end;
rng z c= Segm t by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of Segm t such that
A13:len z1 = t+1 and
A14:for i be Nat st i in dom z1 holds z1.i = [\ (frac ((i-1)*a))*t /] and
A15:len z2 = t+1 and
A16:for i be Nat st i in dom z2 holds z2.i = [\ (frac ((i-1)*a))*t /];
A17:dom z1 = Seg len z1 by FINSEQ_1:def 3.= dom z2 by A13,A15,FINSEQ_1:def 3;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A18: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus z1.x = [\ (frac ((x9 -1)*a))*t /] by A14,A18.= z2.x by A16,A17,A18;
end;
hence thesis by A17;
end;
end;
registration let t,a;
cluster rng F_dp1(t,a) -> non empty;
coherence
proof
A8: 1 < t +1 by Lm1,XREAL_1:39;
dom (F_dp1(t,a)) = Seg len F_dp1(t,a) by FINSEQ_1:def 3
.= Seg (t+1) by Def4; then
1 in dom (F_dp1(t,a)) by A8;
hence thesis by FUNCT_1:3;
end;
end;
theorem Lm10:
card rng(F_dp1(t,a)) in card dom(F_dp1(t,a))
proof
A1: card dom (F_dp1(t,a)) = card (Seg len F_dp1(t,a)) by FINSEQ_1:def 3
.= card (Seg (t+1)) by Def4 .= t + 1 by FINSEQ_1:57;
per cases;
suppose
A3: rng (F_dp1(t,a)) = Segm t;
card Segm t in nextcard card Segm t by CARD_1:18; then
card Segm t in card Segm(t+1) by NAT_1:42;
hence thesis by A1,A3;
end;
suppose
A6: rng (F_dp1(t,a)) c< Segm t;
Segm t c= Segm (t+1) by NAT_1:39,XREAL_1:31; then
rng (F_dp1(t,a)) c< Segm (t+1) by A6,XBOOLE_1:58; then
card rng (F_dp1(t,a)) in Segm card Segm (t+1) by CARD_2:48;
hence thesis by A1;
end;
end;
Th27:
ex x1, x2 st x1 in dom F_dp1(t,a) & x2 in dom F_dp1(t,a) &
x1 <> x2 & F_dp1(t,a).x1 = F_dp1(t,a).x2
proof
set A = dom(F_dp1(t,a));
set B = rng(F_dp1(t,a));
A1: card B in card A & B <> {} by Lm10;
defpred P[object,object] means
ex m1 being object st $1 in A &
$2=m1 & (F_dp1(t,a)).$1 = m1;
A2: for x being object st x in A ex y being object st y in B & P[x,y]
by FUNCT_1:3;
consider h be Function of A,B such that
A3: for x being object st x in A holds P[x,h.x] from FUNCT_2:sch 1(A2);
consider m1,m2 be object such that
A4: m1 in A and
A5: m2 in A and
A6: m1 <> m2 and
A7: h.m1 = h.m2 by A1,FINSEQ_4:65;
A9: P[m2,h.m2] by A3,A5;
P[m1,h.m1] by A3,A4; then
(F_dp1(t,a)).m1 = h.m2 by A7 .= (F_dp1(t,a)).m2 by A9;
hence thesis by A4,A5,A6;
end;
registration let t,a;
cluster F_dp1 (t,a) -> non one-to-one;
coherence
proof
assume
a1: F_dp1 (t,a) is one-to-one;
consider x1, x2 such that
A2: x1 in dom (F_dp1(t,a)) & x2 in dom (F_dp1(t,a)) &
x1 <> x2 & F_dp1(t,a).x1 = F_dp1(t,a).x2 by Th27;
thus thesis by a1,A2;
end;
end;
begin :: Proof of Dirichlet's Theorem
::[Baker] Chapter 6.1
::$N Dirichlet's approximation theorem
theorem
ex x,y be Integer st |. x*a - y .| < 1/t & 0 < x & x <= t
proof
consider x1, x2 be object such that
A1: x1 in dom (F_dp1(t,a)) and
A2: x2 in dom (F_dp1(t,a)) and
A3: x1 <> x2 and
A4: F_dp1(t,a).x1 = F_dp1(t,a).x2 by Th27;
A5: dom (F_dp1(t,a)) = Seg len F_dp1(t,a) by FINSEQ_1:def 3
.= Seg (t+1) by Def4;
consider n1 be Nat such that
A6: x1 = n1 and
A7: 1<= n1 and
A8: n1 <= t+1 by A1, A5;
reconsider x1 as Nat by A6;
consider n2 be Nat such that
A9: x2 = n2 and
A10: 1 <= n2 and
A11: n2 <= t+1 by A2,A5;
reconsider x2 as Nat by A9;
F_dp1(t,a).x1 in rng F_dp1(t,a) by A1,FUNCT_1:3;then
F_dp1(t,a).x1 in Segm t; then
F_dp1(t,a).x1 in { i where i is Nat : i < t } by AXIOMS:4; then
consider i be Nat such that
A13: F_dp1(t,a).x1 = i and i < t;
A14: [\ (frac ((x1 -1)*a))*t /] = i by Def4,A1,A13;
reconsider r1 = frac ((x1 -1)*a) as Real;
F_dp1(t,a).x2 in rng F_dp1(t,a) by A2,FUNCT_1:3;then
F_dp1(t,a).x2 in Segm t; then
F_dp1(t,a).x2 in { i where i is Nat : i < t } by AXIOMS:4; then
consider i2 be Nat such that
A16: F_dp1(t,a).x2 = i2 and i2 < t;
A17: [\ (frac ((x2 -1)*a))*t /] = i2 by Def4,A2,A16;
reconsider r2 = frac ((x2 -1)*a) as Real;
i = F_dp1(t,a).x1 by A13 .= F_dp1(t,a).x2 by A4 .= i2 by A16; then
A18: r1 in (Equal_Div_interval(t)).i & r2 in (Equal_Div_interval(t)).i
by A14,Lm4,A17;
A19: |. r1 - r2 .| < t" by Lm5,A18;
set m1 = x1 - 1;
set m2 = x2 - 1;
A20: r1 - r2 = m1*a - [\ m1*a /] - frac (m2*a) by INT_1:def 8
.= m1*a - [\ m1*a /] - (m2*a - [\ m2*a /]) by INT_1:def 8
.= (m1-m2)*a -( [\ m1*a /] - [\ m2*a /]);
per cases by A3,XXREAL_0:1;
suppose
A21: x1 > x2;
set x = m1 - m2;
set y = [\ m1*a /] - [\ m2*a /];
A24: x = x1 - x2;
A25: t+1 - x2 >= x1 - x2 by A6,A8,XREAL_1:13;
t+1 - 1 >= t + 1 - x2 by A9,A10,XREAL_1:10; then
A27: x <= t by A25,XXREAL_0:2;
A28: 0 < x by A21,XREAL_1:50,A24;
|. x*a -y .| < t" by Lm5,A18,A20;
hence thesis by A27,A28;
end;
suppose
A29: x1 < x2;
set x = m2 - m1;
set y = [\ m2*a /] - [\ m1*a /];
A32: x = x2 - x1;
A33: t+1 - x1 >= x2 - x1 by A9,A11,XREAL_1:13;
t+1 - 1 >= t + 1 - x1 by A6,A7,XREAL_1:10; then
A35: x <= t by A33,XXREAL_0:2;
A36: 0 < x by A29,XREAL_1:50,A32;
-(r1-r2) = x*a - y by A20; then
|. x*a -y .| < t" by A19,COMPLEX1:52;
hence thesis by A35,A36;
end;
end;