:: Introduction to {L}iouville Numbers
::  by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 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;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

theorem :: LIOUVIL1:1
  for x, y be Nat st x > 1 & y > 1 holds x*y >= x+y;

theorem :: LIOUVIL1:2
  for n be Nat holds n <= n!;

theorem :: LIOUVIL1:3
  for n be Nat holds n * (n!) = (n + 1)! - n!;

theorem :: LIOUVIL1:4
  for n be Nat st n >= 1 holds 2 <= (n + 1)!;

theorem :: LIOUVIL1:5
  for n,i be Nat st n >= 1 & i >= 1 holds (n + i)! >= n! + i;

theorem :: LIOUVIL1:6
  for n,i being Nat st n >= 2 & i >= 1 holds (n+i)! > n! + i;

theorem :: LIOUVIL1:7
  for b be Nat st b > 1 holds |. 1/b .| < 1;

theorem :: LIOUVIL1:8
  for d be Integer holds ex n be non zero Nat st 2 to_power (n-1) > d;

registration
  let a be Integer, b be Nat;
  cluster a to_power b -> integer;
end;

begin :: Sequences

theorem :: LIOUVIL1:9
  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);

theorem :: LIOUVIL1:10
  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;

theorem :: LIOUVIL1:11
  for b be Nat st b > 1 holds Sum ((1/b) GeoSeq) = b/(b-1);

registration let n be Nat;
  cluster seq_const n -> NAT-valued;
end;

registration let r be positive Nat;
  cluster seq_const r -> positive-yielding;
end;

registration
  cluster NAT-valued INT-valued for Real_Sequence;
end;

theorem :: LIOUVIL1:12
  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);

theorem :: LIOUVIL1:13
  for n be Nat,a be Real holds (Partial_Sums seq_const a).n = a * (n + 1);

registration let f be INT-valued Real_Sequence;
  cluster Partial_Sums f -> INT-valued;
end;

registration
  let f be NAT-valued Real_Sequence;
  cluster Partial_Sums f -> NAT-valued;
end;

theorem :: LIOUVIL1:14
  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;

theorem :: LIOUVIL1:15
  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;

registration
  let f be nonnegative-yielding Real_Sequence;
  let n be Nat;
  cluster f ^\ n -> nonnegative-yielding;
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
:: LIOUVIL1:def 1
    (NAT --> 0) +* (f | X);
end;

registration let f be Real_Sequence, X be Subset of NAT;
  cluster f | X -> NAT-defined;
end;

registration let f be Real_Sequence, n be Nat;
  cluster f |_ Seg n -> summable;
end;

registration let f be INT-valued Real_Sequence, n be Nat;
  cluster f |_ Seg n -> INT-valued;
end;

theorem :: LIOUVIL1:16
  for f be Real_Sequence holds f |_ Seg 0 = seq_const 0;

definition let f be Real_Sequence, n be Nat;
  func FinSeq (f,n) -> FinSequence of REAL equals
:: LIOUVIL1:def 2
  f | Seg n;
end;

theorem :: LIOUVIL1:17
  for f be Real_Sequence,k,n be Nat st k in Seg n holds (f |_ Seg n).k = f.k;

theorem :: LIOUVIL1:18
  for f be Real_Sequence, n be Nat st f.0 = 0 holds
  Sum FinSeq (f,n) = Sum (f |_ Seg n);

theorem :: LIOUVIL1:19
  for f be Real_Sequence, n be Nat holds dom FinSeq (f,n) = Seg n;

theorem :: LIOUVIL1:20
  for f be Real_Sequence,i be Nat holds
  (FinSeq(f,i))^<* f.(i+1) *> = FinSeq(f,i+1);

theorem :: LIOUVIL1:21
  for f be Real_Sequence,n be Nat st f.0 = 0
  holds Sum FinSeq (f,n) = (Partial_Sums f).n;

theorem :: LIOUVIL1:22
  for f be Real_Sequence, n be Nat st f.0 = 0 holds
  Sum (f |_ Seg n) = (Partial_Sums f).n;

theorem :: LIOUVIL1:23
  for f be INT-valued Real_Sequence, n be Nat st f.0 = 0 holds
  Sum (f |_ Seg n) is Integer;

theorem :: LIOUVIL1:24
  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));

:: |_ is the same as SETWOP_2:def 1, p is FinSequence

registration
  cluster positive-yielding NAT-valued for Real_Sequence;
end;

begin :: Sequences not Vanishing at Infinity

definition
  let f be Real_Sequence;
  attr f is eventually-non-zero means
:: LIOUVIL1:def 3
  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;
end;

registration
  cluster seq_id id NAT -> eventually-nonzero;
end;

registration
  cluster eventually-non-zero for Real_Sequence;
end;

theorem :: LIOUVIL1:25
  for f be eventually-non-zero Real_Sequence holds
  for n be Nat holds f ^\ n is eventually-non-zero;

registration let f be eventually-non-zero Real_Sequence, n be Nat;
  cluster f ^\ n -> eventually-non-zero for Real_Sequence;
end;

registration
  cluster non-zero constant -> eventually-non-zero for Real_Sequence;
end;

definition let b be Nat;
  func powerfact b -> Real_Sequence means
:: LIOUVIL1:def 4
    for i be Nat holds it.i = 1/(b to_power (i!));
end;

theorem :: LIOUVIL1:26
  for b,i be Nat st b >= 1 holds (powerfact b).i <= ((1/b) GeoSeq).i;

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

registration let b be non trivial Nat;
  cluster powerfact b -> summable;
end;

registration
  cluster nonnegative-yielding for Real_Sequence;
end;

theorem :: LIOUVIL1:28
  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);

begin :: Liouville Numbers

::$N Liouville number

definition let x be Real;
  attr x is liouville means
:: LIOUVIL1:def 5
    for n being Nat
     ex p being Integer,
        q being Nat st q > 1 &
       0 < |. x - p / q .| < 1 / (q |^ n);
end;

theorem :: LIOUVIL1:29
  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);

definition let a be Real_Sequence, b be Nat;
  func Liouville_seq (a,b) -> Real_Sequence means
:: LIOUVIL1:def 6
  it.0 = 0 &
  for k be non zero Nat holds it.k = (a.k)/(b to_power(k!));
end;

::$N Liouville number!irrationality

registration
  cluster liouville -> irrational for Real;
end;

begin :: Liouville Constant

::$N Liouville's constant

definition let a be Real_Sequence,b be Nat;
  func Liouville_constant (a,b) -> Real equals
:: LIOUVIL1:def 7
  Sum Liouville_seq (a,b);
end;

definition let b be Nat;
  func BLiouville_seq b -> Real_Sequence means
:: LIOUVIL1:def 8
  for n be Nat holds it.n = b to_power (n!);
end;

registration let b be Nat;
  cluster BLiouville_seq b -> NAT-valued;
end;

definition let a be Real_Sequence, b be Nat;
  func ALiouville_seq (a,b) -> Real_Sequence means
:: LIOUVIL1:def 9
  for n be Nat holds
  it.n = (BLiouville_seq b).n * Sum (Liouville_seq (a,b) |_ Seg n);
end;

theorem :: LIOUVIL1:30
  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;

theorem :: LIOUVIL1:31
  for a be NAT-valued Real_Sequence, b,n be Nat st b > 0 holds
  ALiouville_seq (a,b).n is Integer;

registration let a be NAT-valued Real_Sequence;
             let b be non zero Nat;
  cluster ALiouville_seq (a,b) -> INT-valued;
end;

theorem :: LIOUVIL1:32
  for n,b be non zero Nat st b > 1 holds (BLiouville_seq b).n > 1;

theorem :: LIOUVIL1:33
  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;

theorem :: LIOUVIL1:34
  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);

theorem :: LIOUVIL1:35
  for a be NAT-valued Real_Sequence, b be non trivial Nat,n be Nat
  holds Liouville_seq (a,b).n >= 0;

theorem :: LIOUVIL1:36
  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;

registration
  let a be NAT-valued Real_Sequence, b be non trivial Nat;
  cluster Liouville_seq (a,b) -> nonnegative-yielding;
end;

theorem :: LIOUVIL1:37
  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;

theorem :: LIOUVIL1:38
  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));

theorem :: LIOUVIL1:39
  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)));

theorem :: LIOUVIL1:40
  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;

theorem :: LIOUVIL1:41
  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;

definition
  func Liouville_constant -> Real equals
:: LIOUVIL1:def 10
  Liouville_constant (seq_const 1,10);
end;

theorem :: LIOUVIL1:42
  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;

registration
  cluster Liouville_constant -> liouville;
end;

registration
  cluster liouville for Real;
end;

definition
  mode Liouville is liouville Real;
end;

theorem :: LIOUVIL1:43
  for m,n be non zero Nat holds
  (Liouville_seq (seq_const 1, m)).n = m to_power - n!;

theorem :: LIOUVIL1:44
  for m being Nat st 1 < m holds
    Liouville_seq (seq_const 1, m) is negligible;

theorem :: LIOUVIL1:45
  1/10 < Liouville_constant <= 10/9 - 1/10;

theorem :: LIOUVIL1:46
  for nl be Liouville, z be Integer holds z + nl is liouville;

registration let nl be Liouville, z be Integer;
  cluster nl + z -> liouville;
end;

definition
  func LiouvilleNumbers -> Subset of REAL equals
:: LIOUVIL1:def 11
  the set of all nl where nl is Liouville;
end;

registration
  cluster LiouvilleNumbers -> non empty;
end;

registration
  cluster LiouvilleNumbers -> infinite;
end;