:: Introduction to {L}iouville Numbers
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th1: :: LIOUVIL1:1

for x, y being Nat st x > 1 & y > 1 holds
x * y >= x + y

proof end;

Th2: for n being Nat holds n ! >= 1

proof end;

theorem ADDC1: :: LIOUVIL1:2

for n being Nat holds n <= n !

proof end;

theorem Th3: :: LIOUVIL1:3

for n being Nat holds n * (n !) = ((n + 1) !) - (n !)

proof end;

theorem :: LIOUVIL1:4

for n being Nat st n >= 1 holds
2 <= (n + 1) !

proof end;

Th4: for n being Nat st n >= 1 holds
(n + 1) ! >= (n !) + 1

proof end;

Th5: for n being Nat st n >= 2 holds
(n + 1) ! > (n !) + 1

proof end;

Th6: for n being Nat st n > 1 holds
(n + 2) ! > (n !) + 2

proof end;

Th7: for n, i being Nat st n > 1 & i > 1 holds
(n + i) ! >= (n !) + i

proof end;

theorem Th8: :: LIOUVIL1:5

for n, i being Nat st n >= 1 & i >= 1 holds
(n + i) ! >= (n !) + i

proof end;

theorem :: LIOUVIL1:6

for n, i being Nat st n >= 2 & i >= 1 holds
(n + i) ! > (n !) + i

proof end;

theorem Th9: :: LIOUVIL1:7

for b being Nat st b > 1 holds
|.(1 / b).| < 1

proof end;

theorem Th10: :: LIOUVIL1:8

for d being Integer ex n being non zero Nat st 2 to_power (n - 1) > d

proof end;

registration

let a be Integer;
let b be Nat;

cluster a to_power b -> integer ;

coherence
a to_power b is integer

proof end;

end;

theorem Th11: :: LIOUVIL1:9

for s1, s2 being Real_Sequence st ( for n being Nat holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & ex n being Nat st
( 1 <= n & s1 . n < s2 . n ) & s2 is summable holds
( s1 is summable & Sum s1 < Sum s2 )

proof end;

theorem Th12: :: LIOUVIL1:10

for f being Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
f is summable

proof end;

theorem Th13: :: LIOUVIL1:11

for b being Nat st b > 1 holds
Sum ((1 / b) GeoSeq) = b / (b - 1)

proof end;

registration

let n be Nat;

cluster seq_const n -> NAT -valued ;

coherence
seq_const n is NAT -valued

proof end;

end;

registration

let r be positive Nat;

cluster seq_const r -> positive-yielding ;

coherence
seq_const r is positive-yielding ;

end;

registration

cluster Relation-like omega -defined NAT -valued REAL -valued INT -valued non empty Function-like V28( omega ) V32( omega , REAL ) V39() V40() V41() for Element of K21(K22(omega,REAL));

existence
ex b₁ being Real_Sequence st
( b₁ is NAT -valued & b₁ is INT -valued )

proof end;

end;

theorem Th14: :: LIOUVIL1:12

for F being Real_Sequence
for n being Nat
for a being Real st ( for k being Nat holds F . k = a ) holds
(Partial_Sums F) . n = a * (n + 1)

proof end;

theorem :: LIOUVIL1:13

for n being Nat
for a being Real holds (Partial_Sums (seq_const a)) . n = a * (n + 1)

proof end;

registration

let f be INT -valued Real_Sequence;

cluster Partial_Sums f -> INT -valued ;

coherence
Partial_Sums f is INT -valued

proof end;

end;

registration

let f be NAT -valued Real_Sequence;

cluster Partial_Sums f -> NAT -valued ;

coherence
Partial_Sums f is NAT -valued

proof end;

end;

theorem :: LIOUVIL1:14

for f being Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
ex n being Nat st
for k being Nat st k >= n holds
(Partial_Sums f) . k = (Partial_Sums f) . n

proof end;

theorem Th16: :: LIOUVIL1:15

for f being INT -valued Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
Sum f is Integer

proof end;

registration

let f be nonnegative-yielding Real_Sequence;
let n be Nat;

cluster f ^\ n -> nonnegative-yielding ;

coherence
f ^\ n is nonnegative-yielding

proof end;

end;

definition

let f be Real_Sequence;
let X be Subset of NAT;

func f |_ X -> Real_Sequence equals :: LIOUVIL1:def 1
(NAT --> 0) +* (f | X);

coherence
(NAT --> 0) +* (f | X) is Real_Sequence

proof end;

end;

:: deftheorem defines |_ LIOUVIL1:def 1 :
for f being Real_Sequence
for X being Subset of NAT holds f |_ X = (NAT --> 0) +* (f | X);

registration

let f be Real_Sequence;
let X be Subset of NAT;

cluster f | X -> NAT -defined ;

coherence
f | X is NAT -defined ;

end;

registration

let f be Real_Sequence;
let n be Nat;

cluster f |_ (Seg n) -> summable ;

coherence
f |_ (Seg n) is summable

proof end;

end;

registration

let f be INT -valued Real_Sequence;
let n be Nat;

cluster f |_ (Seg n) -> INT -valued ;

coherence
f |_ (Seg n) is INT -valued ;

end;

theorem :: LIOUVIL1:16

for f being Real_Sequence holds f |_ (Seg 0) = seq_const 0

proof end;

definition

let f be Real_Sequence;
let n be Nat;

func FinSeq (f,n) -> FinSequence of REAL equals :: LIOUVIL1:def 2
f | (Seg n);

coherence
f | (Seg n) is FinSequence of REAL

proof end;

end;

:: deftheorem defines FinSeq LIOUVIL1:def 2 :
for f being Real_Sequence
for n being Nat holds FinSeq (f,n) = f | (Seg n);

theorem Th17: :: LIOUVIL1:17

for f being Real_Sequence
for k, n being Nat st k in Seg n holds
(f |_ (Seg n)) . k = f . k

proof end;

theorem Th18: :: LIOUVIL1:18

for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))

proof end;

theorem Th19: :: LIOUVIL1:19

for f being Real_Sequence
for n being Nat holds dom (FinSeq (f,n)) = Seg n

proof end;

theorem Th20: :: LIOUVIL1:20

for f being Real_Sequence
for i being Nat holds (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1))

proof end;

theorem Th21: :: LIOUVIL1:21

for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = (Partial_Sums f) . n

proof end;

theorem Th22: :: LIOUVIL1:22

for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (f |_ (Seg n)) = (Partial_Sums f) . n

proof end;

theorem :: LIOUVIL1:23

for f being INT -valued Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (f |_ (Seg n)) is Integer

proof end;

theorem Th23: :: LIOUVIL1:24

for f being Real_Sequence
for n being Nat st f is summable & f . 0 = 0 holds
Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))

proof end;

:: |_ is the same as SETWOP_2:def 1, p is FinSequence

registration

cluster Relation-like omega -defined NAT -valued REAL -valued non empty Function-like V28( omega ) V32( omega , REAL ) V39() V40() V41() positive-yielding for Element of K21(K22(omega,REAL));

existence
ex b₁ being Real_Sequence st
( b₁ is positive-yielding & b₁ is NAT -valued )

proof end;

end;

definition

let f be Real_Sequence;

attr f is eventually-non-zero means :ENZ: :: LIOUVIL1:def 3
for n being Nat ex N being Nat st
( n <= N & f . N <> 0 );

end;

:: deftheorem ENZ defines eventually-non-zero LIOUVIL1:def 3 :
for f being Real_Sequence holds
( f is eventually-non-zero iff for n being Nat ex N being Nat st
( n <= N & f . N <> 0 ) );

registration

cluster Function-like V32( omega , REAL ) eventually-nonzero -> eventually-non-zero for Element of K21(K22(omega,REAL));

coherence
for b₁ being Real_Sequence st b₁ is eventually-nonzero holds
b₁ is eventually-non-zero

proof end;

end;

registration

cluster seq_id (id NAT) -> eventually-nonzero ;

coherence
seq_id (id NAT) is eventually-nonzero

proof end;

end;

registration

cluster Relation-like omega -defined REAL -valued non empty Function-like V28( omega ) V32( omega , REAL ) V39() V40() V41() eventually-non-zero for Element of K21(K22(omega,REAL));

existence
ex b₁ being Real_Sequence st b₁ is eventually-non-zero

proof end;

end;

theorem Th24: :: LIOUVIL1:25

for f being eventually-non-zero Real_Sequence
for n being Nat holds f ^\ n is eventually-non-zero

proof end;

registration

let f be eventually-non-zero Real_Sequence;
let n be Nat;

cluster f ^\ n -> eventually-non-zero for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = f ^\ n holds
b₁ is eventually-non-zero by Th24;

end;

registration

cluster non-zero Function-like constant V32( omega , REAL ) -> eventually-non-zero for Element of K21(K22(omega,REAL));

coherence
for b₁ being Real_Sequence st b₁ is non-zero & b₁ is constant holds
b₁ is eventually-non-zero

proof end;

end;

definition

let b be Nat;

func powerfact b -> Real_Sequence means :DefPower: :: LIOUVIL1:def 4
for i being Nat holds it . i = 1 / (b to_power (i !));

correctness
existence
ex b₁ being Real_Sequence st
for i being Nat holds b₁ . i = 1 / (b to_power (i !));
uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = 1 / (b to_power (i !)) ) & ( for i being Nat holds b₂ . i = 1 / (b to_power (i !)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem DefPower defines powerfact LIOUVIL1:def 4 :
for b being Nat
for b₂ being Real_Sequence holds
( b₂ = powerfact b iff for i being Nat holds b₂ . i = 1 / (b to_power (i !)) );

theorem Th25: :: LIOUVIL1:26

for b, i being Nat st b >= 1 holds
(powerfact b) . i <= ((1 / b) GeoSeq) . i

proof end;

theorem Th26: :: LIOUVIL1:27

for b being Nat st b > 1 holds
( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) )

proof end;

registration

let b be non trivial Nat;

cluster powerfact b -> summable ;

coherence
powerfact b is summable

proof end;

end;

registration

cluster Relation-like omega -defined REAL -valued non empty Function-like V28( omega ) V32( omega , REAL ) V39() V40() V41() nonnegative-yielding for Element of K21(K22(omega,REAL));

existence
ex b₁ being Real_Sequence st b₁ is nonnegative-yielding

proof end;

end;

theorem Th27: :: LIOUVIL1:28

for n, b being Nat st b > 1 & n >= 1 holds
Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n)

proof end;

:: Liouville number

definition

let x be Real;

attr x is liouville means :: LIOUVIL1:def 5
for n being Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(x - (p / q)).| & |.(x - (p / q)).| < 1 / (q |^ n) );

end;

:: deftheorem defines liouville LIOUVIL1:def 5 :
for x being Real holds
( x is liouville iff for n being Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(x - (p / q)).| & |.(x - (p / q)).| < 1 / (q |^ n) ) );

theorem Def2: :: LIOUVIL1:29

for r being Real holds
( r is liouville iff for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) )

proof end;

definition

let a be Real_Sequence;
let b be Nat;

func Liouville_seq (a,b) -> Real_Sequence means :DefLio: :: LIOUVIL1:def 6
( it . 0 = 0 & ( for k being non zero Nat holds it . k = (a . k) / (b to_power (k !)) ) );

existence
ex b₁ being Real_Sequence st
( b₁ . 0 = 0 & ( for k being non zero Nat holds b₁ . k = (a . k) / (b to_power (k !)) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for k being non zero Nat holds b₁ . k = (a . k) / (b to_power (k !)) ) & b₂ . 0 = 0 & ( for k being non zero Nat holds b₂ . k = (a . k) / (b to_power (k !)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefLio defines Liouville_seq LIOUVIL1:def 6 :
for a being Real_Sequence
for b being Nat
for b₃ being Real_Sequence holds
( b₃ = Liouville_seq (a,b) iff ( b₃ . 0 = 0 & ( for k being non zero Nat holds b₃ . k = (a . k) / (b to_power (k !)) ) ) );

:: Liouville number!irrationality

registration

cluster V38() liouville -> irrational for object ;

coherence
for b₁ being Real st b₁ is liouville holds
b₁ is irrational

proof end;

end;

:: Liouville's constant

definition

let a be Real_Sequence;
let b be Nat;

func Liouville_constant (a,b) -> Real equals :: LIOUVIL1:def 7
Sum (Liouville_seq (a,b));

coherence
Sum (Liouville_seq (a,b)) is Real ;

end;

:: deftheorem defines Liouville_constant LIOUVIL1:def 7 :
for a being Real_Sequence
for b being Nat holds Liouville_constant (a,b) = Sum (Liouville_seq (a,b));

definition

let b be Nat;

func BLiouville_seq b -> Real_Sequence means :LiuSeq: :: LIOUVIL1:def 8
for n being Nat holds it . n = b to_power (n !);

correctness
existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = b to_power (n !);
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = b to_power (n !) ) & ( for n being Nat holds b₂ . n = b to_power (n !) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem LiuSeq defines BLiouville_seq LIOUVIL1:def 8 :
for b being Nat
for b₂ being Real_Sequence holds
( b₂ = BLiouville_seq b iff for n being Nat holds b₂ . n = b to_power (n !) );

registration

let b be Nat;

cluster BLiouville_seq b -> NAT -valued ;

coherence
BLiouville_seq b is NAT -valued

proof end;

end;

definition

let a be Real_Sequence;
let b be Nat;

func ALiouville_seq (a,b) -> Real_Sequence means :ALiuDef: :: LIOUVIL1:def 9
for n being Nat holds it . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)));

correctness
existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)));
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) & ( for n being Nat holds b₂ . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem ALiuDef defines ALiouville_seq LIOUVIL1:def 9 :
for a being Real_Sequence
for b being Nat
for b₃ being Real_Sequence holds
( b₃ = ALiouville_seq (a,b) iff for n being Nat holds b₃ . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) );

theorem Th28: :: LIOUVIL1:30

for a being NAT -valued Real_Sequence
for b, n, k being Nat st b > 0 & k <= n holds
((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer

proof end;

theorem Th29: :: LIOUVIL1:31

for a being NAT -valued Real_Sequence
for b, n being Nat st b > 0 holds
(ALiouville_seq (a,b)) . n is Integer

proof end;

registration

let a be NAT -valued Real_Sequence;
let b be non zero Nat;

cluster ALiouville_seq (a,b) -> INT -valued ;

coherence
ALiouville_seq (a,b) is INT -valued

proof end;

end;

theorem Th30: :: LIOUVIL1:32

for n, b being non zero Nat st b > 1 holds
(BLiouville_seq b) . n > 1

proof end;

theorem Th31: :: LIOUVIL1:33

for a being NAT -valued Real_Sequence
for b being non zero Nat st b >= 2 & rng a c= b holds
Liouville_seq (a,b) is summable

proof end;

theorem Th32: :: LIOUVIL1:34

for a being Real_Sequence
for n, b being non zero Nat st b > 1 holds
((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = Sum (FinSeq ((Liouville_seq (a,b)),n))

proof end;

theorem Th33: :: LIOUVIL1:35

for a being NAT -valued Real_Sequence
for b being non trivial Nat
for n being Nat holds (Liouville_seq (a,b)) . n >= 0

proof end;

theorem :: LIOUVIL1:36

for a being NAT -valued positive-yielding Real_Sequence
for b being non trivial Nat
for n being non zero Nat holds (Liouville_seq (a,b)) . n > 0

proof end;

registration

let a be NAT -valued Real_Sequence;
let b be non trivial Nat;

cluster Liouville_seq (a,b) -> nonnegative-yielding ;

coherence
Liouville_seq (a,b) is nonnegative-yielding

proof end;

end;

theorem Th34: :: LIOUVIL1:37

for a being NAT -valued Real_Sequence
for b, c being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i

proof end;

theorem :: LIOUVIL1:38

for a being NAT -valued Real_Sequence
for b, c being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
Sum (Liouville_seq (a,b)) <= Sum ((c - 1) (#) (powerfact b))

proof end;

theorem Th35: :: LIOUVIL1:39

for a being NAT -valued Real_Sequence
for b, c, n being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((c - 1) (#) ((powerfact b) ^\ (n + 1)))

proof end;

theorem Th36: :: LIOUVIL1:40

for a being NAT -valued Real_Sequence
for b being non trivial Nat
for n being Nat st a is eventually-non-zero & rng a c= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0

proof end;

theorem Th37: :: LIOUVIL1:41

for a being NAT -valued Real_Sequence
for b being non trivial Nat st rng a c= b & a is eventually-non-zero holds
for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )

proof end;

definition

func Liouville_constant -> Real equals :: LIOUVIL1:def 10
Liouville_constant ((seq_const 1),10);

correctness
coherence
Liouville_constant ((seq_const 1),10) is Real;
;

end;

:: deftheorem defines Liouville_constant LIOUVIL1:def 10 :
Liouville_constant = Liouville_constant ((seq_const 1),10);

theorem Th38: :: LIOUVIL1:42

for a being NAT -valued Real_Sequence
for b being non trivial Nat st rng a c= b & a is eventually-non-zero holds
Liouville_constant (a,b) is liouville

proof end;

registration

cluster Liouville_constant -> liouville ;

coherence
Liouville_constant is liouville

proof end;

end;

registration

cluster ext-real complex V38() liouville for object ;

existence
ex b₁ being Real st b₁ is liouville

proof end;

end;

definition

mode Liouville is liouville Real;

end;

theorem Th39: :: LIOUVIL1:43

for m, n being non zero Nat holds (Liouville_seq ((seq_const 1),m)) . n = m to_power (- (n !))

proof end;

TC1: for m, n being non zero Nat st 1 < m holds
(Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)

proof end;

TLLC: for m, n being Nat st 1 < m holds
(Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)

proof end;

theorem :: LIOUVIL1:44

for m being Nat st 1 < m holds
Liouville_seq ((seq_const 1),m) is negligible

proof end;

theorem :: LIOUVIL1:45

( 1 / 10 < Liouville_constant & Liouville_constant <= (10 / 9) - (1 / 10) )

proof end;

theorem Th40: :: LIOUVIL1:46

for nl being Liouville
for z being Integer holds z + nl is liouville

proof end;

registration

let nl be Liouville;
let z be Integer;

cluster nl + z -> liouville ;

coherence
nl + z is liouville by Th40;

end;

definition

func LiouvilleNumbers -> Subset of REAL equals :: LIOUVIL1:def 11
{ nl where nl is Liouville : verum } ;

coherence
{ nl where nl is Liouville : verum } is Subset of REAL

proof end;

end;

:: deftheorem defines LiouvilleNumbers LIOUVIL1:def 11 :
LiouvilleNumbers = { nl where nl is Liouville : verum } ;

registration

cluster LiouvilleNumbers -> non empty ;

coherence
not LiouvilleNumbers is empty

proof end;

end;

registration

cluster LiouvilleNumbers -> infinite ;

coherence
not LiouvilleNumbers is finite

proof end;

end;