:: Introduction to {L}iouville Numbers
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LIOUVIL1, RSSPACE, PARTFUN3, EC_PF_2, VALUED_0, NUMBERS,
SUBSET_1, INT_1, SEQ_1, FINSEQ_1, RAT_1, ORDINAL4, POWER, XXREAL_0,
CARD_1, ARYTM_3, RELAT_1, NAT_1, FUNCT_1, ARYTM_1, REALSET1, ORDINAL2,
COMPLEX1, VALUED_1, SERIES_1, CARD_3, XBOOLE_0, NEWTON, IRRAT_1, REAL_1,
ASYMPT_1, XCMPLX_0, FUNCT_7, TARSKI, PREPOWER, ABIAN, FUNCT_4, FUNCOP_1,
BINOP_2, FINSOP_1, ZFMISC_1, ASYMPT_0, FINSET_1, ORDINAL1, ASYMPT_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, RELAT_1, INT_1, COMPLEX1, FUNCT_1, BINOP_1, NAT_1, FUNCOP_1,
FINSET_1, CARD_1, CARD_2, ASYMPT_1, FUNCT_4, FUNCT_2, VALUED_1, PARTFUN3,
BINOP_2, FINSOP_1, FINSEQ_1, SEQ_1, SEQ_2, NEWTON, PREPOWER, POWER,
RVSUM_1, SERIES_1, RAT_1, RSSPACE, IRRAT_1, ABIAN, ASYMPT_0, NEWTON04,
EC_PF_2, ASYMPT_3;
constructors SEQ_2, RVSUM_1, PREPOWER, ABIAN, BINOP_2, PARTFUN3, SETWISEO,
FINSOP_1, ASYMPT_0, RSSPACE, COMSEQ_3, RELSET_1, COMSEQ_2, SEQ_1,
NEWTON04, EC_PF_2, FINSET_1, CARD_2, ASYMPT_1, ASYMPT_3;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, FINSEQ_1,
SEQ_1, SEQ_2, ABSVALUE, XCMPLX_0, FUNCT_1, PREPOWER, NUMPOLY1, BINOP_2,
NEWTON04, RAT_1, FUNCOP_1, RELAT_1, RSSPACE, PARTFUN3, COMPLEX1, CARD_1,
NAT_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, PARTFUN3, ASYMPT_0;
equalities SEQ_1, SERIES_1;
expansions SERIES_1, ASYMPT_0;
theorems RAT_1, INT_1, POWER, ENTROPY1, NAT_1, XXREAL_0, XCMPLX_1, ABSVALUE,
COMPLEX1, XREAL_1, HOLDER_1, FUNCT_2, NEWTON, RELAT_1, FUNCT_1, FUNCOP_1,
FUNCT_4, XBOOLE_1, SERIES_1, SIN_COS, RVSUM_1, IRRAT_1, SEQ_4, ORDINAL1,
SEQ_1, FINSEQ_1, EC_PF_2, RSSPACE2, VALUED_1, BINOP_2, FINSOP_1, TARSKI,
PRE_FF, PREPOWER, ASYMPT_1, NEWTON04, NAT_2, ZFMISC_1, CARD_1, ENUMSET1,
PARTFUN3, FINSEQ_3, FINSET_1, TOPGEN_3, SUBSET_1, XREAL_0, ASYMPT_3;
schemes NAT_1, IRRAT_1, FUNCT_2;
begin :: Preliminaries
theorem Th1:
for x, y be Nat st x > 1 & y > 1 holds x*y >= x+y
proof
let x, y be Nat;
assume
A1: x > 1 & y > 1;
per cases;
suppose
A2: x >= y;
y - 0 > 1 by A1; then
y - 1 >= 0 + 1 by INT_1:7,XREAL_1:12; then
x * (y - 1) >= y * 1 by A2,XREAL_1:66; then
x * y - x + x >= y + x by XREAL_1:6;
hence thesis;
end;
suppose
A3: x < y;
x - 0 > 1 by A1; then
x - 1 >= 0 + 1 by XREAL_1:12,INT_1:7; then
y * (x - 1) >= x * 1 by A3,XREAL_1:66; then
x * y - y + y >= x + y by XREAL_1:6;
hence thesis;
end;
end;
Th2:
for n be Nat holds n! >= 1
proof
let n be Nat;
n! >= 0 + 1 by NAT_1:13;
hence thesis;
end;
theorem ADDC1:
for n be Nat holds n <= n!
proof
let n be Nat;
n + 1 <= 3 or 3 <= n by INT_1:7; then
n + 1 - 1 <= 3 - 1 or 3 <= n by XREAL_1:9; then
CCS:(n = 0 or ... or n = 2) or 3 <= n;
per cases by CCS;
suppose n = 0;
hence thesis;
end;
suppose n = 1;
hence thesis by NEWTON:13;
end;
suppose n = 2;
hence thesis by NEWTON:14;
end;
suppose n >= 3;
hence thesis by ASYMPT_1:59;
end;
end;
theorem Th3:
for n be Nat holds n * (n!) = (n + 1)! - n!
proof
let n be Nat;
set a = n!;
thus n * a = (n + 1) * a - a .= (n + 1)! - a by NEWTON:15;
end;
theorem
for n be Nat st n >= 1 holds 2 <= (n + 1)!
proof
let n be Nat;
assume n >= 1; then
n + 1 >= 1 + 1 by XREAL_1:7; then
1 < (n+1)! by ASYMPT_1:55; then
1 + 1 <= (n+1)! by NAT_1:13;
hence thesis;
end;
Th4:
for n be Nat st n >= 1 holds (n+1)! >= n! + 1
proof
let n be Nat;
assume
A1: n >= 1;
n! >= 1 by Th2; then
n * (n!) >= 1 * 1 by A1,XREAL_1:66; then
(n+1)! - n! >= 1 by Th3; then
(n+1)! - n! + n! >= 1 + n! by XREAL_1:6;
hence thesis;
end;
Th5:
for n be Nat st n >= 2 holds (n + 1)! > n! + 1
proof
let n be Nat;
assume n >= 2; then
n >= 1 + 1; then
A1: n > 1 by NAT_1:13;
n! >= n by NEWTON:38; then
n! > 1 by A1,XXREAL_0:2; then
n * (n!) > 1 * 1 by A1,XREAL_1:96; then
(n+1)! - n! > 1 by Th3; then
(n+1)! - n! + n! > 1 + n! by XREAL_1:6;
hence thesis;
end;
Th6:
for n be Nat st n > 1 holds (n+2)! > n! + 2
proof
let n be Nat;
assume
A1: n > 1; then
A2: n+1 > 1+1 by XREAL_1:8; then
A3: n+1 > 1 by XXREAL_0:2;
n! >= n by NEWTON:38; then
A4: n! > 1 by XXREAL_0:2,A1;
n+1 <= n+1+1 by NAT_1:11; then
A5: (n+1)! <= (n+2)! by ASYMPT_1:56;
(n+1)! <> (n+2)!
proof
assume (n+1)! = (n+2)!; then
(n+1)! * 1 = (n+1)! * (n+1+1) by NEWTON:15; then
1 = n+1+1 by XCMPLX_1:5; then
0 = n+1;
hence thesis;
end; then
A6: (n+1)! < (n+2)! by XXREAL_0:1,A5;
(n+1)! = (n+1) * (n!) by NEWTON:15; then
A7: (n+1)! >= (n+1) + n! by A3,Th1,A4;
(n+1) + n! > n! + 2 by XREAL_1:8,A2; then
(n+1)! >= n! + 2 by A7,XXREAL_0:2;
hence thesis by A6,XXREAL_0:2;
end;
Th7:
for n,i be Nat st n > 1 & i > 1 holds (n+i)! >= n! + i
proof
let n,i be Nat;
assume
A1: n > 1 & i > 1; then
A2: i >= 1+1 by NAT_1:13;
A3: (n+i)! >= n! * (i!) by NEWTON04:70;
n >= 1 + 1 by A1,NAT_1:13; then
n! > 1 & i! > 1 by A2,ASYMPT_1:55; then
A5: n! * (i!) >= n! + (i!) by Th1;
per cases by A2,XXREAL_0:1;
suppose i = 2;
hence thesis by A1,Th6;
end;
suppose
i > 2; then
A6: i >= 2+1 by NAT_1:13;
i! > i by ASYMPT_1:59,A6; then
n! + (i!) > n! + i by XREAL_1:6; then
n! * (i!) > n! + i by A5,XXREAL_0:2;
hence thesis by A3,XXREAL_0:2;
end;
end;
theorem Th8:
for n,i be Nat st n >= 1 & i >= 1 holds (n + i)! >= n! + i
proof
let n,i be Nat;
assume n >= 1 & i >= 1; then
per cases by XXREAL_0:1;
suppose n >= 1 & i > 1; then
per cases by XXREAL_0:1;
suppose n > 1 & i > 1;
hence thesis by Th7;
end;
suppose
n = 1 & i > 1;
hence thesis by NEWTON:13,NEWTON:38;
end;
end;
suppose n >= 1 & i = 1;
hence thesis by Th4;
end;
end;
theorem
for n,i being Nat st n >= 2 & i >= 1 holds (n+i)! > n! + i
proof
let n,i be Nat;
assume n >= 2 & i >= 1; then
per cases by XXREAL_0:1;
suppose n >= 2 & i > 1; then
per cases by XXREAL_0:1;
suppose
A1: n > 2 & i > 1; then
A2: i >= 1+1 by NAT_1:13;
A3: (n+i)! >= n! * (i!) by NEWTON04:70;
n! > 1 & i! > 1 by A2,A1,ASYMPT_1:55; then
A5: n! * (i!) >= n! + (i!) by Th1;
per cases by A2,XXREAL_0:1;
suppose
A6: i = 2;
n > 1 by A1,XXREAL_0:2;
hence thesis by A6,Th6;
end;
suppose
i > 2; then
A7: i >= 2 + 1 by NAT_1:13;
i! > i by ASYMPT_1:59,A7; then
n! + (i!) > n! + i by XREAL_1:6; then
n! * (i!) > n! + i by A5,XXREAL_0:2;
hence thesis by A3,XXREAL_0:2;
end;
end;
suppose
A8: n = 2 & i > 1; then
2 + i >= 2 + 1 by XREAL_1:7;
hence thesis by A8,NEWTON:14,ASYMPT_1:59;
end;
end;
suppose n >= 2 & i = 1;
hence thesis by Th5;
end;
end;
theorem Th9:
for b be Nat st b > 1 holds |. 1/b .| < 1
proof
let b be Nat;
assume b > 1; then
1/b < 1/1 by XREAL_1:76;
hence thesis;
end;
theorem Th10:
for d be Integer holds ex n be non zero Nat st 2 to_power (n-1) > d
proof
let d be Integer;
per cases;
suppose
A1: d <= 0;
take n = 1;
thus thesis by A1,POWER:24;
end;
suppose
A2: d > 0; then
d >= 1+0 by INT_1:7; then
per cases by XXREAL_0:1;
suppose
A3: d = 1;
take n = 2;
2 to_power (n-1) = 2 to_power 1 .= 2;
hence thesis by A3;
end;
suppose
d > 1; then
log (2,d) > 0 by ENTROPY1:4; then
A4: [/ log (2,d) \] > 0;
set n = [/ log (2,d) \] + 2;
n in NAT by A4,INT_1:3; then
reconsider n as Nat;
reconsider n as non zero Nat by A4;
take n;
n-1 = [/ log (2,d) \] + 1; then
2 to_power(n-1) > 2 to_power (log(2,d)) by POWER:39,INT_1:32;
hence thesis by A2,POWER:def 3;
end;
end;
end;
registration
let a be Integer, b be Nat;
cluster a to_power b -> integer;
coherence
proof
per cases;
suppose a >= 0; then
a in NAT by INT_1:3; then
reconsider aa = a as Nat;
aa to_power b is Integer;
hence thesis;
end;
suppose a < 0; then
reconsider aa = -a as Element of NAT by INT_1:3;
per cases;
suppose b is odd; then
(-aa) |^ b = -(aa |^ b) by POWER:2;
hence thesis;
end;
suppose b is even; then
(-aa) |^ b = aa |^ b by POWER:1;
hence thesis;
end;
end;
end;
end;
begin :: Sequences
theorem Th11:
for s1, s2 be Real_Sequence st
(for n be Nat holds 0 <= s1.n & s1.n <= s2.n) &
(ex n be Nat st 1 <= n & s1.n < s2.n) & s2 is summable holds
s1 is summable & Sum(s1) < Sum(s2)
proof
let s1, s2 be Real_Sequence;
assume that
A1: for n be Nat holds 0 <= s1.n & s1.n <= s2.n and
A2: ex n be Nat st 1 <= n & s1.n < s2.n and
A3: s2 is summable;
consider N be Nat such that
A4: 1 <= N & s1.N < s2.N by A2;
A5: for n be Nat st 0 <= n holds s1.n <= s2.n by A1;
hence s1 is summable by A1,A3,SERIES_1:19;
N - 1 in NAT by A4,INT_1:5; then
reconsider N1 = N - 1 as Nat;
A6: N1 + 1 = N; then
A7: Partial_Sums(s1).N = Partial_Sums(s1).N1 + s1.N by SERIES_1:def 1;
A8: Sum(s1) = Partial_Sums(s1).N + Sum(s1^\(N+1)) by A1,A3,A5,SERIES_1:15,19;
A9: Partial_Sums(s2).N = Partial_Sums(s2).N1 + s2.N by A6,SERIES_1:def 1;
A10: Sum(s2) = Partial_Sums(s2).N + Sum(s2^\(N+1)) by SERIES_1:15,A3;
A11: for n be Nat holds 0 <= (s1 ^\ (N + 1)).n
proof
let n be Nat;
(s1 ^\ (N + 1)).n = s1.(n + (N + 1)) by NAT_1:def 3;
hence thesis by A1;
end;
A12: s2 ^\ (N + 1) is summable by A3,SERIES_1:12;
for n be Nat holds (s1 ^\ (N + 1)).n <= (s2 ^\ (N + 1)).n
proof
let n be Nat;
A13: (s1 ^\ (N + 1)).n = s1.(n + (N + 1)) by NAT_1:def 3;
(s2 ^\ (N + 1)).n = s2.(n + (N + 1)) by NAT_1:def 3;
hence thesis by A1,A13;
end; then
A14: Sum(s1 ^\ (N + 1)) <= Sum(s2 ^\ (N + 1)) by A11,A12,SERIES_1:20;
Partial_Sums(s1).N1 + s1.N < Partial_Sums(s2).N1 + s2.N
by XREAL_1:8,A4,A1,SERIES_1:14;
hence thesis by A7,A8,A9,A10,A14,XREAL_1:8;
end;
theorem Th12:
for f be Real_Sequence st ex n be Nat st
(for k be Nat st k >= n holds f.k = 0) holds f is summable
proof
let f be Real_Sequence;
given n be Nat such that
A1: for k be Nat st k >= n holds f.k = 0;
set p = Partial_Sums f;
reconsider pk = p.n as Real;
set r = seq_const pk;
for k be Nat st k >= n holds p.k = r.k
proof
let k be Nat;
assume
A2: k >= n;
defpred P[Nat] means p.$1 = r.$1;
A3: P[n] by SEQ_1:57;
A4: for i be Nat st n <= i holds P[i] implies P[i+1]
proof
let i be Nat;
assume
A5: n <= i;
assume
A6: P[i];
p.(i + 1)
= p.i + f.(i + 1) by SERIES_1:def 1
.= r.i + 0 by A1,A5,A6,NAT_1:12
.= pk by SEQ_1:57
.= r.(i + 1);
hence thesis;
end;
for k be Nat st n <= k holds P[k] from NAT_1:sch 8(A3,A4);
hence thesis by A2;
end;
hence thesis by SEQ_4:18;
end;
theorem Th13:
for b be Nat st b > 1 holds Sum ((1/b) GeoSeq) = b/(b-1)
proof
let b be Nat;
assume
A0: b > 1; then
A1: |. 1/b .| < 1 by Th9;
Sum ((1/b) GeoSeq) = 1/( 1-(1/b) ) by A1,SERIES_1:24
.= 1/( (b/b)-(1/b) ) by XCMPLX_1:60,A0
.= 1/((b-1)/b) by XCMPLX_1:120
.= b/(b-1) by XCMPLX_1:57;
hence thesis;
end;
registration let n be Nat;
cluster seq_const n -> NAT-valued;
coherence;
end;
registration let r be positive Nat;
cluster seq_const r -> positive-yielding;
coherence;
end;
registration
cluster NAT-valued INT-valued for Real_Sequence;
existence
proof
take f = seq_const 0;
thus thesis;
end;
end;
theorem Th14:
for F be Real_Sequence, n be Nat, a be Real st (for k be Nat holds F.k = a)
holds (Partial_Sums F).n = a * (n+1)
proof
let F be Real_Sequence, n be Nat, a be Real;
assume
A1: for k be Nat holds F.k = a;
defpred P[Nat] means (Partial_Sums F).$1 = a*($1 + 1);
(Partial_Sums F).0 = F.0 by SERIES_1:def 1; then
A2: P[0] by A1;
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A4: P[i];
reconsider i1 = i+1, One = 1 as Real;
(Partial_Sums F).(i+1) = (Partial_Sums F).i + F.(i+1) by SERIES_1:def 1;
then
(Partial_Sums F).(i+1) = a*(i+1) + a by A1,A4;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
for n be Nat,a be Real holds (Partial_Sums seq_const a).n = a * (n + 1)
proof
let n be Nat, a be Real;
set f = seq_const a;
for k be Nat holds f.k = a by SEQ_1:57;
hence thesis by Th14;
end;
registration let f be INT-valued Real_Sequence;
cluster Partial_Sums f -> INT-valued;
coherence
proof
set g = Partial_Sums f;
rng g c= INT
proof
let y be object;
assume y in rng g; then
consider x be object such that
A0: x in dom g & y = g.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A0,FUNCT_2:def 1;
defpred P[Nat] means g.$1 is integer;
g.0 = f.0 by SERIES_1:def 1; then
A1: P[0];
A2: for k be Nat st P[k] holds P[k + 1]
proof let k be Nat;
assume
A3: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
g.(k+1) = g.k + f.(k+1) by SERIES_1:def 1;
hence thesis by A3;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2); then
g.n is integer;
hence thesis by A0,INT_1:def 2;
end;
hence thesis by RELAT_1:def 19;
end;
end;
registration
let f be NAT-valued Real_Sequence;
cluster Partial_Sums f -> NAT-valued;
coherence
proof
set g = Partial_Sums f;
rng g c= NAT
proof
let y be object;
assume y in rng g; then
consider x be object such that
A0: x in dom g & y = g.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A0,FUNCT_2:def 1;
defpred P[Nat] means g.$1 is Nat;
g.0 = f.0 by SERIES_1:def 1; then
A1: P[0];
A2: for k be Nat st P[k] holds P[k+1]
proof let k be Nat;
assume
A3: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
g.(k+1) = g.k + f.(k+1) by SERIES_1:def 1;
hence thesis by A3;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
then g.n is Nat;
hence thesis by A0,ORDINAL1:def 12;
end;
hence thesis by RELAT_1:def 19;
end;
end;
theorem
for f be Real_Sequence st ex n be Nat st (for k be Nat st k >= n holds f.k=0)
holds ex n be Nat st for k be Nat st k >= n holds
(Partial_Sums f).k = (Partial_Sums f).n
proof
let f be Real_Sequence;
given n being Nat such that
A1: for k being Nat st k >= n holds f.k = 0;
set p = Partial_Sums f;
reconsider pk = p.n as Real;
set r = seq_const pk;
A2: for k being Nat st k >= n holds p.k = r.k
proof
let k be Nat;
assume
A3: k >= n;
defpred P[Nat] means p.$1 = r.$1;
A4: P[n] by SEQ_1:57;
A5: for i being Nat st n <= i holds P[i] implies P[i+1]
proof
let i be Nat;
assume
A6: n <= i;
assume
A7: P[i];
p.(i+1)
= p.i + f.(i+1) by SERIES_1:def 1
.= r.i + 0 by A1,A6,A7,NAT_1:12
.= pk by SEQ_1:57
.= r.(i + 1);
hence thesis;
end;
for k being Nat st n <= k holds P[k] from NAT_1:sch 8(A4,A5);
hence thesis by A3;
end;
take n;
let k be Nat;
assume k >= n; then
p.k = r.k by A2 .= p.n by SEQ_1:57;
hence thesis;
end;
theorem Th16:
for f be INT-valued Real_Sequence st ex n be Nat
st (for k be Nat st k >= n holds f.k = 0) holds Sum f is Integer
proof
let f be INT-valued Real_Sequence;
given n be Nat such that
A1: for k be Nat st k >= n holds f.k = 0;
set p = Partial_Sums f;
reconsider pk = p.n as Real;
set r = seq_const pk;
for k be Nat st k >= n holds p.k = r.k
proof
let k be Nat;
assume
A2: k >= n;
defpred P[Nat] means p.$1 = r.$1;
A3: P[n] by SEQ_1:57;
A4: for i be Nat st n <= i holds P[i] implies P[i+1]
proof
let i be Nat;
assume
A5: n <= i;
assume
A6: P[i];
p.(i+1)
= p.i + f.(i+1) by SERIES_1:def 1 .= r.i + 0 by A1,A5,A6,NAT_1:12
.= pk by SEQ_1:57 .= r.(i+1);
hence thesis;
end;
for k be Nat st n <= k holds P[k] from NAT_1:sch 8(A3,A4);
hence thesis by A2;
end; then
lim p = lim r by SEQ_4:19;
hence thesis;
end;
registration
let f be nonnegative-yielding Real_Sequence;
let n be Nat;
cluster f ^\ n -> nonnegative-yielding;
coherence
proof
rng (f ^\ n) c= rng f by NAT_1:55; then
for r be Real st r in rng (f ^\ n) holds 0 <= r by PARTFUN3:def 4;
hence thesis by PARTFUN3:def 4;
end;
end;
begin :: Transformations between Real Functions and Finite Sequences
definition let f be Real_Sequence, X be Subset of NAT;
func f |_ X -> Real_Sequence equals
(NAT --> 0) +* (f | X);
coherence
proof
set g = (NAT --> 0) +* (f | X);
A0: dom g = dom (NAT --> 0) \/ dom (f | X) by FUNCT_4:def 1
.= NAT \/ dom (f | X);
dom f = NAT by FUNCT_2:def 1; then
dom (f | X) = X by RELAT_1:62; then
A1: dom g = NAT by XBOOLE_1:12,A0;
rng g c= REAL;
hence thesis by A1,FUNCT_2:2;
end;
end;
registration let f be Real_Sequence, X be Subset of NAT;
cluster f | X -> NAT-defined;
coherence;
end;
registration let f be Real_Sequence, n be Nat;
cluster f |_ Seg n -> summable;
coherence
proof
set seq = f |_ Seg n;
for k be Nat st k >= n + 1 holds seq.k = 0
proof
let k be Nat;
assume k >= n + 1; then
k > n by NAT_1:16,XXREAL_0:2; then
not k in Seg n by FINSEQ_1:1; then
not k in dom (f | Seg n) by RELAT_1:57; then
seq.k = (NAT --> 0).k by FUNCT_4:11;
hence thesis;
end;
hence thesis by Th12;
end;
end;
registration let f be INT-valued Real_Sequence, n be Nat;
cluster f |_ Seg n -> INT-valued;
coherence;
end;
theorem
for f be Real_Sequence holds f |_ Seg 0 = seq_const 0
proof
let f be Real_Sequence;
set ff = f |_ Seg 0;
set g = seq_const 0;
for x be Element of NAT holds ff.x = g.x
proof
let x be Element of NAT;
not x in dom (f | Seg 0);
hence thesis by FUNCT_4:11;
end;
hence thesis by FUNCT_2:63;
end;
definition let f be Real_Sequence, n be Nat;
func FinSeq (f,n) -> FinSequence of REAL equals
f | Seg n;
coherence
proof
set g = f | Seg n;
A1: dom f = NAT by FUNCT_2:def 1;
dom g = Seg n by A1,RELAT_1:62; then
A2: g is FinSequence by FINSEQ_1:def 2;
rng g c= REAL;
hence thesis by A2,FINSEQ_1:def 4;
end;
end;
theorem Th17:
for f be Real_Sequence,k,n be Nat st k in Seg n holds (f |_ Seg n).k = f.k
proof
let f be Real_Sequence, k,n be Nat;
assume
A0: k in Seg n;
A1: dom f = NAT by FUNCT_2:def 1;
dom (f | Seg n) = Seg n by A1,RELAT_1:62; then
(f |_ Seg n).k = (f | Seg n).k by A0,FUNCT_4:13 .= f.k by A0,FUNCT_1:49;
hence thesis;
end;
theorem Th18:
for f be Real_Sequence, n be Nat st f.0 = 0 holds
Sum FinSeq (f,n) = Sum (f |_ Seg n)
proof
let f be Real_Sequence, n be Nat;
assume
A0: f.0 = 0;
set f1 = f |_ Seg n;
set g = FinSeq (f,n);
reconsider f0 = f.0 as Element of REAL;
set h = <*f0*> ^ g;
A1: dom f = NAT by FUNCT_2:def 1;
A2: dom g = Seg n by A1,RELAT_1:62; then
Seg len g = Seg n by FINSEQ_1:def 3; then
A3: len g = n by FINSEQ_1:6;
len h = len <*f0*> + len g by FINSEQ_1:22; then
A4: len h = n + 1 by A3,FINSEQ_1:39;
reconsider g as FinSequence of REAL;
A5: len <*f0*> = 1 by FINSEQ_1:39;
A6: for k be Nat st k < n + 1 holds f1.k = h.(k+1)
proof
let k be Nat;
assume k < n + 1; then
A7: k <= n by NAT_1:13;
per cases by NAT_1:14;
suppose
A8: 1 <= k; then
A9: k in dom g by FINSEQ_3:25,A7,A3;
A10: (f | Seg n).k = f.k by FUNCT_1:49,A2,FINSEQ_3:25,A7,A3,A8;
(f |_ Seg n).k = f.k by A2,A8,Th17,FINSEQ_3:25,A7,A3;
hence thesis by FINSEQ_1:def 7,A5,A9,A10;
end;
suppose
A11: k = 0; then
not k in Seg n by FINSEQ_1:1; then
not k in dom (f | Seg n) by RELAT_1:57; then
f1.k = (NAT --> 0).k by FUNCT_4:11;
hence thesis by A0,A11;
end;
end;
for k be Nat st k >= n + 1 holds f1.k = 0
proof
let k be Nat;
assume k >= n + 1; then
k > n by XXREAL_0:2,NAT_1:16; then
not k in Seg n by FINSEQ_1:1; then
not k in dom (f | Seg n) by RELAT_1:57; then
f1.k = (NAT --> 0).k by FUNCT_4:11 .= 0;
hence thesis;
end; then
Sum f1 = Sum h by IRRAT_1:18,A6,A4; then
Sum f1 = f0 + Sum g by RVSUM_1:76;
hence thesis by A0;
end;
theorem Th19:
for f be Real_Sequence, n be Nat holds dom FinSeq (f,n) = Seg n
proof
let f be Real_Sequence, n be Nat;
dom f = NAT by FUNCT_2:def 1;
hence thesis by RELAT_1:62;
end;
theorem Th20:
for f be Real_Sequence,i be Nat holds
(FinSeq(f,i))^<* f.(i+1) *> = FinSeq(f,i+1)
proof
let f be Real_Sequence, i be Nat;
set f1 = FinSeq (f,i), g = <*f.(i+1)*>, h = FinSeq (f,i + 1);
dom f1 = Seg i by Th19; then
Seg len f1 = Seg i by FINSEQ_1:def 3; then
A0: len f1 = i by FINSEQ_1:6;
A1: dom (f1^g) = Seg (len f1 + len g) by FINSEQ_1:def 7
.= Seg (i+1) by FINSEQ_1:39,A0
.= dom h by Th19;
for k be Nat st k in dom (f1^g) holds (f1^g).k = h.k
proof
let k be Nat;
i <= i + 1 by NAT_1:13; then
A2: Seg i c= Seg (i + 1) by FINSEQ_1:5;
assume k in dom (f1 ^ g); then
per cases by FINSEQ_1:25;
suppose
A3: k in dom f1; then
A4: k in Seg i by Th19;
(f1^g).k = f1.k by FINSEQ_1:def 7,A3
.= f.k by A4,FUNCT_1:49 .= h.k by A2,A4,FUNCT_1:49;
hence thesis;
end;
suppose ex n be Nat st n in dom g & k = len f1 + n; then
consider n be Nat such that
A5: n in dom g & k = len f1 + n;
n in Seg 1 by A5,FINSEQ_1:def 8; then
A6: n = 1 by TARSKI:def 1,FINSEQ_1:2;
1 <= i + 1 by NAT_1:12;
hence thesis by FUNCT_1:49,FINSEQ_1:1,A0,A5,A6;
end;
end;
hence thesis by A1,FINSEQ_1:13;
end;
theorem Th21:
for f be Real_Sequence,n be Nat st f.0 = 0
holds Sum FinSeq (f,n) = (Partial_Sums f).n
proof
let f be Real_Sequence, n be Nat;
assume
A0: f.0 = 0;
defpred P[Nat] means
Sum FinSeq (f,$1) = (Partial_Sums f).$1;
Sum FinSeq (f,0) = 0 .= (Partial_Sums f).0 by A0,SERIES_1:def 1; then
A1: P[0];
A2: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A3: P[i];
A4: (FinSeq (f,i))^<*f.(i+1)*> = FinSeq (f,i+1) by Th20;
(Partial_Sums f).(i+1) = (Partial_Sums f).i + f.(i+1) by SERIES_1:def 1
.= (addreal "**" (FinSeq (f,i))) + f.(i+1) by RVSUM_1:def 12,A3
.= addreal.((addreal "**" (FinSeq (f,i))),f.(i+1)) by BINOP_2:def 9
.= addreal "**" ((FinSeq (f,i)) ^ <*f.(i+1)*>) by FINSOP_1:4
.= Sum FinSeq (f,i+1) by RVSUM_1:def 12,A4;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th22:
for f be Real_Sequence, n be Nat st f.0 = 0 holds
Sum (f |_ Seg n) = (Partial_Sums f).n
proof
let f be Real_Sequence, n be Nat;
assume
A1: f.0 = 0;
Sum FinSeq (f,n) = (Partial_Sums f).n by A1,Th21;
hence thesis by A1,Th18;
end;
theorem
for f be INT-valued Real_Sequence, n be Nat st f.0 = 0 holds
Sum (f |_ Seg n) is Integer
proof
let f be INT-valued Real_Sequence, n be Nat;
assume
A1: f.0 = 0;
set ff = f |_ Seg n;
Sum ff = (Partial_Sums f).n by Th22,A1;
hence thesis;
end;
theorem Th23:
for f be Real_Sequence, n be Nat st f is summable & f.0 = 0 holds
Sum f = Sum FinSeq (f,n) + Sum (f ^\ (n+1))
proof
let f be Real_Sequence, n be Nat;
assume
A1: f is summable & f.0 = 0; then
Sum f = Partial_Sums(f).n + Sum (f ^\ (n+1)) by SERIES_1:15;
hence thesis by A1,Th21;
end;
:: |_ is the same as SETWOP_2:def 1, p is FinSequence
registration
cluster positive-yielding NAT-valued for Real_Sequence;
existence
proof
take seq_const 1;
thus thesis;
end;
end;
begin :: Sequences not Vanishing at Infinity
definition
let f be Real_Sequence;
attr f is eventually-non-zero means :ENZ:
for n be Nat
ex N be Nat st n <= N & f.N <> 0;
end;
registration
cluster eventually-nonzero -> eventually-non-zero for Real_Sequence;
coherence
proof
let f be Real_Sequence;
assume
A1: f is eventually-nonzero;
let n be Nat;
consider N be Nat such that
A2: for k be Nat st k >= N holds f.k <> 0 by A1;
reconsider m = max (N,n) as Nat;
f.m <> 0 by A2,XXREAL_0:25;
hence thesis by XXREAL_0:25;
end;
end;
registration
cluster seq_id id NAT -> eventually-nonzero;
coherence
proof
set f = seq_id id NAT;
A0: dom id NAT = NAT;
rng id NAT c= REAL; then
A1: id NAT is Function of NAT, REAL by A0,FUNCT_2:2;
take N = 1;
let n be Nat;
assume n >= N;
hence thesis by FUNCT_1:18,A1,ORDINAL1:def 12;
end;
end;
registration
cluster eventually-non-zero for Real_Sequence;
existence
proof
take f = seq_id id NAT;
thus thesis;
end;
end;
theorem Th24:
for f be eventually-non-zero Real_Sequence holds
for n be Nat holds f ^\ n is eventually-non-zero
proof
let f be eventually-non-zero Real_Sequence, n be Nat;
set g = f ^\ n;
let k be Nat;
consider N be Nat such that
A1: k + n <= N & f.N <> 0 by ENZ;
k <= N - n by A1,XREAL_1:19; then
N - n in NAT by INT_1:3; then
reconsider Nn = N - n as Nat;
take Nn;
g.Nn = f.(Nn+n) by NAT_1:def 3
.= f.N;
hence thesis by A1,XREAL_1:19;
end;
registration let f be eventually-non-zero Real_Sequence, n be Nat;
cluster f ^\ n -> eventually-non-zero for Real_Sequence;
coherence by Th24;
end;
registration
cluster non-zero constant -> eventually-non-zero for Real_Sequence;
coherence
proof
let f be Real_Sequence;
assume
A0: f is non-zero constant;
consider x be set such that
A1: x in dom f & the_value_of f = f.x by FUNCT_1:def 12,A0;
A2: the_value_of f in rng f by A1,FUNCT_1:3;
reconsider v = the_value_of f as Real by A1;
A3: dom f = NAT by FUNCT_2:def 1;
let n be Nat;
take N = n + 1;
thus thesis by A0,A1,A2,A3,XREAL_1:31,FUNCT_1:def 10;
end;
end;
definition let b be Nat;
func powerfact b -> Real_Sequence means :DefPower:
for i be Nat holds it.i = 1/(b to_power (i!));
correctness
proof
deffunc F(Nat) = 1/(b to_power ($1!));
thus (ex f be Real_Sequence st for n be Nat holds f.n = F(n)) &
for f1, f2 be Real_Sequence st (for n be Nat holds f1.n = F(n)) &
(for n be Nat holds f2.n = F(n)) holds f1 = f2 from IRRAT_1:sch 1;
end;
end;
theorem Th25:
for b,i be Nat st b >= 1 holds (powerfact b).i <= ((1/b) GeoSeq).i
proof
let b,i be Nat;
assume
A1: b >= 1;
A3: (powerfact b).i = 1/(b to_power (i!)) by DefPower;
A2: ((1/b) GeoSeq).i = (1/b)|^i by PREPOWER:def 1
.= 1/(b to_power i) by PREPOWER:7;
1 * (b to_power i) <= 1 * (b to_power (i!)) by A1,PRE_FF:8,NEWTON:38;
hence thesis by A2,A3,A1,XREAL_1:102;
end;
theorem Th26:
for b be Nat st b > 1 holds
powerfact b is summable & Sum powerfact b <= b/(b - 1)
proof
let b be Nat;
assume
A1: b > 1; then
|. 1/b .| < 1/1 by XREAL_1:76; then
A3: (1/b) GeoSeq is summable by SERIES_1:24;
A2: for i be Nat holds 0 <= (powerfact b).i
proof
let i be Nat;
(powerfact b).i = 1/(b to_power (i!)) by DefPower;
hence thesis;
end;
A4: for i be Nat holds (powerfact b).i <= ((1/b) GeoSeq).i by A1,Th25;
then
Sum powerfact b <= Sum ((1/b) GeoSeq) by A2,A3,SERIES_1:20;
hence thesis by Th13,A1,A2,A3,A4,SERIES_1:20;
end;
registration let b be non trivial Nat;
cluster powerfact b -> summable;
coherence
proof
b >= 1+1 by NAT_2:29; then
b > 1 by NAT_1:13;
hence thesis by Th26;
end;
end;
registration
cluster nonnegative-yielding for Real_Sequence;
existence
proof
take seq_const 1;
thus thesis;
end;
end;
theorem Th27:
for n, b be Nat st b > 1 & n >= 1 holds
Sum( (b-1)(#)((powerfact b)^\(n+1)) ) < 1/((b to_power(n!)) to_power n)
proof
let n, b be Nat;
assume
A0: b > 1 & n >= 1; then
(powerfact b)^\(n + 1) is summable by Th26,SERIES_1:12; then
A2: Sum ((b-1)(#)((powerfact b)^\(n+1))) = (b-1)*Sum(((powerfact b)^\(n+1)))
by SERIES_1:10;
1 < b - 0 by A0; then
A3: b - 1 > 0 by XREAL_1:12;
set s1 = (powerfact b) ^\ (n+1);
set s2 = ((1/b) GeoSeq) ^\ ((n+1)!);
A4: |. 1/b .| < 1/1 by A0,XREAL_1:76; then
A5: (1 / b) GeoSeq is summable by SERIES_1:24;
A6: for k be Nat holds 0 <= s1.k & s1.k <= s2.k
proof
let k be Nat;
A7: s1.k = (powerfact b).(k+(n+1)) by NAT_1:def 3
.= 1/(b to_power((k+(n+1))!)) by DefPower;
k = 0 or k >= 1 + 0 by NAT_1:13; then
per cases;
suppose
A8: k >= 1;
A9: s2.k = ((1/b) GeoSeq).(k+(n+1)!) by NAT_1:def 3
.= (1/b)|^(k+(n+1)!) by PREPOWER:def 1
.= 1/(b|^(k+(n+1)!)) by PREPOWER:7;
n+1 >= 1 by A0,NAT_1:16; then
b to_power (k+(n+1)!) <= b to_power((k+(n+1))!) by PRE_FF:8,A0,Th8,A8;
then
(b|^(k+(n+1)!))" >= (b|^((k+(n+1))!))" by A0,XREAL_1:85; then
1/(b|^(k+(n+1)!)) >= (b|^((k+(n+1))!))" by XCMPLX_1:215;
hence thesis by A7,A9,XCMPLX_1:215;
end;
suppose
A10: k = 0; then
A11: s1.k = (powerfact b).(0+(n+1)) by NAT_1:def 3
.= 1/(b to_power((n+1)!)) by DefPower;
hence s1.k >= 0;
s2.k = ((1/b) GeoSeq).(0+(n+1)!) by NAT_1:def 3,A10
.= (1/b)|^(0+(n+1)!) by PREPOWER:def 1
.= 1/(b|^(0+(n+1)!)) by PREPOWER:7;
hence thesis by A11;
end;
end;
A12: s2 is summable by A4,SERIES_1:12,SERIES_1:24;
ex k be Nat st 1 <= k & s1.k < s2.k
proof
take k = 2;
A13: s1.k = (powerfact b).(k+(n+1)) by NAT_1:def 3
.= 1/(b to_power ((k+(n+1))!)) by DefPower;
A14: s2.k = ((1/b) GeoSeq).(k+(n+1)!) by NAT_1:def 3
.= (1/b)|^(k+(n+1)!) by PREPOWER:def 1
.= 1/(b|^(k+(n+1)!)) by PREPOWER:7;
n + 1 > 0 + 1 by A0,XREAL_1:8; then
b to_power (k+(n+1)!) < b to_power ((k+(n+1))!)
by POWER:39,A0,Th6; then
(b|^(k+(n+1)!))" > (b|^((k+(n+1))!))" by A0,XREAL_1:88; then
1/(b|^(k+(n+1)!)) > (b|^((k+(n+1))!))" by XCMPLX_1:215;
hence thesis by A13,A14,XCMPLX_1:215;
end; then
Sum s1 < Sum s2 by A6,A12,Th11; then
A15: (b-1)*Sum(((powerfact b)^\(n+1))) <
(b-1)*Sum(((1/b) GeoSeq)^\((n+1)!)) by XREAL_1:68,A3;
reconsider bn = b |^ ((n + 1)!) as Nat;
A16: ((1/b) GeoSeq)^\((n+1)!) = (1/bn)(#)((1/b) GeoSeq)
proof
now let i be Element of NAT;
thus
(((1/b) GeoSeq)^\((n+1)!)).i=(((1/b) GeoSeq).(i+(n+1)!)) by NAT_1:def 3
.= ((1/b)|^(i+(n+1)!)) by PREPOWER:def 1
.= ((1/b)|^i * (1/b)|^((n+1)!)) by NEWTON:8
.= (1/b)|^i * (1/(b|^((n+1)!))) by PREPOWER:7
.= (1/(b|^((n+1)!))) * (((1/b) GeoSeq).i) by PREPOWER:def 1
.= (1/((b|^((n + 1)!))) (#) ((1/b) GeoSeq)).i by VALUED_1:6;
end;
hence thesis by FUNCT_2:63;
end;
Sum(((1/b) GeoSeq)^\((n+1)!)) = (1/(b|^((n+1)!)))*Sum ((1/b) GeoSeq)
by A16,A5,SERIES_1:10
.= (1/(b|^((n+1)!)))*(b/(b-1)) by Th13,A0
.= (1 * b)/((b|^((n+1)!))*(b-1)) by XCMPLX_1:76
.= b/((b|^((n+1)!))*(b-1)); then
A17: (b-1)*Sum(((1/b) GeoSeq)^\((n+1)!))
= (b-1)*((b/bn)/(b-1)) by XCMPLX_1:78
.= (b-1)*(b/bn)/(b-1) by XCMPLX_1:74
.= b/(b|^((n+1)!)) by A3,XCMPLX_1:89;
n! >= 1 by Th2; then
A18: b/(b|^((n+1)!)) <= (b|^(n!))/(b|^((n+1)!)) by XREAL_1:72,A0,PREPOWER:12;
(b|^(n!))/(b|^((n+1)!))
= (b to_power (n!))/(b to_power ((n + 1)!))
.= b to_power (n! - (n+1)!) by POWER:29,A0
.= b to_power (- ((n+1)! - n!))
.= b to_power (-(n * (n!))) by Th3
.= 1/(b to_power (n * (n!))) by POWER:28,A0
.= 1/((b to_power (n!)) to_power n) by POWER:33,A0;
hence thesis by A2,A15,XXREAL_0:2,A17,A18;
end;
begin :: Liouville Numbers
::$N Liouville number
definition let x be Real;
attr x is liouville means
for n being Nat
ex p being Integer,
q being Nat st q > 1 &
0 < |. x - p / q .| < 1 / (q |^ n);
end;
theorem Def2:
for r being Real holds r is liouville iff
for n being non zero Nat ex p being Integer, q being Nat st 1 < q &
0 < |. r - p/q .| < 1 / (q |^ n)
proof
let r be Real;
thus r is liouville implies
for n being non zero Nat ex p being Integer, q being Nat st 1 < q &
0 < |. r - p/q .| < 1 / (q |^ n);
assume
Z1: for n being non zero Nat
ex p being Integer, q being Nat st
1 < q & 0 < |. r - p/q .| < 1 / (q |^ n);
let n be Nat;
per cases;
suppose n is non zero;
hence thesis by Z1;
end;
suppose
A1: n is zero;
consider p being Integer, q being Nat such that
A2: 1 < q and
A3: 0 < |. r - p/q .| and
A4: |. r - p/q .| < 1 / (q |^ 1) by Z1;
take p,q;
thus 1 < q & 0 < |. r - p/q .| by A2,A3;
A5: q |^ 0 = 1 by NEWTON:4;
1 / q < 1 / 1 by A2,XREAL_1:76;
hence thesis by A1,A4,A5,XXREAL_0:2;
end;
end;
definition let a be Real_Sequence, b be Nat;
func Liouville_seq (a,b) -> Real_Sequence means :DefLio:
it.0 = 0 &
for k be non zero Nat holds it.k = (a.k)/(b to_power(k!));
existence
proof
deffunc G(Nat,Element of REAL) =
In ((a.($1 + 1)) / (b to_power (($1 + 1)!)),REAL);
deffunc A() = In(0,REAL);
consider f be sequence of REAL such that
A1: f.0 = A() &
for n be Nat holds f.(n+1) = G(n,f.n) from NAT_1:sch 12;
reconsider f as Real_Sequence;
take f;
thus f.0 = 0 by A1;
let n be non zero Nat;
consider k be Nat such that
A2: k + 1 = n by NAT_1:6;
f.(k+1) = G(k,f.k) by A1
.= (a.(k + 1))/(b to_power((k + 1)!));
hence thesis by A2;
end;
uniqueness
proof
let f1,f2 be Real_Sequence;
assume that
A1: f1.0 = 0 &
for n be non zero Nat holds f1.n = (a.n)/(b to_power(n!)) and
A2: f2.0 = 0 &
for n be non zero Nat holds f2.n = (a.n)/(b to_power (n!));
for n be Element of NAT holds f1.n = f2.n
proof
let n be Element of NAT;
per cases;
suppose n = 0;
hence thesis by A1,A2;
end;
suppose
A3: n <> 0; then
f1.n = (a.n)/(b to_power(n!)) by A1
.= f2.n by A2,A3;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
::$N Liouville number!irrationality
registration
cluster liouville -> irrational for Real;
coherence
proof
let x be Real;
assume
A0: x is liouville;
assume x is rational; then
consider c be Integer, d be Nat such that
A1: d > 0 & x = c/d by RAT_1:8;
consider n be non zero Nat such that
ST: 2 to_power (n-1) > d by Th10;
consider p be Integer, q be Nat such that
B1: q > 1 & 0 < |. x - p/q .| < 1/(q|^n) by A0;
SS: |. c/d - p/q .| = |. (c*q - p*d)/(d*q) .| by XCMPLX_1:130,B1,A1
.= |. (c * q - p * d) .|/|. d * q .| by COMPLEX1:67
.= |. (c * q - p * d) .|/(d * q);
c * q - p * d <> 0
proof
assume c * q - p * d = 0; then
p/q = c/d by XCMPLX_1:94,B1,A1;
hence thesis by B1,A1;
end; then
HR: |. x - p/q .| >= 1/(d * q) by SS,A1,XREAL_1:72,NAT_1:14;
d * q < (2 to_power(n-1)) * q by B1,ST,XREAL_1:68; then
1/(d*q) > 1/((2 to_power(n-1))*q) by XREAL_1:76,A1,B1; then
HG: |. x - p/q .| >= 1/((2 to_power (n-1))* q) by HR,XXREAL_0:2;
FG: 2 to_power (n - 1) > 0 by POWER:34;
n - 0 >= 1 by NAT_1:14; then
FO: n - 1 >= 0 by XREAL_1:11;
1 + 1 <= q by B1,NAT_1:13; then
2 to_power (n-1) <= q to_power (n-1) by FO,HOLDER_1:3; then
(2 to_power (n-1))*q <= (q to_power (n-1))*(q to_power 1) by XREAL_1:66,FG;
then
(2 to_power (n-1))*q <= (q to_power (n-1+1)) by B1,POWER:27; then
qa:(2 to_power (n-1)) * q <= q to_power n;
2 to_power (n-1) > 0 by POWER:34; then
1/((2 to_power (n-1)) * q) >= 1/q|^n by XREAL_1:118,qa,B1;
hence thesis by B1,XXREAL_0:2,HG;
end;
end;
begin :: Liouville Constant
::$N Liouville's constant
definition let a be Real_Sequence,b be Nat;
func Liouville_constant (a,b) -> Real equals
Sum Liouville_seq (a,b);
coherence;
end;
definition let b be Nat;
func BLiouville_seq b -> Real_Sequence means :LiuSeq:
for n be Nat holds it.n = b to_power (n!);
correctness
proof
deffunc F(Nat) = b to_power ($1!);
thus (ex f be Real_Sequence st for n be Nat holds f.n = F(n)) &
for f1, f2 be Real_Sequence st (for n be Nat holds f1.n = F(n)) &
(for n be Nat holds f2.n = F(n)) holds f1 = f2 from IRRAT_1:sch 1;
end;
end;
registration let b be Nat;
cluster BLiouville_seq b -> NAT-valued;
coherence
proof
set f = BLiouville_seq b;
let x be object;
assume x in rng f; then
consider n be object such that
AB: n in dom f & x = f.n by FUNCT_1:def 3;
reconsider n as Nat by AB;
f.n = b to_power (n!) by LiuSeq;
hence thesis by AB;
end;
end;
definition let a be Real_Sequence, b be Nat;
func ALiouville_seq (a,b) -> Real_Sequence means :ALiuDef:
for n be Nat holds
it.n = (BLiouville_seq b).n * Sum (Liouville_seq (a,b) |_ Seg n);
correctness
proof
deffunc F(Nat)
= (BLiouville_seq b).$1 * Sum (Liouville_seq (a,b) |_ Seg $1);
thus (ex f be Real_Sequence st for n be Nat holds f.n = F(n)) &
for f1, f2 be Real_Sequence st
(for n be Nat holds f1.n = F(n)) & (for n be Nat holds f2.n = F(n))
holds f1 = f2 from IRRAT_1:sch 1;
end;
end;
theorem Th28:
for a be NAT-valued Real_Sequence,b,n,k be Nat st b > 0 & k <= n holds
(Liouville_seq (a,b).k) * (BLiouville_seq b).n is Integer
proof
let a be NAT-valued Real_Sequence, b,n,k be Nat;
assume
A1: b > 0 & k <= n; then
0 + k! <= n! by SIN_COS:39; then
A2: n! - k! in NAT by INT_1:3,XREAL_1:19;
set bk = b to_power (k!), bn = b to_power (n!);
A3: bn / bk = b to_power (n! - k!) by A1,POWER:29;
per cases;
suppose k = 0; then
Liouville_seq (a,b).k = 0 by DefLio;
hence thesis;
end;
suppose
k is non zero; then
(Liouville_seq (a,b)).k = (a.k)/(b to_power (k!)) by DefLio; then
(Liouville_seq (a,b).k) * (BLiouville_seq b).n
= ((a.k)/(b to_power (k!))) * ((b to_power(n!) /1)) by LiuSeq
.= ((a.k) * bn)/(bk * 1) by XCMPLX_1:76
.= (a.k) * (bn/bk) by XCMPLX_1:74;
hence thesis by A2,A3;
end;
end;
theorem Th29:
for a be NAT-valued Real_Sequence, b,n be Nat st b > 0 holds
ALiouville_seq (a,b).n is Integer
proof
let a be NAT-valued Real_Sequence,b,n be Nat;
set LS = Liouville_seq (a,b);
set BS = BLiouville_seq b;
set AS = ALiouville_seq (a,b);
set ff = BS.n (#) (LS |_ Seg n);
assume
A0: b > 0;
A1: AS.n = BS.n * Sum (LS |_ Seg n) by ALiuDef;
A2: BS.n * Sum (LS |_ Seg n) = Sum ff by SERIES_1:10;
rng ff c= INT
proof
let y be object;
assume y in rng ff; then
consider x be object such that
A3: x in dom ff & y = ff.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
A4: y = (BLiouville_seq b).n * (Liouville_seq (a,b) |_ Seg n).x
by A3,VALUED_1:6;
per cases;
suppose
A5: x in Seg n; then
A6: 1 <= x <= n by FINSEQ_1:1;
dom LS = NAT by FUNCT_2:def 1; then
x in dom (LS | Seg n) by A5,RELAT_1:62; then
A8: (Liouville_seq (a,b) |_ Seg n).x =
((Liouville_seq (a,b) | Seg n)).x by FUNCT_4:13
.= (Liouville_seq (a,b).x) by FUNCT_1:49,A5;
(Liouville_seq (a,b).x) * (BLiouville_seq b).n is Integer
by A0,A6,Th28;
hence thesis by INT_1:def 2,A4,A8;
end;
suppose
not x in Seg n; then
not x in dom (Liouville_seq (a,b) | Seg n) by RELAT_1:57; then
(Liouville_seq (a,b) |_ Seg n).x = (NAT --> 0).x by FUNCT_4:11;
hence thesis by INT_1:def 2,A4;
end;
end; then
reconsider ff as INT-valued Real_Sequence by RELAT_1:def 19;
set m = n + 1;
for k be Nat st k >= m holds ff.k = 0
proof
let k be Nat;
assume k >= m; then
k > n by NAT_1:13; then
not k in Seg n by FINSEQ_1:1; then
A9: not k in dom (LS | Seg n) by RELAT_1:57;
A10: ff.k = BS.n * ((LS |_ Seg n).k) by VALUED_1:6;
(LS |_ Seg n).k = (NAT --> 0).k by FUNCT_4:11,A9
.= 0;
hence thesis by A10;
end;
hence thesis by A1,A2,Th16;
end;
registration let a be NAT-valued Real_Sequence;
let b be non zero Nat;
cluster ALiouville_seq (a,b) -> INT-valued;
coherence
proof
set f = ALiouville_seq (a,b);
rng f c= INT
proof
let y be object;
assume y in rng f; then
consider x be object such that
A1: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Nat by A1;
y is Integer by Th29,A1;
hence thesis by INT_1:def 2;
end;
hence thesis by RELAT_1:def 19;
end;
end;
theorem Th30:
for n,b be non zero Nat st b > 1 holds (BLiouville_seq b).n > 1
proof
let n,b be non zero Nat;
assume
A1: b > 1;
(BLiouville_seq b).n = b to_power (n!) by LiuSeq;
hence thesis by A1,POWER:35;
end;
theorem Th31:
for a be NAT-valued Real_Sequence, b be non zero Nat st
b >= 2 & rng a c= b holds Liouville_seq (a,b) is summable
proof
let a be NAT-valued Real_Sequence, b be non zero Nat;
assume
A1: b >= 2 & rng a c= b;
A2: b > 1 by A1,XXREAL_0:2; then
A3: b - 1 >= 0 by XREAL_1:48;
set f = Liouville_seq (a,b);
A4: for i be Nat holds (b-1)/(b to_power (i!)) = ((b-1)(#)(powerfact b)).i
proof
let i be Nat;
((b - 1)(#)(powerfact b)).i
= (b - 1)*((powerfact b).i) by VALUED_1:6
.= (b - 1) * (1 / (b to_power (i!))) by DefPower
.= (b - 1) / (b to_power (i!)) by XCMPLX_1:99;
hence thesis;
end;
A5: for i be Nat holds
f.i >= 0 & f.i <= ((b - 1) (#) (powerfact b)).i
proof
let i be Nat;
reconsider b1 = b - 1 as Element of NAT by INT_1:3,XREAL_1:48,A2;
per cases;
suppose
A6: i is zero; then
A7: f.i = 0 by DefLio;
A8: b to_power (i!) = b by NEWTON:12,A6;
(b - 1) / b >= 0 by A3;
hence thesis by A7,A4,A8;
end;
suppose
A9: i is non zero; then
reconsider ii = i as non zero Nat;
A10: f.i = (a.i)/(b to_power (i!)) by A9,DefLio;
reconsider ai = a.i as Nat;
a.i in rng a by NAT_1:51; then
a.i in b by A1; then
a.i in Segm b by ORDINAL1:def 17; then
ai < b1 + 1 by NAT_1:44; then
ai <= b1 by NAT_1:13; then
f.i <= (b - 1) / (b to_power (i!)) by A10,XREAL_1:72;
hence thesis by A4,A10;
end;
end;
powerfact b is summable by A2,Th26; then
(b - 1) (#) (powerfact b) is summable by SERIES_1:10;
hence thesis by A5,SERIES_1:20;
end;
theorem Th32:
for a be Real_Sequence,n be non zero Nat, b be non zero Nat st b > 1
holds (ALiouville_seq(a,b)).n /(BLiouville_seq b).n
= Sum FinSeq (Liouville_seq (a,b),n)
proof
let a be Real_Sequence, n, b be non zero Nat;
assume b > 1; then
A1: (BLiouville_seq b).n <> 0 by Th30;
A2: Liouville_seq (a,b).0 = 0 by DefLio;
thus (ALiouville_seq (a,b)).n / (BLiouville_seq b).n
= (BLiouville_seq b).n * Sum (Liouville_seq (a,b) |_ Seg n) /
(BLiouville_seq b).n by ALiuDef
.= Sum (Liouville_seq (a,b) |_ Seg n) by XCMPLX_1:89,A1
.= Sum FinSeq (Liouville_seq (a,b),n) by Th18,A2;
end;
theorem Th33:
for a be NAT-valued Real_Sequence, b be non trivial Nat,n be Nat
holds Liouville_seq (a,b).n >= 0
proof
let a be NAT-valued Real_Sequence, b be non trivial Nat, n be Nat;
per cases;
suppose n = 0;
hence thesis by DefLio;
end;
suppose n <> 0; then
Liouville_seq (a,b).n = (a.n) / (b to_power (n!)) by DefLio;
hence thesis;
end;
end;
theorem
for a be positive-yielding NAT-valued Real_Sequence,
b be non trivial Nat,n be non zero Nat
holds Liouville_seq (a,b).n > 0
proof
let a be positive-yielding NAT-valued Real_Sequence,b be non trivial Nat,
n be non zero Nat;
A1: Liouville_seq (a,b).n = (a.n) / (b to_power (n!)) by DefLio;
n in NAT by ORDINAL1:def 12; then
n in dom a by FUNCT_2:def 1; then
a.n in rng a by FUNCT_1:3; then
a.n > 0 by PARTFUN3:def 1;
hence thesis by A1;
end;
registration
let a be NAT-valued Real_Sequence, b be non trivial Nat;
cluster Liouville_seq (a,b) -> nonnegative-yielding;
coherence
proof
let r be Real;
assume r in rng Liouville_seq (a,b); then
consider n be object such that
A1: n in dom Liouville_seq (a,b) & r = Liouville_seq (a,b).n by FUNCT_1:def 3;
thus thesis by A1,Th33;
end;
end;
theorem Th34:
for a be NAT-valued Real_Sequence, b, c be Nat
st b >= 2 & c >= 1 & rng a c= c & c <= b holds
for i be Nat holds Liouville_seq (a,b).i <= ((c - 1)(#)(powerfact b)).i
proof
let a be NAT-valued Real_Sequence,b, c be Nat;
assume
A1: b >= 2 & c >= 1 & rng a c= c & c <= b;
set f = Liouville_seq (a,b);
A2: for i be Nat holds (c-1)/(b to_power (i!)) = ((c-1)(#)(powerfact b)).i
proof
let i be Nat;
((c - 1) (#) (powerfact b)).i = (c - 1) * ((powerfact b).i) by VALUED_1:6
.= (c - 1) * (1 / (b to_power (i!))) by DefPower
.= (c - 1) / (b to_power (i!)) by XCMPLX_1:99;
hence thesis;
end;
let i be Nat;
A4: b >= 1 by A1,XXREAL_0:2;
reconsider b1 = b - 1 as Element of NAT by A4,INT_1:3,XREAL_1:48;
reconsider c1 = c - 1 as Element of NAT by A1,INT_1:3,XREAL_1:48;
per cases;
suppose
A5: i is zero; then
A6: f.i = 0 by DefLio;
A7: b to_power (i!) = b by NEWTON:12,A5;
c1 >= 0; then
(c - 1) / b >= 0;
hence thesis by A2,A6,A7;
end;
suppose
A8: i is non zero; then
reconsider ii = i as non zero Nat;
A9: f.i = (a.i) / (b to_power (i!)) by A8,DefLio;
reconsider ai = a.i as Nat;
a.i in rng a by NAT_1:51; then
a.i in c by A1; then
a.i in Segm c by ORDINAL1:def 17; then
ai < c1 + 1 by NAT_1:44; then
ai <= c1 by NAT_1:13; then
f.i <= (c - 1) / (b to_power (i!)) by A9,XREAL_1:72;
hence thesis by A2;
end;
end;
theorem
for a be NAT-valued Real_Sequence, b, c be Nat
st b >= 2 & c >= 1 & rng a c= c & c <= b holds
Sum Liouville_seq (a,b) <= Sum ((c - 1) (#) (powerfact b))
proof
let a be NAT-valued Real_Sequence, b, c be Nat;
assume
A0: b >= 2 & c >= 1 & rng a c= c & c <= b; then
b >= 1 + 1; then
b > 1 by NAT_1:13; then
powerfact b is summable by Th26; then
A1: ((c - 1) (#) (powerfact b)) is summable by SERIES_1:10;
b is 2_or_greater by A0,EC_PF_2:def 1; then
A2: for i be Nat holds 0 <= Liouville_seq (a,b).i by Th33;
for i be Nat holds Liouville_seq (a,b).i <= ((c-1)(#)(powerfact b)).i
by Th34,A0;
hence thesis by SERIES_1:20,A1,A2;
end;
theorem Th35:
for a be NAT-valued Real_Sequence, b, c, n be 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
let a be NAT-valued Real_Sequence, b, c, n be Nat;
set g = (c-1)(#)((powerfact b)^\(n+1));
assume
A0: b >= 2 & c >= 1 & rng a c= c & c <= b; then
b >= 1+1; then
b > 1 by NAT_1:13; then
(powerfact b)^\(n+1) is summable by Th26,SERIES_1:12; then
A1: (c-1)(#)((powerfact b)^\(n+1)) is summable by SERIES_1:10;
set f = (Liouville_seq (a,b)^\(n+1));
A2: b is 2_or_greater by A0,EC_PF_2:def 1;
A3: for i be Nat holds 0 <= f.i
proof
let i be Nat;
dom f = NAT by FUNCT_2:def 1; then
f.i in rng f by FUNCT_1:3,ORDINAL1:def 12;
hence thesis by A2,PARTFUN3:def 4;
end;
for i be Nat holds f.i <= g.i
proof
let i be Nat;
A4: f.i = Liouville_seq (a,b).(n+1+i) by NAT_1:def 3;
g.i = (c-1)*(((powerfact b)^\(n+1)).i) by SEQ_1:9
.= (c-1)*((powerfact b).(n+1+i)) by NAT_1:def 3
.= ((c-1)(#)(powerfact b)).(n+1+i) by SEQ_1:9;
hence thesis by A4,Th34,A0;
end;
hence thesis by SERIES_1:20,A1,A3;
end;
theorem Th36:
for a be NAT-valued Real_Sequence,b be non trivial Nat, n be Nat
st a is eventually-non-zero & rng a c= b holds
Sum(Liouville_seq (a,b) ^\ (n+1)) > 0
proof
let a be NAT-valued Real_Sequence, b be non trivial Nat, n be Nat;
assume
A1: a is eventually-non-zero & rng a c= b;
set LS = Liouville_seq (a,b) ^\ (n + 1);
A2: for i be Nat holds 0 <= LS.i
proof
let i be Nat;
LS.i = Liouville_seq (a,b).(n+1+i) by NAT_1:def 3;
hence thesis by Th33;
end;
ex i be Nat st i in dom LS & 0 < LS.i
proof
consider j be Nat such that
A3: n + 1 <= j & a.j <> 0 by A1;
j - (n + 1) in NAT by A3,INT_1:5; then
reconsider i = j - (n + 1) as Nat;
take i;
A4: n + 1 + i = j;
A5: dom LS = NAT by FUNCT_2:def 1;
LS.i = Liouville_seq (a,b).j by NAT_1:def 3,A4
.= (a.(n + 1 + i)) / (b to_power (j!)) by DefLio;
hence thesis by A5,A3,ORDINAL1:def 12;
end; then
consider k be Nat such that
A6: k in dom LS & LS.k > 0;
Liouville_seq (a,b) is summable by Th31,A1,NAT_2:29; then
LS is summable by SERIES_1:12;
hence thesis by A6,RSSPACE2:3,A2;
end;
theorem Th37:
for a be NAT-valued Real_Sequence, b be non trivial Nat st
rng a c= b & a is eventually-non-zero holds
for n be non zero Nat ex p be Integer, q be Nat st q > 1 &
0 < |. Liouville_constant (a,b) - p/q .| < 1/q|^n
proof
let a be NAT-valued Real_Sequence, b be non trivial Nat;
assume
A1: rng a c= b & a is eventually-non-zero;
set x = Liouville_constant (a,b);
A2: b >= 1 + 1 by NAT_2:29; then
A3: b > 1 by NAT_1:13;
set pn = ALiouville_seq (a,b);
set qn = BLiouville_seq b;
let n be non zero Nat;
A4: n >= 0 + 1 by NAT_1:13;
reconsider p = pn.n as Integer;
reconsider q = qn.n as Nat;
take p, q;
A5: q = b to_power (n!) by LiuSeq;
thus q > 1 by Th30,A3;
set LS = Liouville_seq (a,b);
A6: LS is summable by Th31,NAT_2:29,A1;
A7: Sum (Liouville_seq (a,b)^\(n+1)) > 0 by Th36,A1;
LS.0 = 0 by DefLio; then
A8: Sum LS = Sum FinSeq (LS,n) + Sum (LS^\(n+1)) by Th23,A6;
A9: |. x - p/q .|
= |. Sum Liouville_seq(a,b) - Sum FinSeq(Liouville_seq (a,b),n) .|
by A3,Th32
.= Sum (Liouville_seq (a,b)^\(n+1)) by A7,A8,ABSVALUE:def 1;
A10: Sum (Liouville_seq (a,b)^\(n+1))
<= Sum ((b-1)(#)((powerfact b)^\(n+1))) by A1,A2,A3,Th35;
Sum ((b-1) (#) ((powerfact b)^\(n+1)))
< 1/((b to_power (n!)) to_power n) by A3,A4,Th27;
hence thesis by A1,A5,A9,A10,XXREAL_0:2,Th36;
end;
definition
func Liouville_constant -> Real equals
Liouville_constant (seq_const 1,10);
correctness;
end;
theorem Th38:
for a be NAT-valued Real_Sequence, b be non trivial Nat st
rng a c= b & a is eventually-non-zero holds
Liouville_constant (a,b) is liouville
proof
let a be NAT-valued Real_Sequence, b be non trivial Nat;
assume
A1: rng a c= b & a is eventually-non-zero;
set x = Liouville_constant (a,b);
for n be non zero Nat ex p be Integer, q be Nat st q > 1 &
0 < |. x - p/q .| < 1/q|^n by Th37,A1;
hence thesis by Def2;
end;
registration
cluster Liouville_constant -> liouville;
coherence
proof
A0: rng seq_const 1 = {1} by FUNCOP_1:8;
A1: 1 in 10 by ENUMSET1:def 8,CARD_1:58;
10 is non trivial by NAT_2:28;
hence thesis by A1,Th38,A0,ZFMISC_1:31;
end;
end;
registration
cluster liouville for Real;
existence
proof
take Liouville_constant;
thus thesis;
end;
end;
definition
mode Liouville is liouville Real;
end;
theorem Th39:
for m,n be non zero Nat holds
(Liouville_seq (seq_const 1, m)).n = m to_power - n!
proof
let m,n be non zero Nat;
thus (Liouville_seq (seq_const 1, m)).n
= ((seq_const 1).n) / (m to_power (n!)) by DefLio
.= 1/(m to_power (n!)) by SEQ_1:57
.= (1/m) to_power (n!) by PREPOWER:7
.= m to_power -n! by POWER:32;
end;
:: Added by Reviewer
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
let m,n be non zero Nat;
assume
AS: 1 < m; then
1 + 1 <= m by INT_1:7; then
CCM2: 2 = m or 2 < m by XXREAL_0:1;
reconsider fn = n! as Real;
TT1: m to_power n <= m to_power fn by PRE_FF:8,ADDC1,AS;
zz: (Liouville_seq (seq_const 1, m)).n = m to_power -n! by Th39
.= m to_power -fn
.= 1 / (m to_power fn) by POWER:28; then
ZXC2: (Liouville_seq (seq_const 1, m)).n <= 1/(m to_power n)
by TT1,XREAL_1:118;
per cases by POWER:37,CCM2;
suppose 2 to_power n = m to_power n;
hence thesis by zz,TT1,XREAL_1:118;
end;
suppose 2 to_power n < m to_power n; then
1/(m to_power n) < 1/(2 to_power n) by XREAL_1:76;
hence thesis by ZXC2,XXREAL_0:2;
end;
end;
TLLC:
for m,n be Nat st 1 < m holds
(Liouville_seq (seq_const 1, m)).n <= 1 / (2 to_power n)
proof
let m,n be Nat;
assume AS: 1 < m;
per cases;
suppose n = 0;
hence thesis by DefLio;
end;
suppose n is non zero;
hence thesis by TC1,AS;
end;
end;
theorem
for m being Nat st 1 < m holds
Liouville_seq (seq_const 1, m) is negligible
proof
let m be Nat;
assume
AS: 1 < m;
ex f being Function of NAT,REAL
st for x be Nat holds f.x = 1 / (2 to_power x)
proof
deffunc F(Nat) = 1 / (2 to_power ($1));
(ex f being Real_Sequence st for n being Nat holds f.n = F(n)) &
for f1, f2 being Real_Sequence st
(for n being Nat holds f1.n = F(n)) &
(for n being Nat holds f2.n = F(n)) holds f1 = f2
from IRRAT_1:sch 1;
hence thesis;
end; then
consider f being Function of NAT,REAL such that
ACF: for x be Nat holds f.x = 1 / (2 to_power x);
set g = Liouville_seq (seq_const 1, m);
for x be Nat holds |. g.x .| <= |. f.x .|
proof
let x be Nat;
m1: f.x = 1 / (2 to_power x) by ACF; then
M1: g.x <= f.x by TLLC,AS;
0 <= g.x
proof
per cases;
suppose x = 0;
hence thesis by DefLio;
end;
suppose x is non zero; then
g.x = ((seq_const 1).x) / (m to_power (x!)) by DefLio;
hence thesis;
end;
end; then
-(f.x) <= g.x by m1; then
M3: |. g.x .| <= f.x by M1,ABSVALUE:5;
f.x <= |. f.x .| by ABSVALUE:4;
hence thesis by XXREAL_0:2,M3;
end;
hence thesis by ACF,ASYMPT_3:25,ASYMPT_3:26;
end;
theorem
1/10 < Liouville_constant <= 10/9 - 1/10
proof
set x = Liouville_constant;
set a = seq_const 1;
set b = 10;
set c = 2;
A0: rng a = {1} by FUNCOP_1:8;
A1: 1 in 10 by ENUMSET1:def 8,CARD_1:58;
A2: 10 is non trivial by NAT_2:28;
reconsider n = 1 as non zero Nat;
set f = Liouville_seq (a,b);
set pb = powerfact b;
A3: f is summable by Th31,A0,A1,ZFMISC_1:31;
for n be Nat holds 0 <= f.n by Th33,A2; then
A4: f.1 <= Sum f by RSSPACE2:3,A3;
A5: f.1 = 10 to_power -1 by NEWTON:13,Th39
.= (1/10) to_power 1 by POWER:32
.= 1/10;
set s1 = f ^\ 2;
set s2 = pb ^\ 2;
A6: (powerfact b).0 = 1/(b to_power(0!)) by DefPower .= 1/b by NEWTON:12;
A7: (powerfact b).1 = 1/(b to_power (1!)) by DefPower .= 1/b by NEWTON:13;
A8: (Partial_Sums pb).(0+1) = (Partial_Sums pb).0 + pb.(0+1) by SERIES_1:def 1
.= pb.0 + pb.(0 + 1) by SERIES_1:def 1;
Sum pb = (Partial_Sums pb).1 + Sum (pb^\(1+1)) by Th26,SERIES_1:15
.= 2/b + Sum s2 by A6,A7,A8; then
A9: Sum s2 = Sum pb - 2 / b;
Sum pb <= b/(b-1) by Th26; then
A10: Sum s2 <= b/(b-1) - 2/b by A9,XREAL_1:9;
A11: s2 is summable by Th26,SERIES_1:12;
for n be Nat holds 0 <= s1.n & s1.n <= s2.n
proof
let n be Nat;
A12: s1.n = f.(n + 2) by NAT_1:def 3;
f.(n+2) <= ((c-1)(#)(powerfact b)).(n+2)
by Th34,A0,ZFMISC_1:7,CARD_1:50; then
f.(n+2) <= (c-1)*((powerfact b).(n+2)) by VALUED_1:6;
hence thesis by Th33,A2,A12,NAT_1:def 3;
end; then
A13: Sum s1 <= Sum s2 by SERIES_1:20,A11;
A14: Sum f = (Partial_Sums f).1 + Sum (f^\(1+1)) by A3,SERIES_1:15
.= ((Partial_Sums f).0 + f.(0+1)) + Sum (f^\(1+1)) by SERIES_1:def 1
.= (f.0 + f.(0+1)) + Sum (f^\(1+1)) by SERIES_1:def 1
.= (0 + f.1) + Sum (f^\(1+1)) by DefLio
.= 1/10 + Sum (f^\ 2) by A5;
Sum s1 <= 10/(10-1) - 2/10 by A13,A10,XXREAL_0:2; then
1/10 + Sum (f ^\ 2) <= 1/10 + (10/(10 - 1) - 2/10) by XREAL_1:7;
hence thesis by A4,A5,A14,XXREAL_0:1;
end;
theorem Th40:
for nl be Liouville, z be Integer holds z + nl is liouville
proof
let nl be Liouville, z be Integer;
set zl = z + nl;
for n be non zero Nat ex p be Integer, q be Nat
st q > 1 & 0 < |. zl - p/q .| < 1/q|^n
proof
let n be non zero Nat;
nl is liouville; then
consider p1 be Integer, q1 be Nat such that
A1: q1 > 1 & 0 < |. nl - p1/q1 .| < 1/q1|^n;
set p2 = z * q1 + p1;
take p2, q2 = q1;
thus q2 > 1 by A1;
p2/q2 = (z * q1)/q1 + p1/q1 by XCMPLX_1:62
.= z + p1/q1 by A1,XCMPLX_1:89;
hence thesis by A1;
end;
hence thesis by Def2;
end;
registration let nl be Liouville, z be Integer;
cluster nl + z -> liouville;
coherence by Th40;
end;
definition
func LiouvilleNumbers -> Subset of REAL equals
the set of all nl where nl is Liouville;
coherence
proof
the set of all nl where nl is Liouville c= REAL
proof
let x be object;
assume x in the set of all nl where nl is Liouville; then
ex nl be Liouville st x = nl;
hence thesis by XREAL_0:def 1;
end;
hence thesis;
end;
end;
registration
cluster LiouvilleNumbers -> non empty;
coherence
proof
Liouville_constant in the set of all r where r is Liouville;
hence thesis;
end;
end;
registration
cluster LiouvilleNumbers -> infinite;
coherence
proof
deffunc F(Element of INT) = In ($1 + Liouville_constant,LiouvilleNumbers);
consider f be Function of INT, LiouvilleNumbers such that
A1: for i be Element of INT holds f.i = F(i) from FUNCT_2:sch 4;
A2: dom f = INT by FUNCT_2:def 1;
A3: rng f c= LiouvilleNumbers by RELAT_1:def 19;
for x1,x2 be object st x1 in INT & x2 in INT & f.x1 = f.x2 holds
x1 = x2
proof
let x1, x2 be object;
assume x1 in INT & x2 in INT; then
reconsider xx1 = x1, xx2 = x2 as Element of INT;
assume
A4: f.x1 = f.x2;
A5: xx1 + Liouville_constant in LiouvilleNumbers &
xx2 + Liouville_constant in LiouvilleNumbers;
A6: f.x1 = In (xx1 + Liouville_constant,LiouvilleNumbers) by A1
.= xx1 + Liouville_constant by A5,SUBSET_1:def 8;
f.x2 = In (xx2 + Liouville_constant,LiouvilleNumbers) by A1
.= xx2 + Liouville_constant by A5,SUBSET_1:def 8;
hence thesis by A4,A6;
end; then
f is one-to-one by FUNCT_2:19; then
omega c= card LiouvilleNumbers by TOPGEN_3:16,A2,A3,CARD_1:10;
hence thesis by FINSET_1:1;
end;
end;