:: Introduction to {D}iophantine Approximation
:: by Yasushige Watase
::
:: Copyright (c) 2015-2019 Association of Mizar Users

:: Approximation an irrational by its simple continued fraction
theorem Th1: :: DIOPHAN1:1
for n being Nat
for r being Real holds
( r = (rfs r) . 0 & r = ((scf r) . 0) + (1 / ((rfs r) . 1)) & (rfs r) . n = ((scf r) . n) + (1 / ((rfs r) . (n + 1))) )
proof end;

theorem Th2: :: DIOPHAN1:2
for n being Nat
for r being Real st r is irrational holds
(rfs r) . n is irrational
proof end;

theorem Th3: :: DIOPHAN1:3
for n being Nat
for r being Real st r is irrational holds
( (rfs r) . n <> 0 & ((rfs r) . 1) * ((rfs r) . 2) <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 )
proof end;

theorem Th4: :: DIOPHAN1:4
for n being Nat
for r being Real st r is irrational holds
( (scf r) . n < (rfs r) . n & (rfs r) . n < ((scf r) . n) + 1 & 1 < (rfs r) . (n + 1) )
proof end;

theorem Th5: :: DIOPHAN1:5
for n being Nat
for r being Real st r is irrational holds
0 < (scf r) . (n + 1)
proof end;

Th6: for r being Real
for n being Nat holds (c_n r) . n is Integer

proof end;

registration
let r be Real;
let n be Nat;
cluster (c_n r) . n -> integer ;
coherence
(c_n r) . n is integer
by Th6;
end;

theorem Th7: :: DIOPHAN1:6
for r being Real st r is irrational holds
for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n
proof end;

theorem Th8: :: DIOPHAN1:7
for n being Nat
for r being Real st r is irrational holds
(c_d r) . n >= 1
proof end;

::[Hardy&Wright] Irrational case of Ch. 10 Th155
theorem :: DIOPHAN1:8
for n being Nat
for r being Real st r is irrational holds
(c_d r) . (n + 2) > (c_d r) . (n + 1)
proof end;

::[Hardy&Wright] Ch.10 Th156
theorem Th10: :: DIOPHAN1:9
for n being Nat
for r being Real st r is irrational holds
(c_d r) . n >= n
proof end;

::[Hardy&Wright] Ch.10 Th157
theorem :: DIOPHAN1:10
for n being Nat
for r being Real
for cn, cd being Integer st cn = (c_n r) . n & cd = (c_d r) . n & cn <> 0 holds
cn,cd are_coprime
proof end;

theorem Th12: :: DIOPHAN1:11
for n being Nat
for r being Real st r is irrational holds
( (((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 end;

theorem Th13: :: DIOPHAN1:12
for n being Nat
for r being Real st r is irrational holds
((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) > 0
proof end;

theorem Th14: :: DIOPHAN1:13
for n being Nat
for r being Real st r is irrational holds
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 end;

::[Hardy&Wright] Ch.10 Th158
theorem Th15: :: DIOPHAN1:14
for n being Nat
for r being Real st r is irrational holds
(((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 end;

theorem Th16: :: DIOPHAN1:15
for n being Nat
for r being Real st r is irrational & n is even & n > 0 holds
r > ((c_n r) . n) / ((c_d r) . n)
proof end;

theorem Th17: :: DIOPHAN1:16
for n being Nat
for r being Real st r is irrational & n is odd holds
r < ((c_n r) . n) / ((c_d r) . n)
proof end;

theorem :: DIOPHAN1:17
for n being Nat
for r being Real st r is irrational & n > 0 holds
|.(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 end;

theorem Th19: :: DIOPHAN1:18
for n being Nat
for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0
proof end;

theorem :: DIOPHAN1:19
for n being Nat
for r being Real st r is irrational holds
(c_d r) . (n + 2) >= 2 * ((c_d r) . n)
proof end;

theorem Th21: :: DIOPHAN1:20
for n being Nat
for r being Real st r is irrational holds
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / (((c_d r) . (n + 1)) * ((c_d r) . (n + 2)))
proof end;

theorem Th22: :: DIOPHAN1:21
for n being Nat
for r being Real st r is irrational holds
( |.((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 end;

theorem Th23: :: DIOPHAN1:22
for m, n being Nat
for r being Real st r is irrational & m > n holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . m) / ((c_d r) . m))).|
proof end;

::[Hardy&Wright] Ch.10 Th164
theorem Th24: :: DIOPHAN1:23
for n being Nat
for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
proof end;

theorem :: DIOPHAN1:24
for S being Subset of RAT
for r being Real st r is irrational & S = { p where p is Element of RAT : |.(r - p).| < 1 / (() |^ 2) } holds
S is infinite
proof end;

theorem :: DIOPHAN1:25
for r being Real st r is irrational holds
( cocf r is convergent & lim (cocf r) = r )
proof end;

:: Proof of an existence of a solution of |. x*a -y .| < 1/t x < t
:: Dirichlet's argument
registration
existence
ex b1 being Nat st b1 is 1 _greater
proof end;
end;

Lm1: for t being 1 _greater Nat holds
( t > 0 & t > 1 & t " > 0 & t * (t ") = 1 )

proof end;

definition
let t be 1 _greater Nat;
func Equal_Div_interval t -> SetSequence of REAL means :Def1: :: DIOPHAN1:def 1
for n being Nat holds it . n = [.(n / t),((n / t) + (t ")).[;
existence
ex b1 being SetSequence of REAL st
for n being Nat holds b1 . n = [.(n / t),((n / t) + (t ")).[
proof end;
uniqueness
for b1, b2 being SetSequence of REAL st ( for n being Nat holds b1 . n = [.(n / t),((n / t) + (t ")).[ ) & ( for n being Nat holds b2 . n = [.(n / t),((n / t) + (t ")).[ ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Equal_Div_interval DIOPHAN1:def 1 :
for t being 1 _greater Nat
for b2 being SetSequence of REAL holds
( b2 = Equal_Div_interval t iff for n being Nat holds b2 . n = [.(n / t),((n / t) + (t ")).[ );

theorem Lm2: :: DIOPHAN1:26
for k being Nat
for t being 1 _greater Nat holds [.0,((k + 1) / t).[ \/ [.((k + 1) / t),((k + 2) / t).[ = [.0,((k + 2) / t).[
proof end;

theorem Lm3: :: DIOPHAN1:27
for i being Nat
for t being 1 _greater Nat holds . i = [.0,((i + 1) / t).[
proof end;

theorem Lm4: :: DIOPHAN1:28
for t being 1 _greater Nat
for r being Real
for i being Nat st [\(r * t)/] = i holds
r in . i
proof end;

theorem Lm5: :: DIOPHAN1:29
for i being Nat
for r1, r2 being Real
for t being 1 _greater Nat st r1 in . i & r2 in . i holds
|.(r1 - r2).| < t "
proof end;

theorem Lm6: :: DIOPHAN1:30
for t being 1 _greater Nat holds . (t - 1) = [.0,1.[
proof end;

theorem Lm7: :: DIOPHAN1:31
for t being 1 _greater Nat
for r being Real st r in [.0,1.[ holds
ex i being Nat st
( i <= t - 1 & r in . i )
proof end;

theorem Lm8: :: DIOPHAN1:32
for t being 1 _greater Nat
for r being Real
for i being Nat st r in . i holds
[\(r * t)/] = i
proof end;

theorem Lm9: :: DIOPHAN1:33
for t being 1 _greater Nat
for r being Real st r in [.0,1.[ holds
ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i )
proof end;

definition
let t be 1 _greater Nat;
let a be Real;
func F_dp1 (t,a) -> FinSequence of Segm t means :Def4: :: DIOPHAN1:def 2
( len it = t + 1 & ( for i being Nat st i in dom it holds
it . i = [\((frac ((i - 1) * a)) * t)/] ) );
existence
ex b1 being FinSequence of Segm t st
( len b1 = t + 1 & ( for i being Nat st i in dom b1 holds
b1 . i = [\((frac ((i - 1) * a)) * t)/] ) )
proof end;
uniqueness
for b1, b2 being FinSequence of Segm t st len b1 = t + 1 & ( for i being Nat st i in dom b1 holds
b1 . i = [\((frac ((i - 1) * a)) * t)/] ) & len b2 = t + 1 & ( for i being Nat st i in dom b2 holds
b2 . i = [\((frac ((i - 1) * a)) * t)/] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines F_dp1 DIOPHAN1:def 2 :
for t being 1 _greater Nat
for a being Real
for b3 being FinSequence of Segm t holds
( b3 = F_dp1 (t,a) iff ( len b3 = t + 1 & ( for i being Nat st i in dom b3 holds
b3 . i = [\((frac ((i - 1) * a)) * t)/] ) ) );

registration
let t be 1 _greater Nat;
let a be Real;
cluster rng (F_dp1 (t,a)) -> non empty ;
coherence
not rng (F_dp1 (t,a)) is empty
proof end;
end;

theorem Lm10: :: DIOPHAN1:34
for a being Real
for t being 1 _greater Nat holds card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))
proof end;

Th27: for a being Real
for t being 1 _greater Nat ex x1, x2 being object 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 end;

registration
let t be 1 _greater Nat;
let a be Real;
cluster F_dp1 (t,a) -> non one-to-one ;
coherence
not F_dp1 (t,a) is one-to-one
proof end;
end;

::[Baker] Chapter 6.1
:: Dirichlet's approximation theorem
theorem :: DIOPHAN1:35
for a being Real
for t being 1 _greater Nat ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )
proof end;