:: Sequences of Prime Reciprocals -- Preliminaries
:: by Adam Grabowski
::
:: Received March 27, 2018
:: Copyright (c) 2018-2021 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 set ;

existence
ex b₁ being Nat st
( not b₁ is zero & b₁ is square & not b₁ 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 f | A -> A -defined for PartFunc of Z,REAL;

coherence
for b₁ being PartFunc of Z,REAL st b₁ = f | A holds
b₁ is A -defined ;

end;

theorem :: MOEBIUS3:1

for Z being Subset of REAL st 0 in Z holds
(id Z) " {0} = {0}

proof end;

theorem Counter0: :: MOEBIUS3:2

for Z being Subset of REAL st not 0 in Z holds
(id Z) " {0} = {}

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
(Partial_Sums invNAT) . n;

coherence
(Partial_Sums invNAT) . n is Real ;

end;

:: deftheorem defines Harmonic MOEBIUS3:def 1 :
for n being Nat holds Harmonic n = (Partial_Sums invNAT) . n;

theorem Harm0: :: MOEBIUS3:8

Harmonic 0 = 0

proof end;

theorem Harmon1: :: MOEBIUS3:9

for n being Nat holds Harmonic (n + 1) = (Harmonic n) + (1 / (n + 1))

proof end;

theorem Harm1: :: MOEBIUS3:10

Harmonic 1 = 1

proof end;

theorem :: MOEBIUS3:11

Harmonic 2 = 3 / 2

proof end;

theorem LogZero: :: MOEBIUS3:12

ln . 1 = 0

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 . (exp_R . x) = 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 n ^2 -> 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 (Partial_Sums s) . 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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = 1 / ((n ^2) - (1 / 4))

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = 1 / ((n ^2) - (1 / 4)) ) & ( for n being Nat holds b₂ . n = 1 / ((n ^2) - (1 / 4)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem MyDef defines Reci-seq1 MOEBIUS3:def 2 :
for b₁ being Real_Sequence holds
( b₁ = Reci-seq1 iff for n being Nat holds b₁ . 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 SEQ_1:7, Tele2;

theorem :: MOEBIUS3:28

for n being Nat holds (Partial_Sums Reci-seq1) . n < - 2

proof end;

theorem Seq3: :: MOEBIUS3:29

for n being Nat holds Sum (Reci-seq1,n,1) < 2 / 3

proof end;

registration

cluster Basel-seq -> summable ;

coherence
Basel-seq is summable

proof end;

end;

theorem :: MOEBIUS3:30

for n being Nat holds (Partial_Sums Reci-seq1) . 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 (Partial_Sums Basel-seq) . 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 / (primenumber n));

existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = 1 + (1 / (primenumber n))

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = 1 + (1 / (primenumber n)) ) & ( for n being Nat holds b₂ . n = 1 + (1 / (primenumber n)) ) holds
b₁ = b₂

proof end;

end;

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

theorem :: MOEBIUS3:34

Sum (Sgm {1}) = 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;

cluster SetPrimes n -> finite ;

coherence
SetPrimes n is finite ;

end;

theorem :: MOEBIUS3:35

for m, n being Nat st m <= n holds
SetPrimes m c= SetPrimes n by XBOOLE_1:26, FINSEQ_1:5;

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

( SetPrimes 0 = {} & SetPrimes 1 = {} )

proof end;

theorem PrimesSet2: :: MOEBIUS3:38

for n being Nat st n + 1 is Prime holds
SetPrimes (n + 1) = (SetPrimes n) \/ {(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

SetPrimes 2 = {2}

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 (SetPrimes n);

coherence
card (SetPrimes n) is Nat ;

end;

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

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 n div ((SqF n) |^ 2) -> square-free for Nat;

coherence
for b₁ being Nat st b₁ = n div ((SqF n) |^ 2) holds
not b₁ 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;

cluster SquarefreePart n -> non zero square-free ;

coherence
not SquarefreePart n is square-containing ;

end;

theorem Canonical: :: MOEBIUS3:47

for n being non zero Nat holds n = (SquarefreePart n) * ((SqF n) ^2)

proof end;

theorem :: MOEBIUS3:48

for n being non zero Nat holds support (pfexp n) 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 (SquarefreePart n) 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 Surprise, NAT_D:6;

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
(EmptyBag SetPrimes) +* (id A);

coherence
(EmptyBag SetPrimes) +* (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 = (EmptyBag SetPrimes) +* (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;

cluster A -bag -> prime-factorization-like ;

coherence
A -bag is prime-factorization-like

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 Product (A -bag) -> square-free for Nat;

coherence
for b₁ being Nat st b₁ = Product (A -bag) holds
not b₁ is square-containing by ProdSqF;

end;

theorem :: MOEBIUS3:57

for n being non zero Nat
for x being object st x in bool (SetPrimes n) 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 (SetPrimes n)),(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

indexp 0 = 0 ;

theorem GreaterProduct: :: MOEBIUS3:61

for n being Nat holds (Partial_Product Reci-seq2) . n > 0

proof end;

theorem Crucial5X: :: MOEBIUS3:62

for n being Nat holds ln . ((Partial_Product Reci-seq2) . n) <= (Partial_Sums ReciPrime) . n

proof end;

theorem :: MOEBIUS3:63

for n being Nat holds ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . 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 / (SquarefreePart i) ) );

existence
ex b₁ being Real_Sequence st
( b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (SquarefreePart i) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (SquarefreePart i) ) & b₂ . 0 = 0 & ( for i being non zero Nat holds b₂ . i = 1 / (SquarefreePart i) ) holds
b₁ = b₂

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 b₁ being Real_Sequence st
( b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (TSqF i) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (TSqF i) ) & b₂ . 0 = 0 & ( for i being non zero Nat holds b₂ . i = 1 / (TSqF i) ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem MySum2Def defines Reci-TSq MOEBIUS3:def 9 :
for b₁ being Real_Sequence holds
( b₁ = Reci-TSq iff ( b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . 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 <= ((Partial_Sums Reci-Sqf) . n) * ((Partial_Sums Reci-TSq) . n) by SERIES_3:39, Seqs1, Seqs4, Core1;

definition

let n be non zero Nat;

func Compose n -> Function of [:(bool (SetPrimes n)),(Seg n):],NAT means :: MOEBIUS3:def 10
for x being Element of [:(bool (SetPrimes n)),(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 b₁ being Function of [:(bool (SetPrimes n)),(Seg n):],NAT st
for x being Element of [:(bool (SetPrimes n)),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b₁ . x = (Product ((A,1) -bag)) * (k ^2)

proof end;

uniqueness
for b₁, b₂ being Function of [:(bool (SetPrimes n)),(Seg n):],NAT st ( for x being Element of [:(bool (SetPrimes n)),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b₁ . x = (Product ((A,1) -bag)) * (k ^2) ) & ( for x being Element of [:(bool (SetPrimes n)),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b₂ . x = (Product ((A,1) -bag)) * (k ^2) ) holds
b₁ = b₂

proof end;

end;

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

theorem :: MOEBIUS3:69

for n being Nat holds (Partial_Sums Basel-seq) . 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 (SetPrimes n) : verum } ;

coherence
{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : 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 (SetPrimes n) : verum } ;

registration

let n be Nat;

cluster ReciProducts n -> finite ;

correctness
coherence
ReciProducts n is finite ;

proof end;

end;

theorem :: MOEBIUS3:70

ReciProducts 0 = {1}

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

ReciProducts 1 = {1}

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) = (ReciProducts n) \/ { (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 (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

proof end;