:: Introduction to {D}iophantine Approximation
:: by Yasushige Watase
::
:: Received April 19, 2015
:: Copyright (c) 2015-2021 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 / ((denominator p) |^ 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

cluster ordinal natural V19() V20() ext-real non negative integer dim-like finite cardinal non irrational 1 _greater for set ;

existence
ex b₁ being Nat st b₁ 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 b₁ being SetSequence of REAL st
for n being Nat holds b₁ . n = [.(n / t),((n / t) + (t ")).[

proof end;

uniqueness
for b₁, b₂ being SetSequence of REAL st ( for n being Nat holds b₁ . n = [.(n / t),((n / t) + (t ")).[ ) & ( for n being Nat holds b₂ . n = [.(n / t),((n / t) + (t ")).[ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Equal_Div_interval DIOPHAN1:def 1 :
for t being 1 _greater Nat
for b₂ being SetSequence of REAL holds
( b₂ = Equal_Div_interval t iff for n being Nat holds b₂ . 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 (Partial_Union (Equal_Div_interval t)) . 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 (Equal_Div_interval t) . 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 (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i holds
|.(r1 - r2).| < t "

proof end;

theorem Lm6: :: DIOPHAN1:30

for t being 1 _greater Nat holds (Partial_Union (Equal_Div_interval t)) . (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 (Equal_Div_interval t) . i )

proof end;

theorem Lm8: :: DIOPHAN1:32

for t being 1 _greater Nat
for r being Real
for i being Nat st r in (Equal_Div_interval t) . 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 b₁ being FinSequence of Segm t st
( len b₁ = t + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = [\((frac ((i - 1) * a)) * t)/] ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of Segm t st len b₁ = t + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = [\((frac ((i - 1) * a)) * t)/] ) & len b₂ = t + 1 & ( for i being Nat st i in dom b₂ holds
b₂ . i = [\((frac ((i - 1) * a)) * t)/] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines F_dp1 DIOPHAN1:def 2 :
for t being 1 _greater Nat
for a being Real
for b₃ being FinSequence of Segm t holds
( b₃ = F_dp1 (t,a) iff ( len b₃ = t + 1 & ( for i being Nat st i in dom b₃ holds
b₃ . 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;