:: 1. Define Liouville numbers
:: 2. Show that in the definition of Liouville numbers taken from Wikipedia
:: the quantification of n can be replaced from "every positive integer"
:: into "non-zero natural number".
:: 3. Prove auxiliary lemma that powers of two are unbounded, i.e.,
:: for any integer d, there exists a non-zero natural number
:: such that 2 to_power (n - 1) > d.
:: 4. Prove that no Liouville number can be rational (follow the proof
:: from Wikipedia).
environ
vocabularies CICM9,
NUMBERS, SUBSET_1, INT_1, SEQ_1, FINSEQ_1, RAT_1, ORDINAL4,
POWER, INT_2, SQUARE_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, NAT_1,
FUNCT_1, ARYTM_1, REALSET1, SEQ_2, ORDINAL2, COMPLEX1, VALUED_1,
SERIES_1, CARD_3, XBOOLE_0, RFINSEQ, PARTFUN1, FINSEQ_2, NEWTON, SIN_COS,
IRRAT_1, REAL_1, ASYMPT_1, XCMPLX_0, FUNCT_7, TARSKI, PREPOWER,
ABIAN, ORDINAL1, FUNCT_4, FUNCOP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, RELAT_1, REAL_1, INT_1, COMPLEX1, SQUARE_1,
FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_4, ABSVALUE, VALUED_0, VALUED_1,
FUNCT_2, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, PREPOWER,
POWER, FINSEQ_1, RVSUM_1,
SERIES_1, FINSEQ_2, RFINSEQ, SIN_COS, RAT_1, INT_2, PEPIN, NEWTON,
IRRAT_1, ABIAN, ASYMPT_1;
constructors ARYTM_0, REAL_1, NAT_1, NAT_D, SEQ_2, PARTFUN1, RVSUM_1,
ABSVALUE, IRRAT_1, FUNCT_1, ASYMPT_1, PREPOWER, ABIAN, FUNCT_4,
LIMFUNC1, COMSEQ_3, RFINSEQ, BINARITH, SIN_COS, PEPIN, SERIES_1, POWER,
RELSET_1, COMSEQ_2, SEQ_1, NUMBERS, FUNCOP_1, FUNCT_2;
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,
SQUARE_1, RVSUM_1, SEQ_1, SEQ_2, CARD_1, ABSVALUE, XCMPLX_0, FUNCT_1,
PREPOWER, NUMPOLY1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SEQ_1;
definitions TARSKI, XBOOLE_0, FINSEQ_1;
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,
RFINSEQ, FINSEQ_2, IRRAT_1, SEQ_4, ORDINAL1, SEQ_1, FINSEQ_1,
VALUED_1, XBOOLE_0, XREAL_0, FINSEQ_3;
schemes NAT_1, SEQ_1, IRRAT_1;
begin
:: HOLDER_1:3 revised
theorem HOLDER13:
for p be Real st 0 <= p :: originally: 0 < p
for a,b be Real st 0 <= a & a <= b holds
a to_power p <= b to_power p :: by HOLDER_1:3
proof
let p be Real such that
A1: 0 <= p;
let a, b be Real such that
A2: 0 <= a and
A3: a <= b;
per cases by A1;
suppose
S1: 0 = p;
a to_power 0 = 1 & b to_power 0 = 1 by POWER:24;
hence thesis by S1;
end;
suppose
S2: 0 < p;
per cases;
suppose a = b;
hence thesis;
end;
suppose
A4: a <> b;
A5: a < b by A3,A4,XXREAL_0:1;
now
per cases;
suppose
A6: a = 0;
then a to_power p = 0 by S2,POWER:def 2;
hence thesis by A3,A4,A6,POWER:34;
end;
suppose a <> 0;
hence thesis by A2,A5,S2,POWER:37;
end;
end;
hence thesis;
end;
end;
end;
begin :: Potentially useful MML theorems
theorem :: XREAL_1:72
for a,b,c being Real holds
0 <= c & b <= a implies b/c <= a/c by XREAL_1:72;
theorem :: XREAL_1:76
for a,b,c being Real holds
0 < c & 0 < a & a < b implies c/b < c/a by XREAL_1:76;
theorem :: XREAL_1:118
for a,b,c being Real holds
0 < a & 0 <= c & a <= b implies c/b <= c/a by XREAL_1:118;
theorem :: XXREAL_0:2
for a,b,c being Real holds
a <= b & b <= c implies a <= c by XXREAL_0:2;
theorem :: XXREAL_0:1
for a,b being Real holds a <= b & b <= a implies a = b by XXREAL_0:1;
theorem :: XREAL_1:11
for a,b,c being Real holds
a <= b-c implies c <= b-a by XREAL_1:11;
theorem :: XCMPLX_1:130
for a,b,c,d being Real holds
b <> 0 & d <> 0 implies a / b - c / d = (a * d - c * b) / (b * d)
by XCMPLX_1:130;
theorem :: XCMPLX_1:94
for a,b,c,d being Real holds
c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c
by XCMPLX_1:94;
theorem :: ABSVALUE:2
for x being Real holds
x = 0 iff |.x.| = 0 by ABSVALUE:2;
theorem :: COMPLEX1:67
for z1,z2 being Real holds
|.z1.| / |.z2.| = |.z1/z2.| by COMPLEX1:67;
:: Integer numbers
theorem :: INT_1:3
for i0 being Integer holds
0 <= i0 implies i0 in NAT by INT_1:3;
theorem :: NAT_1:13
for i,j being Nat holds i < j + 1 iff i <= j by NAT_1:13;
theorem :: INT_1:7
for i0, i1 being Integer holds
i0 < i1 implies i0 + 1 <= i1 by INT_1:7;
theorem :: NAT_1:14
for i being Nat holds i < 1 implies i = 0 by NAT_1:14;
:: Power and logarithm function
theorem :: NEWTON:4
for z being Real holds z |^ 0 = 1 by NEWTON:4;
theorem :: POWER:24
for a being Real holds a to_power 0 = 1 by POWER:24;
theorem :: POWER:34
for a, b being Real holds
a > 0 implies a to_power b > 0 by POWER:34;
theorem :: ENTROPY1:4
for a,b being Real holds
a>1 & b>1 implies log(a,b) > 0 by ENTROPY1:4;
theorem :: POWER:27
for a,b,c being Real holds
a > 0 implies a to_power (b+c) = a to_power b * a to_power c
by POWER:27;
theorem
for a,b being Real st a>0 & a<>1 & b>0 holds
a to_power log(a,b) = b by POWER:def 3;
:: Ceiling function
theorem
for r being Real holds
r <= [/ r \] & [/ r \] < r + 1 by INT_1:def 7;
theorem :: INT_1:32
for r being Real holds
r - 1 < [/ r \] & r < [/ r \] + 1 by INT_1:32;
:: Rational numbers
theorem
for r being object holds
r is rational iff r in RAT by RAT_1:def 2;
theorem :: RAT_1:8
for p being Rational
ex m being Integer, k being Nat st k<>0 & p=m/k by RAT_1:8;
begin :: Liouville numbers
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;
::: Exercise 1: In the definition above the quantification of n
::: can be over non-zero natural numbers
theorem LiouvilleEquivalent:
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;
:: Exercise 2: Lemma: Powers of 2 are unbounded
theorem Lemma1:
for d being Integer holds
ex n being non zero Nat st 2 to_power (n - 1) > d
proof
let d be Integer;
per cases;
suppose
C1: d <= 0;
take n = 1;
2 to_power (n - 1) = 2 to_power 0 .= 1 by POWER:24;
hence thesis by C1;
end;
suppose
C0: d > 0; then
d >= 1 + 0 by INT_1:7; then
d = 1 or d > 1 by XXREAL_0:1; then
per cases;
suppose
C1: d = 1;
take n = 2;
2 to_power (n - 1) = 2 to_power 1
.= 2;
hence thesis by C1;
end;
suppose
d > 1; then
B1: log (2,d) > 0 by ENTROPY1:4; then
[/ log (2,d) \] >= log (2,d) by INT_1:def 7; then
B2: [/ log (2,d) \] > 0 by B1;
set n = [/ log (2,d) \] + 2;
AA: n > 0 by B2; then
n in NAT by INT_1:3; then
reconsider n as non zero Nat by AA;
take n;
A2: 2 > 0 & d > 0 by C0;
n - 1 = [/ log (2,d) \] + 1; then
n - 1 > log (2,d) by INT_1:32; then
A3: 2 to_power (n - 1) > 2 to_power (log (2,d)) by POWER:39;
2 to_power (log (2,d)) = d by A2,POWER:def 3;
hence thesis by A3;
end;
end;
end;
::: Exercise 3: Show that all Liouville numbers are irrational
registration
cluster liouville -> irrational for Real;
coherence
proof
let x be Real;
assume
A0: x is liouville;
assume x is rational; then
x in RAT by RAT_1:def 2; then
consider c being Integer, d being Nat such that
A1: d <> 0 & x = c / d by RAT_1:8;
consider n being non zero Nat such that
ST: 2 to_power (n - 1) > d by Lemma1;
consider p being Integer, q being Nat such that
B1: q > 1 & 0 < |. x - p / q .| < 1 / (q |^ n) by A0;
T1: q <> 0 by B1;
T2: d <> 0 by A1;
SS: |. c/d - p/q .| = |. (c * q - p * d) / (d * q) .| by XCMPLX_1:130,T1,T2
.= |. (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 * d = c * q; then
T3: p / q = c / d by XCMPLX_1:94,T1,T2;
|. x - p/q .| = |. c/d - p/q .| by A1
.= 0 by T3;
hence thesis by B1;
end; then
|. c * q - p * d .| <> 0 by ABSVALUE:2; then
|. c * q - p * d .| >= 1 by NAT_1:14; then
|. c * q - p * d .| / (d * q) >= 1 / (d * q) by XREAL_1:72; then
HR: |. x - p / q .| >= 1 / (d * q) by SS,A1;
d * q <> 0 by T1,T2;
QW: d * q > 0 by T2,B1;
q > 0 by B1; then
d * q < (2 to_power (n - 1)) * q by ST,XREAL_1:68; then
1 / (d * q) > 1 / ((2 to_power (n - 1)) * q) by XREAL_1:76,QW; 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,HOLDER13; then
(2 to_power (n - 1)) * q <= (q to_power (n - 1)) * q
by XREAL_1:66,FG; then
(2 to_power (n - 1)) * q <= (q to_power (n - 1)) * (q to_power 1); then
(2 to_power (n - 1)) * q <= (q to_power (n - 1 + 1))
by B1,POWER:27; then
(2 to_power (n - 1)) * q <= q to_power n; then
QA: (2 to_power (n - 1)) * q <= q |^ n;
2 to_power (n - 1) > 0 by POWER:34; then
(2 to_power (n - 1)) * q > 0 by B1; then
1 / ((2 to_power (n-1)) * q) >= 1 / (q |^ n) by XREAL_1:118,QA; then
|. x - p / q .| >= 1 / (q |^ n) by XXREAL_0:2,HG;
hence thesis by B1;
end;
end;
definition let a be Nat;
func Liouville_seq a -> Real_Sequence means
it.0 = 0 &
for n being non zero Nat holds
it.n = a to_power (-n!);
:: The same can be obtained with the more general definition
existence
proof
deffunc G(Nat,Element of REAL) = In (a to_power (-($1+1)!),REAL);
deffunc A() = In(0,REAL);
consider f being sequence of REAL such that
A1: f.0 = A() &
for n being 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 being Nat such that
A2: k + 1 = n by NAT_1:6;
f.(k+1) = In(a to_power (-(k + 1)!), REAL) by A1
.= a 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 being non zero Nat holds f1.n = a to_power (-n!) and
A2: f2.0 = 0 &
for n being non zero Nat holds f2.n = a to_power (-n!);
for n being 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 to_power (-n!) by A1
.= f2.n by A2,A3;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition let a be Nat;
func Liouville_constant a -> Real equals
Sum Liouville_seq a;
coherence;
end;
registration let a be non zero Nat;
cluster Liouville_constant a -> liouville;
coherence;
::> *4
end;
registration
cluster liouville for Real;
existence
proof
take Liouville_constant 1;
thus thesis;
end;
end;
definition
mode Liouville is liouville Real;
end;
1 is not Liouville;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin :: Other stuff, not really needed
definition let b be Nat;
func BLiouville_seq b -> Real_Sequence means :LiuSeq:
for n being Nat holds
it.n = b to_power (n!);
correctness
proof
deffunc F(Nat) = b to_power ($1!);
thus (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;
end;
end;
registration let b be Nat;
cluster BLiouville_seq b -> NAT-valued;
coherence
proof
set f = BLiouville_seq b;
rng f c= NAT
proof let x be object;
assume x in rng f; then
consider n being object such that
AB: n in dom f & x = f.n by FUNCT_1:def 3;
reconsider n as Nat by AB;
AA: b to_power (n!) in INT by INT_1:def 2;
f.n = b to_power (n!) by LiuSeq;
hence thesis by AB;
end;
hence thesis by RELAT_1:def 19;
end;
end;
registration
cluster NAT-valued for Real_Sequence;
existence
proof
take BLiouville_seq 1;
thus thesis;
end;
end;
definition let a be Real_Sequence;
let b be Nat;
:: assume b >= 2;
func Liouville_seq (a,b) -> Real_Sequence means :DefLio:
it.0 = 0 &
for k being 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 being sequence of REAL such that
A1: f.0 = A() &
for n being 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 being Nat such that
A2: k + 1 = n by NAT_1:6;
f.(k+1) = G(k,f.k) by A1
.= In((a.(k+1)) / (b to_power ((k + 1)!)), REAL)
.= (a.(k + 1)) / (b to_power ((k + 1)!)); then
f.n = (a.n) / (b to_power (n!)) by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Real_Sequence;
assume that
A1: f1.0 = 0 &
for n being non zero Nat holds f1.n = (a.n) / (b to_power (n!)) and
A2: f2.0 = 0 &
for n being non zero Nat holds f2.n = (a.n) / (b to_power (n!));
for n being 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;
definition let a be Real_Sequence;
let b be Nat;
func Liouville_constant (a,b) -> Real equals
Sum Liouville_seq (a,b);
coherence;
end;
registration let a be NAT-valued Real_Sequence;
let b be non zero Nat;
cluster Liouville_constant (a,b) -> liouville;
coherence;
::> *4
end;
theorem
for n being 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;
registration let a be Integer;
let 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
-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;
theorem SomeLemma:
for b being Nat st b > 1 holds
|. 1 / b .| < 1
proof
let b be Nat;
assume
A0: b > 1; then
A1: b > 0;
A2: 1 / b < 1 / 1 by A0,XREAL_1:76;
|. 1 / b .| < 1 by A2;
hence thesis;
end;
theorem
for b being Nat st b > 1 holds
Sum ((1/b) GeoSeq) = b / (b - 1)
proof
let b be Nat;
assume
A0: b > 1; then
A2: b > 0;
A1: |. 1 / b .| < 1 by SomeLemma,A0; then
(1 / b) GeoSeq is summable by SERIES_1:24;
Sum ((1/b) GeoSeq) = 1 / (1 - (1 / b)) by A1,SERIES_1:24
.= 1 / ((b / b) - (1 / b)) by XCMPLX_1:60,A2
.= 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
proof
n in NAT by ORDINAL1:def 12; then
seq_const n is Function of NAT, NAT by FUNCOP_1:46; then
rng seq_const n c= NAT by RELAT_1:def 19;
hence thesis by RELAT_1:def 19;
end;
end;
registration
cluster INT-valued for Real_Sequence;
existence
proof
take f = seq_const 0;
thus thesis;
end;
end;
::>
::> 4: This inference is not accepted