:: 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 b₁ being Function of RAT,NAT st
for x being Rational holds b₁ . x = denominator x

proof end;

uniqueness
for b₁, b₂ being Function of RAT,NAT st ( for x being Rational holds b₁ . x = denominator x ) & ( for x being Rational holds b₂ . x = denominator x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3A defines TRANQN DIOPHAN2:def 4 :
for b₁ being Function of RAT,NAT holds
( b₁ = TRANQN iff for x being Rational holds b₁ . 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
:: 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 b₁ being Function of [:INT,INT:],REAL st
for x, y being Integer holds b₁ . (x,y) = ((a0 * x) + (b0 * y)) + c0

proof end;

uniqueness
for b₁, b₂ being Function of [:INT,INT:],REAL st ( for x, y being Integer holds b₁ . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) & ( for x, y being Integer holds b₂ . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines LF DIOPHAN2:def 5 :
for a0, b0, c0 being Real
for b₄ being Function of [:INT,INT:],REAL holds
( b₄ = LF (a0,b0,c0) iff for x, y being Integer holds b₄ . (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;