:: Sequences of Prime Reciprocals -- Preliminaries
:: by Adam Grabowski
::
:: Received March 27, 2018
:: Copyright (c) 2018 Association of Mizar Users

registration
cluster non trivial V21() V22() V23() V27() non zero complex V32() integer dim-like ext-real non negative square for Nat;
existence
ex b1 being Nat st
( not b1 is zero & b1 is square & not b1 is trivial )
proof end;
end;

registration
let Z be Subset of REAL;
let f be PartFunc of Z,REAL;
let A be Subset of REAL;
cluster K5(f,A) -> A -defined for PartFunc of Z,REAL;
coherence
for b1 being PartFunc of Z,REAL st b1 = f | A holds
b1 is A -defined
;
end;

theorem :: MOEBIUS3:1
for Z being Subset of REAL st 0 in Z holds
(id Z) " =
proof end;

theorem Counter0: :: MOEBIUS3:2
for Z being Subset of REAL st not 0 in Z holds
(id Z) " = {}
proof end;

theorem ContCut: :: MOEBIUS3:3
for Z being open Subset of REAL
for A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds
((id Z) ^) | A is continuous
proof end;

theorem :: MOEBIUS3:4
for n being Nat
for Z being open Subset of REAL
for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & A = [.1,(n + 1).] holds
integral (((id Z) ^),A) = ln . (n + 1)
proof end;

theorem :: MOEBIUS3:5
for n being Nat
for Z being open Subset of REAL
for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & 0 < n & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) = ln . ((n + 1) / n)
proof end;

theorem MacPositive: :: MOEBIUS3:6
for x, r being Real st x > 0 & r > 0 holds
Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding
proof end;

theorem Th36: :: MOEBIUS3:7
for f being summable Real_Sequence
for n being Nat st f is positive-yielding holds
Sum (f ^\ (n + 1)) > 0
proof end;

:: n-th harmonic number
definition
let n be Nat;
func Harmonic n -> Real equals :: MOEBIUS3:def 1
. n;
coherence
. n is Real
;
end;

:: deftheorem defines Harmonic MOEBIUS3:def 1 :
for n being Nat holds Harmonic n = . n;

theorem Harm0: :: MOEBIUS3:8
proof end;

theorem Harmon1: :: MOEBIUS3:9
for n being Nat holds Harmonic (n + 1) = () + (1 / (n + 1))
proof end;

theorem Harm1: :: MOEBIUS3:10
proof end;

theorem :: MOEBIUS3:11
Harmonic 2 = 3 / 2
proof end;

theorem LogZero: :: MOEBIUS3:12
proof end;

theorem :: MOEBIUS3:13
for x being Real st x > 0 holds
exp_R . x > x + 1
proof end;

theorem Diesel1: :: MOEBIUS3:14
for x being Real st x > 0 holds
ln . (x + 1) < x
proof end;

theorem Diesel2: :: MOEBIUS3:15
for n being Nat st n > 0 holds
ln . ((n + 1) / n) < 1 / n
proof end;

theorem LogExp: :: MOEBIUS3:16
for x being Real holds ln . () = x
proof end;

theorem LogMono: :: MOEBIUS3:17
for x, y being Real st 0 < x & x < y holds
ln . x < ln . y
proof end;

theorem :: MOEBIUS3:18
for n being non zero Nat holds ln . (n + 1) > 0
proof end;

theorem LogAdd: :: MOEBIUS3:19
for x, y being Real st 0 < x & 0 < y holds
ln . (x * y) = (ln . x) + (ln . y)
proof end;

theorem :: MOEBIUS3:20
for x being Real ex y being non zero Nat st x < ln . (ln . (y + 1))
proof end;

theorem Diesel3: :: MOEBIUS3:21
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) < 1 / n
proof end;

theorem :: MOEBIUS3:22
for n being non zero Nat holds ln . (n + 1) < Harmonic n
proof end;

theorem :: MOEBIUS3:23
for n1, n2 being Nat st n1 ^2 = n2 ^2 holds
n1 = n2
proof end;

registration
let n be non trivial Nat;
cluster K650(n) -> non trivial ;
coherence
not n ^2 is trivial
proof end;
end;

:: Telescoping series
theorem Telescoping: :: MOEBIUS3:24
for a, b, s being Real_Sequence st ( for n being Nat holds s . n = (a . n) + (b . n) ) & ( for k being Nat holds b . k = - (a . (k + 1)) ) holds
for n being Nat holds () . n = (a . 0) + (b . n)
proof end;

theorem Impor3: :: MOEBIUS3:25
for f1, f2 being Real_Sequence
for n being non trivial Nat st ( for k being non trivial Nat st k <= n holds
f1 . k < f2 . k ) holds
Sum (f1,n,1) < Sum (f2,n,1)
proof end;

definition
func Reci-seq1 -> Real_Sequence means :MyDef: :: MOEBIUS3:def 2
for n being Nat holds it . n = 1 / ((n ^2) - (1 / 4));
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = 1 / ((n ^2) - (1 / 4))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = 1 / ((n ^2) - (1 / 4)) ) & ( for n being Nat holds b2 . n = 1 / ((n ^2) - (1 / 4)) ) holds
b1 = b2
proof end;
end;

:: deftheorem MyDef defines Reci-seq1 MOEBIUS3:def 2 :
for b1 being Real_Sequence holds
( b1 = Reci-seq1 iff for n being Nat holds b1 . n = 1 / ((n ^2) - (1 / 4)) );

theorem Tele1: :: MOEBIUS3:26
for n being Nat holds Reci-seq1 . n = (1 / (n - (1 / 2))) - (1 / (n + (1 / 2)))
proof end;

AlgDef: for n being Nat
for a, b being Real holds (rseq (0,1,a,b)) . n = 1 / ((a * n) + b)

proof end;

Tele2: for n being Nat holds Reci-seq1 . n = ((rseq (0,1,1,(- (1 / 2)))) . n) + ((- (rseq (0,1,1,(1 / 2)))) . n)
proof end;

theorem :: MOEBIUS3:27
Reci-seq1 = (rseq (0,1,1,(- (1 / 2)))) + (- (rseq (0,1,1,(1 / 2)))) by ;

theorem :: MOEBIUS3:28
for n being Nat holds . n < - 2
proof end;

theorem Seq3: :: MOEBIUS3:29
for n being Nat holds Sum (Reci-seq1,n,1) < 2 / 3
proof end;

registration
coherence
proof end;
end;

theorem :: MOEBIUS3:30
for n being Nat holds . n = (- 2) + (- (1 / (n + (1 / 2))))
proof end;

theorem Impor2: :: MOEBIUS3:31
for n being non trivial Nat holds Sum (Basel-seq,n,1) < Sum (Reci-seq1,n,1)
proof end;

theorem Important: :: MOEBIUS3:32
for n being non trivial Nat holds Sum (Basel-seq,n) < 5 / 3
proof end;

theorem :: MOEBIUS3:33
for n being Nat holds . n < 5 / 3
proof end;

definition
func Reci-seq2 -> Real_Sequence means :My3Def: :: MOEBIUS3:def 3
for n being Nat holds it . n = 1 + (1 / ());
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = 1 + (1 / ())
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = 1 + (1 / ()) ) & ( for n being Nat holds b2 . n = 1 + (1 / ()) ) holds
b1 = b2
proof end;
end;

:: deftheorem My3Def defines Reci-seq2 MOEBIUS3:def 3 :
for b1 being Real_Sequence holds
( b1 = Reci-seq2 iff for n being Nat holds b1 . n = 1 + (1 / ()) );

theorem :: MOEBIUS3:34
Sum () = 1
proof end;

definition
let n be Nat;
func SetPrimes n -> Subset of NAT equals :: MOEBIUS3:def 4
SetPrimes /\ (Seg n);
coherence
SetPrimes /\ (Seg n) is Subset of NAT
;
end;

:: deftheorem defines SetPrimes MOEBIUS3:def 4 :
for n being Nat holds SetPrimes n = SetPrimes /\ (Seg n);

registration
let n be Nat;
coherence ;
end;

theorem :: MOEBIUS3:35
for m, n being Nat st m <= n holds
SetPrimes m c= SetPrimes n by ;

theorem PrimesSet: :: MOEBIUS3:36
for n being Nat st n + 1 is not Prime holds
SetPrimes (n + 1) = SetPrimes n
proof end;

theorem SetPrime1: :: MOEBIUS3:37
proof end;

theorem PrimesSet2: :: MOEBIUS3:38
for n being Nat st n + 1 is Prime holds
SetPrimes (n + 1) = () \/ {(n + 1)}
proof end;

theorem P1NotPrime: :: MOEBIUS3:39
for p being Prime st p > 2 holds
not p + 1 is Prime
proof end;

theorem Set2: :: MOEBIUS3:40
proof end;

theorem :: MOEBIUS3:41
for n being Nat holds not n + 1 in SetPrimes n
proof end;

definition
let n be Nat;
:: just to get an index for appropriate sequence of primes
func indexp n -> Nat equals :: MOEBIUS3:def 5
card ();
coherence
card () is Nat
;
end;

:: deftheorem defines indexp MOEBIUS3:def 5 :
for n being Nat holds indexp n = card ();

theorem Krzys1: :: MOEBIUS3:42
for n being Nat holds indexp n <= n
proof end;

theorem :: MOEBIUS3:43
for n being non zero Nat holds n = (TSqF n) * (n div (TSqF n))
proof end;

theorem Skup: :: MOEBIUS3:44
for n being non zero Nat holds (SqF n) |^ 2 divides n
proof end;

theorem KeyValue: :: MOEBIUS3:45
for m being natural-valued finite-support ManySortedSet of SetPrimes
for p being Prime st support m = {p} holds
Product m = m . p
proof end;

theorem Cosik: :: MOEBIUS3:46
for n being non zero Nat holds (SqF n) |^ 2 = TSqF n
proof end;

registration
let n be non zero Nat;
cluster K184(n,((SqF n) |^ 2)) -> square-free for Nat;
coherence
for b1 being Nat st b1 = n div ((SqF n) |^ 2) holds
not b1 is square-containing
proof end;
end;

::: TSqF n should be revised to allow zero for an argument
definition
let n be non zero Nat;
func SquarefreePart n -> non zero Nat equals :: MOEBIUS3:def 6
n div (TSqF n);
coherence
n div (TSqF n) is non zero Nat
proof end;
end;

:: deftheorem defines SquarefreePart MOEBIUS3:def 6 :
for n being non zero Nat holds SquarefreePart n = n div (TSqF n);

registration
let n be non zero Nat;
coherence ;
end;

theorem Canonical: :: MOEBIUS3:47
for n being non zero Nat holds n = () * ((SqF n) ^2)
proof end;

theorem :: MOEBIUS3:48
for n being non zero Nat holds support () c= Seg n
proof end;

theorem :: MOEBIUS3:49
for n being non zero Nat holds support (ppf n) c= Seg n
proof end;

theorem :: MOEBIUS3:50
for n being non zero Nat holds Seg () c= Seg n
proof end;

Surprise: for n, m being non zero Nat st m ^2 divides SquarefreePart n holds
m = 1

proof end;

theorem :: MOEBIUS3:51
for k, n being non zero Nat holds
( k ^2 divides SquarefreePart n iff k = 1 ) by ;

theorem :: MOEBIUS3:52
for m, n being non zero Nat st SquarefreePart n = SquarefreePart m & TSqF m = TSqF n holds
m = n
proof end;

definition
let A be finite Subset of SetPrimes;
func A -bag -> bag of SetPrimes equals :: MOEBIUS3:def 7
+* (id A);
coherence
+* (id A) is bag of SetPrimes
proof end;
end;

:: deftheorem defines -bag MOEBIUS3:def 7 :
for A being finite Subset of SetPrimes holds A -bag = +* (id A);

theorem BagSupport: :: MOEBIUS3:53
for A being finite Subset of SetPrimes holds support (A -bag) = A
proof end;

theorem :: MOEBIUS3:54
for A being finite Subset of SetPrimes st A = {} holds
A -bag = EmptyBag SetPrimes
proof end;

theorem BagValue: :: MOEBIUS3:55
for A being finite Subset of SetPrimes
for i being object st i in support (A -bag) holds
(A -bag) . i = i
proof end;

theorem :: MOEBIUS3:56
for A, B being finite Subset of SetPrimes st A -bag = B -bag holds
A = B
proof end;

registration
let A be finite Subset of SetPrimes;
coherence
proof end;
end;

ProdSqF: for A being finite Subset of SetPrimes holds Product (A -bag) is square-free
proof end;

registration
let A be finite Subset of SetPrimes;
cluster K663(SetPrimes,(A -bag)) -> square-free for Nat;
coherence
for b1 being Nat st b1 = Product (A -bag) holds
not b1 is square-containing
by ProdSqF;
end;

theorem :: MOEBIUS3:57
for n being non zero Nat
for x being object st x in bool () holds
x is finite Subset of SetPrimes
proof end;

theorem :: MOEBIUS3:58
for n being non zero Nat
for x being object st x in [:(bool ()),(Seg n):] holds
x `1 is finite Subset of SetPrimes
proof end;

:: Later we should show the connection between sum and products of
:: sequences with exponential function, respectively.
theorem :: MOEBIUS3:59
rseq (0,1,1,0) = invNAT
proof end;

theorem :: MOEBIUS3:60

theorem GreaterProduct: :: MOEBIUS3:61
for n being Nat holds . n > 0
proof end;

theorem Crucial5X: :: MOEBIUS3:62
for n being Nat holds ln . () <= . n
proof end;

theorem :: MOEBIUS3:63
for n being Nat holds ln . () <= . n
proof end;

definition
func Reci-Sqf -> Real_Sequence means :MySumDef: :: MOEBIUS3:def 8
( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / () ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / () ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / () ) & b2 . 0 = 0 & ( for i being non zero Nat holds b2 . i = 1 / () ) holds
b1 = b2
proof end;
func Reci-TSq -> Real_Sequence means :MySum2Def: :: MOEBIUS3:def 9
( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / (TSqF i) ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / (TSqF i) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / (TSqF i) ) & b2 . 0 = 0 & ( for i being non zero Nat holds b2 . i = 1 / (TSqF i) ) holds
b1 = b2
proof end;
end;

:: deftheorem MySumDef defines Reci-Sqf MOEBIUS3:def 8 :
for b1 being Real_Sequence holds
( b1 = Reci-Sqf iff ( b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / () ) ) );

:: deftheorem MySum2Def defines Reci-TSq MOEBIUS3:def 9 :
for b1 being Real_Sequence holds
( b1 = Reci-TSq iff ( b1 . 0 = 0 & ( for i being non zero Nat holds b1 . i = 1 / (TSqF i) ) ) );

theorem Core1: :: MOEBIUS3:64
rseq (0,1,1,0) = Reci-Sqf (#) Reci-TSq
proof end;

theorem Seqs1: :: MOEBIUS3:65
for n being Nat holds Reci-Sqf . n >= 0
proof end;

theorem Seqs4: :: MOEBIUS3:66
for n being Nat holds Reci-TSq . n >= 0
proof end;

theorem :: MOEBIUS3:67
for n being Nat holds Basel-seq . n >= 0
proof end;

theorem :: MOEBIUS3:68
for n being Nat holds (Partial_Sums (rseq (0,1,1,0))) . n <= () * () by ;

definition
let n be non zero Nat;
func Compose n -> Function of [:(bool ()),(Seg n):],NAT means :: MOEBIUS3:def 10
for x being Element of [:(bool ()),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
it . x = (Product ((A,1) -bag)) * (k ^2);
existence
ex b1 being Function of [:(bool ()),(Seg n):],NAT st
for x being Element of [:(bool ()),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b1 . x = (Product ((A,1) -bag)) * (k ^2)
proof end;
uniqueness
for b1, b2 being Function of [:(bool ()),(Seg n):],NAT st ( for x being Element of [:(bool ()),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b1 . x = (Product ((A,1) -bag)) * (k ^2) ) & ( for x being Element of [:(bool ()),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b2 . x = (Product ((A,1) -bag)) * (k ^2) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Compose MOEBIUS3:def 10 :
for n being non zero Nat
for b2 being Function of [:(bool ()),(Seg n):],NAT holds
( b2 = Compose n iff for x being Element of [:(bool ()),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b2 . x = (Product ((A,1) -bag)) * (k ^2) );

theorem :: MOEBIUS3:69
for n being Nat holds . n >= 0
proof end;

definition
let n be Nat;
func ReciProducts n -> Subset of REAL equals :: MOEBIUS3:def 11
{ (1 / (Product (Sgm X))) where X is Subset of () : verum } ;
coherence
{ (1 / (Product (Sgm X))) where X is Subset of () : verum } is Subset of REAL
proof end;
end;

:: deftheorem defines ReciProducts MOEBIUS3:def 11 :
for n being Nat holds ReciProducts n = { (1 / (Product (Sgm X))) where X is Subset of () : verum } ;

registration
let n be Nat;
correctness
coherence ;
proof end;
end;

theorem :: MOEBIUS3:70
proof end;

theorem :: MOEBIUS3:71
for p being Prime st p > 2 holds
ReciProducts (p + 1) = ReciProducts p
proof end;

theorem :: MOEBIUS3:72
for p being Nat st p + 1 is not Prime holds
ReciProducts (p + 1) = ReciProducts p
proof end;

theorem :: MOEBIUS3:73
proof end;

theorem :: MOEBIUS3:74
ReciProducts 2 = {(1 / 2),1}
proof end;

theorem ReciSubset: :: MOEBIUS3:75
for n being Nat holds ReciProducts n c= ReciProducts (n + 1)
proof end;

theorem :: MOEBIUS3:76
for n being Nat st n + 1 is Prime holds
ReciProducts (n + 1) = () \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }
proof end;

theorem :: MOEBIUS3:77
for n being Nat st n + 1 is Prime holds
ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of () : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }
proof end;