:: 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;
::> *4
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);
::> *4
take p,q;
thus 1 < q & 0 < |. r-p/q .|;
::> *4,4
hence thesis;
::> *4
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;
thus thesis;
::> *4
end;
suppose
C0: d > 0;
set n = [/ log (2,d) \] + 2;
reconsider n as non zero Nat;
::> *4,4
take n;
thus thesis;
::> *4
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;
:: Otherwise you can take appropriate constant
thus thesis;
::> *1
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;
uniqueness;
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;
::>
::> 1: It is not true
::> 4: This inference is not accepted