:: Introduction to {D}iophantine Approximation -- Part 2 :: by Yasushige Watase :: :: Received November 29, 2017 :: Copyright (c) 2017-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, CARD_1, FUNCT_1, RELAT_1, ARYTM_3, SUBSET_1, ZFMISC_1, ARYTM_1, XXREAL_0, NAT_1, INT_1, REAL_1, COMPLEX1, SQUARE_1, IRRAT_1, RAT_1, XBOOLE_0, TARSKI, PRE_POLY, NEWTON, FINSET_1, INT_2, XCMPLX_0, FINSEQ_1, REAL_3, FUNCT_3, BORSUK_5, ORDINAL1, DIOPHAN2; notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, NUMBERS, XXREAL_2, ORDINAL1, BORSUK_5, XCMPLX_0, QUIN_1, ZFMISC_1, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, FUNCT_2, XREAL_0, COMPLEX1, IRRAT_1, REAL_3, NEWTON, SQUARE_1, INT_1, INT_2, FINSET_1, RAT_1, PRE_POLY, BINOP_1; constructors REAL_1, PROB_1, RELSET_1, XXREAL_2, BORSUK_5, QUIN_1, ALGSTR_0, SQUARE_1, NAT_D, NEWTON, PRE_POLY, PYTHTRIP, REAL_3; registrations XBOOLE_0, XREAL_0, ORDINAL1, NAT_1, INT_1, FINSET_1, XXREAL_0, NEWTON, CARD_1, VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, RAT_1, SQUARE_1, QUIN_1, XXREAL_2, ABSVALUE, NEWTON03, PYTHTRIP, MEMBERED, REAL_3, BORSUK_5, DIOPHAN1, BORSUK_7, COMPLEX1, FOMODEL0; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Preliminaries reserve r1,r2,r3 for non negative Real; reserve n,m1 for Nat; reserve s for Real; reserve cn,cd,i1,j1 for Integer; reserve r for irrational Real; reserve q for Rational; theorem :: DIOPHAN2:1 r1*r2 <= r3 implies r1 <= sqrt r3 or r2 <= sqrt r3; theorem :: DIOPHAN2:2 sqrt(r1*r2)=(r1+r2)/2 iff r1 = r2; theorem :: DIOPHAN2:3 r1*r2=((r1+r2)/2)^2 iff r1 = r2; theorem :: DIOPHAN2:4 for i1,j1 st i1,j1 are_coprime holds ex s,t be Integer st s*i1+t*j1=1; theorem :: DIOPHAN2:5 1 < s & s+1/s < sqrt 5 implies s < (sqrt 5+1)/2 & 1/s > (sqrt 5 -1)/2; theorem :: DIOPHAN2:6 q=i1/m1 & m1<>0 & i1,m1 are_coprime implies i1=numerator(q) & m1=denominator(q); definition let f be Function; func ZeroPointSet f -> set equals :: DIOPHAN2:def 1 dom f \ support f; end; theorem :: DIOPHAN2:7 for f being Function, o1,o2 being object holds o1 in ZeroPointSet f iff o1 in dom f & f.o1 = 0; begin :: The theorem of Hurwitz registration let r be irrational Real; let n be Nat; cluster c_d(r).n -> positive natural; end; :: Approximation an irrational by its simple continued fraction theorem :: DIOPHAN2:8 for r,n st n > 1 & |.r-c_n(r).n/c_d(r).n.|>= 1/(sqrt 5*c_d(r).n|^2) & |.r-c_n(r).(n+1)/c_d(r).(n+1).| >= 1/(sqrt 5 * c_d(r).(n+1)|^2) holds sqrt 5 > c_d(r).(n+1)/c_d(r).n + 1/(c_d(r).(n+1)/c_d(r).n); theorem :: DIOPHAN2:9 cn = c_n(r).n & cd = c_d(r).n implies cn,cd are_coprime; ::Hardy&Wright Th196 theorem :: DIOPHAN2:10 n > 1 implies |.r-c_n(r).n/c_d(r).n.| < 1/(sqrt 5 * c_d(r).n|^2) or |.r-c_n(r).(n+1)/c_d(r).(n+1).| < 1/(sqrt 5*c_d(r).(n+1)|^2) or |.r-c_n(r).(n+2)/c_d(r).(n+2).| < 1/(sqrt 5*c_d(r).(n+2)|^2); definition let r; func HWZSet(r) -> Subset of RAT equals :: DIOPHAN2:def 2 {p where p is Rational: |.r-p.| < 1/(sqrt 5 * denominator(p)|^2)}; end; definition let r; func HWZSet1(r) -> Subset of NAT equals :: DIOPHAN2:def 3 {x where x is Nat : ex p be Rational st p in HWZSet(r) & x = denominator(p)}; end; definition func TRANQN -> Function of RAT, NAT means :: DIOPHAN2:def 4 for x be Rational holds it.x = denominator(x); end; theorem :: DIOPHAN2:11 TRANQN.:HWZSet(r) = HWZSet1(r); theorem :: DIOPHAN2:12 HWZSet(r) is finite implies HWZSet1(r) is finite; registration let r; cluster HWZSet1(r) -> non empty; end; theorem :: DIOPHAN2:13 for h being Nat st h in HWZSet1(r) holds h > 0; registration let r; cluster HWZSet1(r) -> infinite; end; :: The theorem of Hurwitz :: Hardy&Wright Th194 ::$N Hurwitz's theorem (number theory) theorem :: DIOPHAN2:14 for r holds { q : |.r-q.| < 1/(sqrt 5 * denominator(q)|^2) } is infinite; reserve c0,c1,c2,u,a0,b0 for Real; definition let a0,b0,c0 be Real; func LF(a0,b0,c0) -> Function of [:INT,INT:],REAL means :: DIOPHAN2:def 5 for x,y be Integer holds it.(x,y) = a0*x + b0*y + c0; end; begin :: lemma 2.1 of chapter 2 p16 of Niven[1] theorem :: DIOPHAN2:15 for rh0 be Element of REAL,p,q be Integer st p,q are_coprime holds ex x,y be Element of INT st |. p*x - q*y +rh0 .| <= 1/2; reserve a,b for Real; reserve n for Integer; theorem :: DIOPHAN2:16 n <= b & b <= n+1 implies |.n-b.|*|.n+1-b.| <=1/4; theorem :: DIOPHAN2:17 a is not Integer & (n=[\a/] or n=[\a/]+1) implies |.a-n.|<1; theorem :: DIOPHAN2:18 |.n-a.|*|.n+1-a.| <=1/4 & |.n-b.|*|.n+1-b.| <=1/4 implies |.n-a.|*|.n-b.| <= 1/4 or |.n+1-a.|*|.n+1-b.| <=1/4; theorem :: DIOPHAN2:19 |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.| <= |.a-b.|^2/4 implies |.a-n.|*|.b-n.|<=|.a-b.|/2 or |.a-n-1.|*|.b-n-1.|<=|.a-b.|/2; theorem :: DIOPHAN2:20 (n-b)*(n+1-a)> 0 & (a-n)*(n+1-b)> 0 implies (n-b)*(n+1-a)+(a-n)*(n+1-b)=a-b & |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.| <= |.a-b.|^2/4; ::b< n< a< n+1 => |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4 theorem :: DIOPHAN2:21 b0 & (b-n)*(n+1-a)> 0 implies (n-a)*(n+1-b)+(b-n)*(n+1-a) = b-a & |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4; :: n |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4 theorem :: DIOPHAN2:23 n+1 < b & n < a & a < n + 1 implies |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.| <= |.a - b.|^2/4; theorem :: DIOPHAN2:24 a is not Integer & [\a/]<=b & b<=[\a/]+1 implies ex u be Integer st |.a-u.|<1 & |.a-u.|*|.b-u.|<= 1/4; theorem :: DIOPHAN2:25 |.a-[\a/].|*|.b-[\a/].| >= |.a-b.|/2 & |.a-([\a/]+1).|*|.b-([\a/]+1).| >= |.a-b.|/2 implies a is Integer or [\a/]<=b; theorem :: DIOPHAN2:26 a is not Integer & [\a/] > b implies ex u be Integer st |.a-u.|<1 & |.a-u.|*|.b-u.| < |.a-b.|/2; theorem :: DIOPHAN2:27 |.a-[\a/].|*|.b-[\a/].| >= |.a-b.|/2 & |.a-([\a/]+1).|*|.b-([\a/]+1).| >= |.a-b.|/2 implies a is Integer or [\a/]+1 >= b; theorem :: DIOPHAN2:28 a is not Integer & [\a/]+1 [\r1/]+1 & q in HWZSet(r); theorem :: DIOPHAN2:31 |.a1*b2-a2*b1.|<>0 & q <> q1 & a2*denominator(q)+b2*numerator(q)=0 implies a2*denominator(q1)+b2*numerator(q1)<>0; theorem :: DIOPHAN2:32 for a1,a2,b1,b2,r1 st |.a1*b2-a2*b1.|<>0 holds ex q be Element of RAT st denominator(q) > [\r1/]+1 & q in HWZSet(r) & a2*denominator(q)+b2*numerator(q) <> 0; theorem :: DIOPHAN2:33 for a1,b1 be Real, n1,d1 be Integer st d1 > 0 & |.a1/b1+n1/d1.|<1/(sqrt 5 * d1|^2) holds ex d be Real st n1/d1 = -a1/b1 + d/d1|^2 & |.d.| < 1/sqrt 5; :: Theorem 2.3 of chapter 2 p18 of Niven[1] theorem :: DIOPHAN2:34 |.a1*b2-a2*b1.|<>0 & a1/b1 is irrational implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<|.a1*b2-a2*b1.|/4 & |.LF(a1,b1,c1).(x,y).| < eps; theorem :: DIOPHAN2:35 |.a1*b2-a2*b1.|<>0 & a2/b2 is irrational implies ex x,y be Element of INT st |.LF(a2,b2,c2).(x,y).|*|.LF(a1,b1,c1).(x,y).|<|.a1*b2-a2*b1.|/4 & |.LF(a2,b2,c2).(x,y).| < eps; theorem :: DIOPHAN2:36 ZeroPointSet( LF(a1,b1,c1))<>{} implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4; theorem :: DIOPHAN2:37 ZeroPointSet( LF(a2,b2,c2))<>{} implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4; theorem :: DIOPHAN2:38 |.a1*b2-a2*b1.|<>0 & b1 <> 0 & a1/b1 is rational implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4; theorem :: DIOPHAN2:39 |.a1*b2-a2*b1.|<>0 & b2 <> 0 & a2/b2 is rational implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4; theorem :: DIOPHAN2:40 |.a1*b2-a2*b1.|<>0 & b1 = 0 implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4; ::Hardy&Wright Th455 theorem :: DIOPHAN2:41 |.a1*b2-a2*b1.|<>0 implies ex x,y be Element of INT st |.LF(a1,b1,c1).(x,y).|*|.LF(a2,b2,c2).(x,y).|<=|.a1*b2-a2*b1.|/4;