:: by Adam Grabowski and Artur Korni{\l}owicz

::

:: Received February 23, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

Th2: for n being Nat holds 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 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 )

( 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

for k being Nat st k >= n holds

f . k = 0 holds

f is summable

proof end;

registration
end;

registration

ex b_{1} being Real_Sequence st

( b_{1} is NAT -valued & b_{1} is INT -valued )
end;

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

existence ex b

( b

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

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;

registration
end;

registration
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

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

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

f ^\ n is nonnegative-yielding

end;
let n be Nat;

coherence

f ^\ n is nonnegative-yielding

proof end;

definition

let f be Real_Sequence;

let X be Subset of NAT;

coherence

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

end;
let X be Subset of NAT;

coherence

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

proof end;

:: deftheorem defines |_ LIOUVIL1:def 1 :

for f being Real_Sequence

for X being Subset of NAT holds f |_ X = (NAT --> 0) +* (f | X);

for f being Real_Sequence

for X being Subset of NAT holds f |_ X = (NAT --> 0) +* (f | X);

registration
end;

registration
end;

definition
end;

:: deftheorem defines FinSeq LIOUVIL1:def 2 :

for f being Real_Sequence

for n being Nat holds FinSeq (f,n) = f | (Seg n);

for f being Real_Sequence

for n being Nat holds FinSeq (f,n) = f | (Seg n);

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

for n being Nat st f . 0 = 0 holds

Sum (FinSeq (f,n)) = Sum (f |_ (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))

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

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

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

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

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

ex b_{1} being Real_Sequence st

( b_{1} is positive-yielding & b_{1} is NAT -valued )
end;

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

existence ex b

( b

proof end;

definition

let f be Real_Sequence;

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

for n being Nat ex N being Nat st

( n <= N & f . N <> 0 );

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

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

for b_{1} being Real_Sequence st b_{1} is eventually-nonzero holds

b_{1} is eventually-non-zero
end;

cluster Function-like V32( omega , REAL ) eventually-nonzero -> eventually-non-zero for Real_Sequence;

coherence for b

b

proof end;

registration

ex b_{1} being Real_Sequence st b_{1} is eventually-non-zero
end;

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

existence ex b

proof end;

registration

let f be eventually-non-zero Real_Sequence;

let n be Nat;

coherence

for b_{1} being Real_Sequence st b_{1} = f ^\ n holds

b_{1} is eventually-non-zero
by Th24;

end;
let n be Nat;

coherence

for b

b

registration

for b_{1} being Real_Sequence st b_{1} is non-zero & b_{1} is constant holds

b_{1} is eventually-non-zero
end;

cluster non-zero Function-like constant V32( omega , REAL ) -> eventually-non-zero for Real_Sequence;

coherence for b

b

proof end;

definition

let b be Nat;

existence

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = 1 / (b to_power (i !));

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = 1 / (b to_power (i !)) ) & ( for i being Nat holds b_{2} . i = 1 / (b to_power (i !)) ) holds

b_{1} = b_{2};

end;
func powerfact b -> Real_Sequence means :DefPower: :: LIOUVIL1:def 4

for i being Nat holds it . i = 1 / (b to_power (i !));

correctness for i being Nat holds it . i = 1 / (b to_power (i !));

existence

ex b

for i being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem DefPower defines powerfact LIOUVIL1:def 4 :

for b being Nat

for b_{2} being Real_Sequence holds

( b_{2} = powerfact b iff for i being Nat holds b_{2} . i = 1 / (b to_power (i !)) );

for b being Nat

for b

( b

registration

ex b_{1} being Real_Sequence st b_{1} is nonnegative-yielding
end;

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

existence ex b

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

Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n)

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

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

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

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 0 & ( for k being non zero Nat holds b_{1} . k = (a . k) / (b to_power (k !)) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = 0 & ( for k being non zero Nat holds b_{1} . k = (a . k) / (b to_power (k !)) ) & b_{2} . 0 = 0 & ( for k being non zero Nat holds b_{2} . k = (a . k) / (b to_power (k !)) ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = 0 & ( for k being non zero Nat holds it . k = (a . k) / (b to_power (k !)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefLio defines Liouville_seq LIOUVIL1:def 6 :

for a being Real_Sequence

for b being Nat

for b_{3} being Real_Sequence holds

( b_{3} = Liouville_seq (a,b) iff ( b_{3} . 0 = 0 & ( for k being non zero Nat holds b_{3} . k = (a . k) / (b to_power (k !)) ) ) );

for a being Real_Sequence

for b being Nat

for b

( b

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

for a being Real_Sequence

for b being Nat holds Liouville_constant (a,b) = Sum (Liouville_seq (a,b));

definition

let b be Nat;

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = b to_power (n !);

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = b to_power (n !) ) & ( for n being Nat holds b_{2} . n = b to_power (n !) ) holds

b_{1} = b_{2};

end;
func BLiouville_seq b -> Real_Sequence means :LiuSeq: :: LIOUVIL1:def 8

for n being Nat holds it . n = b to_power (n !);

correctness for n being Nat holds it . n = b to_power (n !);

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem LiuSeq defines BLiouville_seq LIOUVIL1:def 8 :

for b being Nat

for b_{2} being Real_Sequence holds

( b_{2} = BLiouville_seq b iff for n being Nat holds b_{2} . n = b to_power (n !) );

for b being Nat

for b

( b

definition

let a be Real_Sequence;

let b be Nat;

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)));

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) & ( for n being Nat holds b_{2} . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) ) holds

b_{1} = b_{2};

end;
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 for n being Nat holds it . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)));

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem ALiuDef defines ALiouville_seq LIOUVIL1:def 9 :

for a being Real_Sequence

for b being Nat

for b_{3} being Real_Sequence holds

( b_{3} = ALiouville_seq (a,b) iff for n being Nat holds b_{3} . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) );

for a being Real_Sequence

for b being Nat

for b

( b

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

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

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;

coherence

ALiouville_seq (a,b) is INT -valued

end;
let b be non zero Nat;

coherence

ALiouville_seq (a,b) is INT -valued

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

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

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

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

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

Liouville_seq (a,b) is nonnegative-yielding

end;
let b be non trivial Nat;

coherence

Liouville_seq (a,b) is nonnegative-yielding

proof 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

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

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

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

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

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;

:: deftheorem defines Liouville_constant LIOUVIL1:def 10 :

Liouville_constant = Liouville_constant ((seq_const 1),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

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

definition

{ nl where nl is Liouville : verum } is Subset of REAL
end;

func LiouvilleNumbers -> Subset of REAL equals :: LIOUVIL1:def 11

{ nl where nl is Liouville : verum } ;

coherence { nl where nl is Liouville : verum } ;

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

proof end;

:: deftheorem defines LiouvilleNumbers LIOUVIL1:def 11 :

LiouvilleNumbers = { nl where nl is Liouville : verum } ;

LiouvilleNumbers = { nl where nl is Liouville : verum } ;

registration
end;

registration
end;