:: Sequences of Prime Reciprocals -- Preliminaries :: by Adam Grabowski :: :: Received March 27, 2018 :: Copyright (c) 2018-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 ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, INT_1, SQUARE_1, SEQ_1, MEASURE5, FACIRC_1, FUNCT_4, ABIAN, VALUED_1, REALSET1, SERIES_1, POWER, FUNCT_7, FINSET_1, CARD_1, MCART_1, MOEBIUS1, RCOMP_1, SIN_COS, TAYLOR_2, INTEGRA5, PYTHTRIP, BASEL_1, LIMFUNC1, PRE_POLY, XXREAL_2, PARTFUN1, NEWTON, XXREAL_0, ORDINAL4, XBOOLE_0, REAL_1, INT_2, TARSKI, PARTFUN3, NAT_1, TAYLOR_1, SEQ_4, XXREAL_1, FDIFF_1, PBOOLE, NAT_3, CARD_3, VALUED_0, UPROOTS, INT_7, SERIES_3, XCMPLX_0, SUBSET_1, ZFMISC_1, NUMBERS, MOEBIUS2, MOEBIUS3, INTEGRA1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XTUPLE_0, XXREAL_0, XCMPLX_0, VALUED_0, ZFMISC_1, FINSET_1, SQUARE_1, ABIAN, INT_1, INT_2, NAT_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, VALUED_1, FUNCT_4, FINSEQ_1, PARTFUN3, PRE_POLY, RCOMP_1, FCONT_1, MEASURE5, RFUNCT_1, SEQ_4, PBOOLE, NAT_D, SEQ_1, SEQ_2, RVSUM_1, SERIES_1, PYTHTRIP, UPROOTS, BINOP_1, NEWTON, POWER, TAYLOR_1, INT_7, SERIES_3, NAT_3, PEPIN, MOEBIUS1, MOEBIUS2, PARTFUN1, SIN_COS, RELSET_1, PARTFUN2, FDIFF_1, LIMFUNC1, INTEGRA5, TAYLOR_2, BASEL_1; constructors SIN_COS, UPROOTS, INT_7, SERIES_3, COMSEQ_2, INTEGRA1, FCONT_1, TAYLOR_2, ABIAN, MOEBIUS1, FINSOP_1, RVSUM_1, BAGORDER, SERIES_1, REAL_1, PARTFUN3, PEPIN, NAT_3, RELSET_1, RECDEF_1, MOEBIUS2, TAYLOR_1, PYTHTRIP, INTEGRA5, SEQ_4, PARTFUN2, BASEL_1, FDIFF_1, LIMFUNC1; registrations RELSET_1, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSET_1, XXREAL_0, FUNCT_1, NEWTON, XCMPLX_0, NUMBERS, ORDINAL1, PRE_POLY, NAT_3, MOEBIUS2, RCOMP_1, COMSEQ_3, INT_7, SEQ_4, XBOOLE_0, VALUED_0, XXREAL_2, FUNCT_2, MEASURE5, ABIAN, INTEGRA1, RELAT_1, NEWTON03, XTUPLE_0, SUBSET_1, VALUED_1, FCONT_3, POWER, NEWTON04; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve n,i,k,m for Nat; reserve p for Prime; registration cluster non zero square non trivial for Nat; 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; end; theorem :: MOEBIUS3:1 for Z being Subset of REAL st 0 in Z holds (id Z)"{0} = {0}; theorem :: MOEBIUS3:2 for Z being Subset of REAL st not 0 in Z holds (id Z)"{0} = {}; theorem :: MOEBIUS3:3 for Z being open Subset of REAL, A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds ((id Z)^) | A is continuous; theorem :: MOEBIUS3:4 for Z being open Subset of REAL, 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); theorem :: MOEBIUS3:5 for Z being open Subset of REAL, 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); theorem :: MOEBIUS3:6 for x,r being Real st x > 0 & r > 0 holds Maclaurin(exp_R,].-r,r.[,x) is positive-yielding; theorem :: MOEBIUS3:7 for f be summable Real_Sequence, n be Nat st f is positive-yielding holds Sum (f ^\ (n+1)) > 0; begin :: Harmonic Numbers :: n-th harmonic number definition let n be Nat; func Harmonic n -> Real equals :: MOEBIUS3:def 1 (Partial_Sums invNAT).n; end; theorem :: MOEBIUS3:8 Harmonic 0 = 0; theorem :: MOEBIUS3:9 Harmonic (n + 1) = Harmonic n + 1 / (n + 1); theorem :: MOEBIUS3:10 Harmonic 1 = 1; theorem :: MOEBIUS3:11 Harmonic 2 = 3 / 2; begin :: On Exponents and Logarithms theorem :: MOEBIUS3:12 ln.1 = 0; theorem :: MOEBIUS3:13 for x being Real st x > 0 holds exp_R.x > x + 1; theorem :: MOEBIUS3:14 for x being Real st x > 0 holds ln.(x + 1) < x; theorem :: MOEBIUS3:15 for n being Nat st n > 0 holds ln.((n + 1) / n) < 1 / n; theorem :: MOEBIUS3:16 for x being Real holds ln.(exp_R.x) = x; theorem :: MOEBIUS3:17 for x,y being Real st 0 < x < y holds ln.x < ln.y; theorem :: MOEBIUS3:18 for n being non zero Nat holds ln.(n+1) > 0; theorem :: MOEBIUS3:19 for x,y being Real st 0 < x & 0 < y holds ln.(x * y) = ln.x + ln.y; theorem :: MOEBIUS3:20 for x being Real holds ex y being non zero Nat st x < ln.(ln.(y + 1)); theorem :: MOEBIUS3:21 for A being non empty closed_interval Subset of REAL, Z being open Subset of REAL, n being non zero Nat st Z = right_open_halfline 0 & A = [.n, n+1.] holds integral ((id Z)^,A) < 1 / n; theorem :: MOEBIUS3:22 for n being non zero Nat holds ln.(n + 1) < Harmonic n; theorem :: MOEBIUS3:23 for n1, n2 being Nat st n1 ^2 = n2 ^2 holds n1 = n2; registration let n be non trivial Nat; cluster n ^2 -> non trivial; end; ::$N Telescoping series theorem :: 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); theorem :: MOEBIUS3:25 for f1, f2 being Real_Sequence, 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); begin :: Some Special Sequences definition func Reci-seq1 -> Real_Sequence means :: MOEBIUS3:def 2 for n being Nat holds it.n = 1 / (n ^2 - 1 / 4); end; theorem :: MOEBIUS3:26 for n being Nat holds Reci-seq1.n = 1 / (n - 1 / 2) - 1 / (n + 1 / 2); theorem :: MOEBIUS3:27 Reci-seq1 = (rseq (0,1,1, -1/2)) + (- rseq (0,1,1, 1 / 2)); theorem :: MOEBIUS3:28 for n being Nat holds (Partial_Sums Reci-seq1).n < -2; theorem :: MOEBIUS3:29 for n being Nat holds Sum (Reci-seq1, n, 1) < 2 / 3; registration cluster Basel-seq -> summable; end; theorem :: MOEBIUS3:30 for n being Nat holds (Partial_Sums Reci-seq1).n = -2 + - 1 / (n + 1 / 2); theorem :: MOEBIUS3:31 for n being non trivial Nat holds Sum (Basel-seq, n, 1) < Sum (Reci-seq1, n, 1); theorem :: MOEBIUS3:32 for n being non trivial Nat holds Sum (Basel-seq, n) < 5 / 3; theorem :: MOEBIUS3:33 ::: Similar bound in BASEL series, counted independently (Partial_Sums Basel-seq).n < 5 / 3; definition func Reci-seq2 -> Real_Sequence means :: MOEBIUS3:def 3 for n being Nat holds it.n = 1 + 1 / primenumber n; end; :: similar functor is in MOEBIUS2 theorem :: MOEBIUS3:34 Sum Sgm {1} = 1; definition let n be Nat; func SetPrimes n -> Subset of NAT equals :: MOEBIUS3:def 4 SetPrimes /\ Seg n; end; registration let n be Nat; cluster SetPrimes n -> finite; end; theorem :: MOEBIUS3:35 for m, n being Nat st m <= n holds SetPrimes m c= SetPrimes n; theorem :: MOEBIUS3:36 n+1 is not Prime implies SetPrimes (n+1) = SetPrimes n; theorem :: MOEBIUS3:37 SetPrimes 0 = {} & SetPrimes 1 = {}; theorem :: MOEBIUS3:38 n+1 is Prime implies SetPrimes (n+1) = SetPrimes n \/ {n+1}; theorem :: MOEBIUS3:39 for p being Prime st p > 2 holds p+1 is not Prime; theorem :: MOEBIUS3:40 SetPrimes 2 = {2}; theorem :: MOEBIUS3:41 not n+1 in SetPrimes n; 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; end; theorem :: MOEBIUS3:42 for n being Nat holds indexp n <= n; begin :: Squarefree and Square-containing Parts of a Natural Number theorem :: MOEBIUS3:43 for n being non zero Nat holds n = (TSqF n) * (n div TSqF n); theorem :: MOEBIUS3:44 ::: MOEBIUS2:45 strenghtened for n being non zero Nat holds (SqF n) |^ 2 divides n; theorem :: MOEBIUS3:45 for m being finite-support natural-valued ManySortedSet of SetPrimes, p being Prime st support m = {p} holds Product m = m.p; theorem :: MOEBIUS3:46 for n being non zero Nat holds (SqF n) |^ 2 = TSqF n; registration let n be non zero Nat; cluster n div ((SqF n) |^ 2) -> square-free for Nat; 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; end; registration let n be non zero Nat; cluster SquarefreePart n -> square-free; end; theorem :: MOEBIUS3:47 ::: squarefree-decompose for n being non zero Nat holds n = (SquarefreePart n) * (SqF n) ^2; theorem :: MOEBIUS3:48 for n being non zero Nat holds support pfexp n c= Seg n; theorem :: MOEBIUS3:49 ::: a kind of generalized MOEBIUS1:14 for n being non zero Nat holds support ppf n c= Seg n; theorem :: MOEBIUS3:50 for n being non zero Nat holds Seg SquarefreePart n c= Seg n; theorem :: MOEBIUS3:51 for k,n being non zero Nat holds k^2 divides SquarefreePart n iff k = 1; theorem :: MOEBIUS3:52 for m,n being non zero Nat st SquarefreePart n = SquarefreePart m & TSqF m = TSqF n holds m = n; begin :: Generating Bags from Subsets of Prime Numbers definition let A be finite Subset of SetPrimes; func A-bag -> bag of SetPrimes equals :: MOEBIUS3:def 7 (EmptyBag SetPrimes) +* (id A); end; theorem :: MOEBIUS3:53 for A being finite Subset of SetPrimes holds support (A-bag) = A; theorem :: MOEBIUS3:54 for A being finite Subset of SetPrimes st A = {} holds A-bag = EmptyBag SetPrimes; theorem :: MOEBIUS3:55 for A being finite Subset of SetPrimes for i being object st i in support (A-bag) holds (A-bag).i = i; theorem :: MOEBIUS3:56 for A,B be finite Subset of SetPrimes st A-bag = B-bag holds A = B; registration let A be finite Subset of SetPrimes; cluster A-bag -> prime-factorization-like; end; registration let A be finite Subset of SetPrimes; cluster Product (A-bag) -> square-free for Nat; 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; 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; :: 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; theorem :: MOEBIUS3:60 indexp 0 = 0; theorem :: MOEBIUS3:61 for n being Nat holds (Partial_Product Reci-seq2).n > 0; theorem :: MOEBIUS3:62 for n being Nat holds ln.((Partial_Product Reci-seq2).n) <= (Partial_Sums ReciPrime).n; theorem :: MOEBIUS3:63 for n being Nat holds ln.((Partial_Product Reci-seq2).(indexp n)) <= (Partial_Sums ReciPrime).n; definition func Reci-Sqf-> Real_Sequence means :: MOEBIUS3:def 8 it.0 = 0 & for i being non zero Nat holds it.i = 1 / SquarefreePart i; func Reci-TSq -> Real_Sequence means :: MOEBIUS3:def 9 it.0 = 0 & for i being non zero Nat holds it.i = 1 / TSqF i; end; theorem :: MOEBIUS3:64 rseq (0,1,1,0) = Reci-Sqf (#) Reci-TSq; reserve s, s1, s2 for Real_Sequence; theorem :: MOEBIUS3:65 for n being Nat holds Reci-Sqf.n >= 0; theorem :: MOEBIUS3:66 for n being Nat holds Reci-TSq.n >= 0; theorem :: MOEBIUS3:67 for n being Nat holds Basel-seq.n >= 0; theorem :: MOEBIUS3:68 :::Seqs5: for n being Nat holds (Partial_Sums rseq (0,1,1,0)).n <= (Partial_Sums Reci-Sqf).n * (Partial_Sums Reci-TSq).n; 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:], A being finite Subset of SetPrimes, k being Nat st x = [A, k] holds it.x = (Product ((A,1)-bag)) * k ^2; end; theorem :: MOEBIUS3:69 (Partial_Sums Basel-seq).n >= 0; begin :: On Reciprocals of Products of Prime Numbers definition let n be Nat; func ReciProducts n -> Subset of REAL equals :: MOEBIUS3:def 11 the set of all 1 / Product Sgm X where X is Subset of SetPrimes n; end; registration let n be Nat; cluster ReciProducts n -> finite; end; theorem :: MOEBIUS3:70 ReciProducts 0 = { 1 }; theorem :: MOEBIUS3:71 for p being Prime st p > 2 holds ReciProducts (p+1) = ReciProducts p; theorem :: MOEBIUS3:72 for p being Nat st p+1 is not Prime holds ReciProducts (p+1) = ReciProducts p; theorem :: MOEBIUS3:73 ReciProducts 1 = { 1 }; theorem :: MOEBIUS3:74 ReciProducts 2 = { 1 / 2, 1 }; theorem :: MOEBIUS3:75 for n be Nat holds ReciProducts n c= ReciProducts (n+1); theorem :: MOEBIUS3:76 for n be 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}; theorem :: MOEBIUS3:77 for n be 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};