:: Introduction to {L}iouville Numbers
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: Copyright (c) 2017 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;

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

registration
let r be positive Nat;
coherence ;
end;

registration
existence
ex b1 being Real_Sequence st
( b1 is NAT -valued & b1 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
() . n = a * (n + 1)
proof end;

theorem :: LIOUVIL1:13
for n being Nat
for a being Real holds () . n = a * (n + 1)
proof end;

registration
let f be INT -valued Real_Sequence;
coherence
proof end;
end;

registration
let f be NAT -valued Real_Sequence;
coherence
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
() . k = () . 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;
coherence
proof end;
end;

definition
let f be Real_Sequence;
let X be Subset of NAT;
func f |_ X -> Real_Sequence equals :: LIOUVIL1:def 1
() +* (f | X);
coherence
() +* (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 = () +* (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 |_ () = 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)) = () . 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)) = () . 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
existence
ex b1 being Real_Sequence st
( b1 is positive-yielding & b1 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
coherence
for b1 being Real_Sequence st b1 is eventually-nonzero holds
b1 is eventually-non-zero
proof end;
end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being Real_Sequence st b1 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;
coherence
for b1 being Real_Sequence st b1 = f ^\ n holds
b1 is eventually-non-zero
by Th24;
end;

registration
coherence
for b1 being Real_Sequence st b1 is non-zero & b1 is constant holds
b1 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 b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / (b to_power (i !))
;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / (b to_power (i !)) ) & ( for i being Nat holds b2 . i = 1 / (b to_power (i !)) ) holds
b1 = b2
;
proof end;
end;

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

theorem Th25: :: LIOUVIL1:26
for b, i being Nat st b >= 1 holds
() . i <= ((1 / b) GeoSeq) . i
proof end;

theorem Th26: :: LIOUVIL1:27
for b being Nat st b > 1 holds
( powerfact b is summable & Sum () <= b / (b - 1) )
proof end;

registration
let b be non trivial Nat;
coherence
proof end;
end;

registration
existence
ex b1 being Real_Sequence st b1 is nonnegative-yielding
proof end;
end;

theorem Th27: :: LIOUVIL1:28
for n, b being Nat st b > 1 & n >= 1 holds
Sum ((b - 1) (#) (() ^\ (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 b1 being Real_Sequence st
( b1 . 0 = 0 & ( for k being non zero Nat holds b1 . k = (a . k) / (b to_power (k !)) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = 0 & ( for k being non zero Nat holds b1 . k = (a . k) / (b to_power (k !)) ) & b2 . 0 = 0 & ( for k being non zero Nat holds b2 . k = (a . k) / (b to_power (k !)) ) holds
b1 = b2
proof end;
end;

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

:: Liouville number!irrationality
registration
coherence
for b1 being Real st b1 is liouville holds
b1 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 b1 being Real_Sequence st
for n being Nat holds b1 . n = b to_power (n !)
;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = b to_power (n !) ) & ( for n being Nat holds b2 . n = b to_power (n !) ) holds
b1 = b2
;
proof end;
end;

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

registration
let b be Nat;
coherence
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 = (() . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)));
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (() . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)))
;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (() . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) & ( for n being Nat holds b2 . n = (() . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem ALiuDef defines ALiouville_seq LIOUVIL1:def 9 :
for a being Real_Sequence
for b being Nat
for b3 being Real_Sequence holds
( b3 = ALiouville_seq (a,b) iff for n being Nat holds b3 . n = (() . 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) * (() . 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
() . 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) / (() . 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;
coherence
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) (#) ()) . 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) (#) ())
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) (#) (() ^\ (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 ((),10);
correctness
coherence
Liouville_constant ((),10) is Real
;
;
end;

:: deftheorem defines Liouville_constant LIOUVIL1:def 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
coherence
proof end;
end;

registration
existence
ex b1 being Real st b1 is liouville
proof end;
end;

definition end;

theorem Th39: :: LIOUVIL1:43
for m, n being non zero Nat holds (Liouville_seq ((),m)) . n = m to_power (- (n !))
proof end;

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

proof end;

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

proof end;

theorem :: LIOUVIL1:44
for m being Nat st 1 < m holds
Liouville_seq ((),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
coherence
proof end;
end;

registration
coherence
proof end;
end;