:: by Yasushige Watase

::

:: Received April 19, 2015

:: Copyright (c) 2015-2018 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))) )

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 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 )

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) )

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;

Th6: for r being Real

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

proof end;

::[Hardy&Wright] Irrational case of Ch. 10 Th155

::[Hardy&Wright] Ch.10 Th156

::[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

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 )

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

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))

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)))

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)

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)

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)))).|

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

for r being Real st r is irrational holds

|.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0

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)))

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))).| )

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))).|

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)

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

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;

:: Proof of an existence of a solution of |. x*a -y .| < 1/t x < t

:: Dirichlet's argument

:: Dirichlet's argument

registration

ex b_{1} being Nat st b_{1} is 1 _greater
end;

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

existence ex b

proof 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;

ex b_{1} being SetSequence of REAL st

for n being Nat holds b_{1} . n = [.(n / t),((n / t) + (t ")).[

for b_{1}, b_{2} being SetSequence of REAL st ( for n being Nat holds b_{1} . n = [.(n / t),((n / t) + (t ")).[ ) & ( for n being Nat holds b_{2} . n = [.(n / t),((n / t) + (t ")).[ ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = [.(n / t),((n / t) + (t ")).[;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Equal_Div_interval DIOPHAN1:def 1 :

for t being 1 _greater Nat

for b_{2} being SetSequence of REAL holds

( b_{2} = Equal_Div_interval t iff for n being Nat holds b_{2} . n = [.(n / t),((n / t) + (t ")).[ );

for t being 1 _greater Nat

for b

( b

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).[

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).[

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

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 "

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 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 )

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

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 )

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;

ex b_{1} being FinSequence of Segm t st

( len b_{1} = t + 1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = [\((frac ((i - 1) * a)) * t)/] ) )

for b_{1}, b_{2} being FinSequence of Segm t st len b_{1} = t + 1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = [\((frac ((i - 1) * a)) * t)/] ) & len b_{2} = t + 1 & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = [\((frac ((i - 1) * a)) * t)/] ) holds

b_{1} = b_{2}

end;
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 ( len it = t + 1 & ( for i being Nat st i in dom it holds

it . i = [\((frac ((i - 1) * a)) * t)/] ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines F_dp1 DIOPHAN1:def 2 :

for t being 1 _greater Nat

for a being Real

for b_{3} being FinSequence of Segm t holds

( b_{3} = F_dp1 (t,a) iff ( len b_{3} = t + 1 & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = [\((frac ((i - 1) * a)) * t)/] ) ) );

for t being 1 _greater Nat

for a being Real

for b

( b

b

registration
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)))

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
end;

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 )

for t being 1 _greater Nat ex x, y being Integer st

( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )

proof end;