:: Introduction to {D}iophantine Approximation -- Part 2
:: by Yasushige Watase
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem Th18: :: DIOPHAN2:1
for r1, r2, r3 being non negative Real holds
( not r1 * r2 <= r3 or r1 <= sqrt r3 or r2 <= sqrt r3 )
proof end;

theorem Th19: :: DIOPHAN2:2
for r1, r2 being non negative Real holds
( sqrt (r1 * r2) = (r1 + r2) / 2 iff r1 = r2 )
proof end;

theorem Th20: :: DIOPHAN2:3
for r1, r2 being non negative Real holds
( r1 * r2 = ((r1 + r2) / 2) ^2 iff r1 = r2 )
proof end;

theorem Th15: :: DIOPHAN2:4
for i1, j1 being Integer st i1,j1 are_coprime holds
ex s, t being Integer st (s * i1) + (t * j1) = 1
proof end;

sqrt 5 > sqrt (2 ^2)
by SQUARE_1:27;

then SQRT2: 2 < sqrt 5
by SQUARE_1:22;

then SQRT3: 1 / (sqrt 5) < 1 / 2
by XREAL_1:76;

theorem Th1: :: DIOPHAN2:5
for s being Real st 1 < s & s + (1 / s) < sqrt 5 holds
( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )
proof end;

theorem Th8: :: DIOPHAN2:6
for m1 being Nat
for i1 being Integer
for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds
( i1 = numerator q & m1 = denominator q )
proof end;

definition
let f be Function;
func ZeroPointSet f -> set equals :: DIOPHAN2:def 1
(dom f) \ (support f);
correctness
coherence
(dom f) \ (support f) is set ;
;
end;

:: deftheorem defines ZeroPointSet DIOPHAN2:def 1 :
for f being Function holds ZeroPointSet f = (dom f) \ (support f);

theorem Th13: :: DIOPHAN2:7
for f being Function
for o1, o2 being object holds
( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )
proof end;

registration
let r be irrational Real;
let n be Nat;
cluster (c_d r) . n -> natural positive ;
coherence
( (c_d r) . n is positive & (c_d r) . n is natural )
proof end;
end;

:: Approximation an irrational by its simple continued fraction
theorem Th3: :: DIOPHAN2:8
for r being irrational Real
for n being Nat 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)))
proof end;

theorem Th4: :: DIOPHAN2:9
for n being Nat
for cn, cd being Integer
for r being irrational Real st cn = (c_n r) . n & cd = (c_d r) . n holds
cn,cd are_coprime
proof end;

::Hardy&Wright Th196
theorem Th5: :: DIOPHAN2:10
for n being Nat
for r being irrational Real holds
( not n > 1 or |.(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)) )
proof end;

definition
let r be irrational Real;
func HWZSet r -> Subset of RAT equals :: DIOPHAN2:def 2
 { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;
coherence
{ p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } is Subset of RAT
proof end;
end;

:: deftheorem defines HWZSet DIOPHAN2:def 2 :
for r being irrational Real holds HWZSet r = { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;

definition
let r be irrational Real;
func HWZSet1 r -> Subset of NAT equals :: DIOPHAN2:def 3
 { x where x is Nat : ex p being Rational st
( p in HWZSet r & x = denominator p ) } ;
coherence
{ x where x is Nat : ex p being Rational st
( p in HWZSet r & x = denominator p ) } is Subset of NAT
proof end;
end;

:: deftheorem defines HWZSet1 DIOPHAN2:def 3 :
for r being irrational Real holds HWZSet1 r = { x where x is Nat : ex p being Rational st
( p in HWZSet r & x = denominator p ) } ;

definition
func TRANQN -> Function of RAT,NAT means :Def3A: :: DIOPHAN2:def 4
 for x being Rational holds it . x = denominator x;
existence
ex b1 being Function of RAT,NAT st
for x being Rational holds b1 . x = denominator x
proof end;
uniqueness
for b1, b2 being Function of RAT,NAT st ( for x being Rational holds b1 . x = denominator x ) & ( for x being Rational holds b2 . x = denominator x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3A defines TRANQN DIOPHAN2:def 4 :
for b1 being Function of RAT,NAT holds
( b1 = TRANQN iff for x being Rational holds b1 . x = denominator x );

theorem Th6: :: DIOPHAN2:11
for r being irrational Real holds TRANQN .: (HWZSet r) = HWZSet1 r
proof end;

theorem Th7: :: DIOPHAN2:12
for r being irrational Real st HWZSet r is finite holds
HWZSet1 r is finite
proof end;

registration
let r be irrational Real;
cluster HWZSet1 r -> non empty ;
coherence
not HWZSet1 r is empty
proof end;
end;

theorem Th10: :: DIOPHAN2:13
for r being irrational Real
for h being Nat st h in HWZSet1 r holds
h > 0
proof end;

registration
let r be irrational Real;
cluster HWZSet1 r -> infinite ;
coherence
not HWZSet1 r is finite
proof end;
end;

:: The theorem of Hurwitz
:: Hardy&Wright Th194
:: WP: Hurwitz's theorem (number theory)
theorem :: DIOPHAN2:14
for r being irrational Real holds { q where q is Rational : |.(r - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2)) } is infinite
proof end;

definition
let a0, b0, c0 be Real;
func LF (a0,b0,c0) -> Function of [:INT,INT:],REAL means :Def4: :: DIOPHAN2:def 5
 for x, y being Integer holds it . (x,y) = ((a0 * x) + (b0 * y)) + c0;
existence
ex b1 being Function of [:INT,INT:],REAL st
for x, y being Integer holds b1 . (x,y) = ((a0 * x) + (b0 * y)) + c0
proof end;
uniqueness
for b1, b2 being Function of [:INT,INT:],REAL st ( for x, y being Integer holds b1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) & ( for x, y being Integer holds b2 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines LF DIOPHAN2:def 5 :
for a0, b0, c0 being Real
for b4 being Function of [:INT,INT:],REAL holds
( b4 = LF (a0,b0,c0) iff for x, y being Integer holds b4 . (x,y) = ((a0 * x) + (b0 * y)) + c0 );

:: lemma 2.1 of chapter 2 p16 of Niven[1]
theorem Th16: :: DIOPHAN2:15
for rh0 being Element of REAL
for p, q being Integer st p,q are_coprime holds
ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2
proof end;

theorem Th17: :: DIOPHAN2:16
for b being Real
for n being Integer st n <= b & b <= n + 1 holds
|.(n - b).| * |.((n + 1) - b).| <= 1 / 4
proof end;

theorem Th21: :: DIOPHAN2:17
for a being Real
for n being Integer st a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) holds
|.(a - n).| < 1
proof end;

theorem Th22: :: DIOPHAN2:18
for a, b being Real
for n being Integer st |.(n - a).| * |.((n + 1) - a).| <= 1 / 4 & |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 & not |.(n - a).| * |.(n - b).| <= 1 / 4 holds
|.((n + 1) - a).| * |.((n + 1) - b).| <= 1 / 4
proof end;

theorem Th23: :: DIOPHAN2:19
for a, b being Real
for n being Integer holds
( not ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 or |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 )
proof end;

theorem Th24: :: DIOPHAN2:20
for a, b being Real
for n being Integer st (n - b) * ((n + 1) - a) > 0 & (a - n) * ((n + 1) - b) > 0 holds
( ((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 )
proof end;

::b< n< a< n+1 => |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4
theorem Th25: :: DIOPHAN2:21
for a, b being Real
for n being Integer st b < n & n < a & a < n + 1 holds
((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
proof end;

theorem Th26: :: DIOPHAN2:22
for a, b being Real
for n being Integer st (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 holds
( ((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 )
proof end;

:: n <a<n+1 <b => |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4
theorem Th27: :: DIOPHAN2:23
for a, b being Real
for n being Integer st n + 1 < b & n < a & a < n + 1 holds
((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
proof end;

theorem Th28: :: DIOPHAN2:24
for a, b being Real st a is not Integer & [\a/] <= b & b <= [\a/] + 1 holds
ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )
proof end;

theorem Th32: :: DIOPHAN2:25
for a, b being Real st |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 & a is not Integer holds
[\a/] <= b
proof end;

theorem Th33: :: DIOPHAN2:26
for a, b being Real st a is not Integer & [\a/] > b holds
ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )
proof end;

theorem Th37: :: DIOPHAN2:27
for a, b being Real st |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 & a is not Integer holds
[\a/] + 1 >= b
proof end;

theorem Th39: :: DIOPHAN2:28
for a, b being Real st a is not Integer & [\a/] + 1 < b holds
ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )
proof end;

:: lemma 2.2 of chapter 2 p16 of Niven
theorem Th41: :: DIOPHAN2:29
for a, b being Real ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )
proof end;

theorem Th42: :: DIOPHAN2:30
for r being irrational Real
for r1 being non negative Real ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r )
proof end;

theorem Th43: :: DIOPHAN2:31
for a1, a2, b1, b2 being Element of REAL
for q, q1 being Element of RAT st |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 holds
(a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
proof end;

theorem Th44: :: DIOPHAN2:32
for r being irrational Real
for a1, a2, b1, b2 being Element of REAL
for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds
ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )
proof end;

theorem Th45: :: DIOPHAN2:33
for a1, b1 being Real
for n1, d1 being Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) holds
ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )
proof end;

:: Theorem 2.3 of chapter 2 p18 of Niven[1]
theorem Th46: :: DIOPHAN2:34
for a1, a2, b1, b2, c1, c2 being Element of REAL
for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a1 / b1 is irrational holds
ex x, y being 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 )
proof end;

theorem Th47: :: DIOPHAN2:35
for a1, a2, b1, b2, c1, c2 being Element of REAL
for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational holds
ex x, y being 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 )
proof end;

theorem Th48: :: DIOPHAN2:36
for a1, a2, b1, b2, c1, c2 being Element of REAL st ZeroPointSet (LF (a1,b1,c1)) <> {} holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;

theorem Th49: :: DIOPHAN2:37
for a1, a2, b1, b2, c1, c2 being Element of REAL st ZeroPointSet (LF (a2,b2,c2)) <> {} holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;

theorem Th50: :: DIOPHAN2:38
for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 <> 0 & a1 / b1 is rational holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;

theorem Th51: :: DIOPHAN2:39
for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & a2 / b2 is rational holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;

theorem Th52: :: DIOPHAN2:40
for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 = 0 holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;

::Hardy&Wright Th455
theorem :: DIOPHAN2:41
for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
proof end;