:: On the Properties of the {M}\"obius Function :: by Magdalena Jastrz\c{e}bska and Adam Grabowski :: :: Received March 21, 2006 :: Copyright (c) 2006-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 NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, XCMPLX_0, INT_2, XXREAL_0, ARYTM_3, FINSEQ_1, RELAT_1, ABIAN, NEWTON, NAT_3, PRE_POLY, NAT_1, UPROOTS, CARD_3, TARSKI, INT_1, FINSET_1, ARYTM_1, PYTHTRIP, ZFMISC_1, SQUARE_1, REAL_1, SETFAM_1, PBOOLE, VALUED_0, FUNCOP_1, MOEBIUS1, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NEWTON, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0, PBOOLE, SQUARE_1, RVSUM_1, FUNCOP_1, XXREAL_2, NAT_3, DOMAIN_1, ABIAN, UPROOTS, PYTHTRIP, RECDEF_1, PRE_POLY, REAL_1, NAT_1, NAT_D, INT_2; constructors NAT_D, FINSOP_1, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, UPROOTS, NAT_3, RECDEF_1, BINOP_2, XXREAL_2, REAL_1, DOMAIN_1, RELSET_1; registrations XBOOLE_0, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON, NAT_3, VALUED_0, XXREAL_2, CARD_1, RELSET_1, PRE_POLY; requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE; begin scheme :: MOEBIUS1:sch 1 LambdaNATC{A() -> Element of NAT, B() -> set, F(object)->set}: ex f being sequence of B() st f.0 = A() & for x being non zero Element of NAT holds f.x = F(x) provided A() in B() and for x being non zero Element of NAT holds F(x) in B(); registration cluster non prime non zero for Element of NAT; end; theorem :: MOEBIUS1:1 for n being non zero Nat holds n <> 1 implies n >= 2; theorem :: MOEBIUS1:2 for k, n, i being Nat st 1 <= k holds i in Seg n iff k * i in Seg (k * n); theorem :: MOEBIUS1:3 for m, n being Element of NAT st m, n are_coprime holds m > 0 or n > 0; theorem :: MOEBIUS1:4 for n being non prime Element of NAT st n <> 1 ex p being Prime st p divides n & p <> n; theorem :: MOEBIUS1:5 for n being Nat st n <> 1 ex p being Prime st p divides n; theorem :: MOEBIUS1:6 for p being Prime, n being non zero Nat holds p divides n iff p |-count n > 0; theorem :: MOEBIUS1:7 support ppf 1 = {}; theorem :: MOEBIUS1:8 for p being Prime holds support ppf p = {p}; reserve m, n for Nat; theorem :: MOEBIUS1:9 for p being Prime st n <> 0 & m <= p |-count n holds p |^ m divides n; theorem :: MOEBIUS1:10 for a being Element of NAT, p being Prime holds p |^ 2 divides a implies p divides a; theorem :: MOEBIUS1:11 for p being prime Element of NAT, m, n being non zero Element of NAT st m, n are_coprime & p |^ 2 divides (m * n) holds p |^ 2 divides m or p |^ 2 divides n; theorem :: MOEBIUS1:12 for N being Rbag of NAT st support N = {n} holds Sum N = N.n; registration cluster canFS {} -> empty; end; theorem :: MOEBIUS1:13 for p being Prime st p divides n holds { d where d is Element of NAT : d > 0 & d divides n & p divides d } = { p * d where d is Element of NAT : d > 0 & d divides (n div p) }; theorem :: MOEBIUS1:14 for n being non zero Nat holds ex k being Element of NAT st support ppf n c= Seg k; theorem :: MOEBIUS1:15 for n being non zero Element of NAT, p being Prime st not p in support ppf n holds p |-count n = 0; theorem :: MOEBIUS1:16 for k being Nat, n being non zero Element of NAT st support ppf n c= Seg (k+1) & not support ppf n c= Seg k holds k+1 is Prime; theorem :: MOEBIUS1:17 for m, n being non zero Nat st (for p being Prime holds p |-count m <= p |-count n) holds support ppf m c= support ppf n; theorem :: MOEBIUS1:18 for k being Nat, n being non zero Element of NAT st support ppf n c= Seg (k+1) holds ex m being non zero Element of NAT, e being Element of NAT st support ppf m c= Seg k & n = m * ((k+1) |^ e) & for p being Prime holds (p in support ppf m implies p |-count m = p |-count n) & (not p in support ppf m implies p |-count m <= p |-count n); theorem :: MOEBIUS1:19 for m, n being non zero Nat st (for p being Prime holds p |-count m <= p |-count n) holds m divides n; begin :: Squarefree Numbers definition let x be Nat; attr x is square-containing means :: MOEBIUS1:def 1 ex p being Prime st p |^ 2 divides x; end; theorem :: MOEBIUS1:20 for n being Nat st ex p being non zero Nat st p <> 1 & p |^ 2 divides n holds n is square-containing; notation let x be Nat; antonym x is square-free for x is square-containing; end; theorem :: MOEBIUS1:21 0 is square-containing; theorem :: MOEBIUS1:22 1 is square-free; theorem :: MOEBIUS1:23 for p being Prime holds p is square-free; registration cluster prime -> square-free for Element of NAT; end; definition func SCNAT -> Subset of NAT means :: MOEBIUS1:def 2 for n being Nat holds n in it iff n is square-free; end; registration cluster square-free for Nat; cluster square-containing for Nat; end; registration cluster square non trivial -> square-containing for Nat; end; theorem :: MOEBIUS1:24 n is square-free implies for p being Prime holds p |-count n <= 1; theorem :: MOEBIUS1:25 m * n is square-free implies m is square-free; theorem :: MOEBIUS1:26 m is square-free & n divides m implies n is square-free; theorem :: MOEBIUS1:27 for p being Prime, m, d being Nat st m is square-free & p divides m & d divides (m div p) holds d divides m & not p divides d; theorem :: MOEBIUS1:28 for p being Prime, m, d being Nat st p divides m & d divides m & not p divides d holds d divides (m div p); theorem :: MOEBIUS1:29 for p being Prime, m being Nat st m is square-free & p divides m holds { d where d is Element of NAT : 0 < d & d divides m & not p divides d } = { d where d is Element of NAT : 0 < d & d divides (m div p) }; begin :: Moebius Function definition let n be Nat; ::$N Moebius function func Moebius n -> Real means :: MOEBIUS1:def 3 it = 0 if n is square-containing otherwise ex n9 being non zero Nat st n9 = n & it = (-1) |^ card support ppf n9; end; theorem :: MOEBIUS1:30 Moebius 1 = 1; theorem :: MOEBIUS1:31 Moebius 2 = -1; theorem :: MOEBIUS1:32 Moebius 3 = -1; theorem :: MOEBIUS1:33 for n being Nat st n is square-free holds Moebius n <> 0; registration let n be square-free Nat; cluster Moebius n -> non zero; end; theorem :: MOEBIUS1:34 for p being Prime holds Moebius p = -1; theorem :: MOEBIUS1:35 for m, n being non zero Element of NAT st m, n are_coprime holds Moebius (m * n) = Moebius m * Moebius n; theorem :: MOEBIUS1:36 for p being Prime, n being Element of NAT st 1 <= n & n * p is square-free holds Moebius (n * p) = - Moebius n; theorem :: MOEBIUS1:37 for m, n being non zero Element of NAT st not m, n are_coprime holds Moebius (m * n) = 0; theorem :: MOEBIUS1:38 for n being Nat holds n in SCNAT iff Moebius n <> 0; begin :: Natural Divisors definition let n be Nat; func NatDivisors n -> Subset of NAT equals :: MOEBIUS1:def 4 { k where k is Element of NAT : k <> 0 & k divides n }; end; theorem :: MOEBIUS1:39 for n, k being Nat holds k in NatDivisors n iff 0 < k & k divides n; theorem :: MOEBIUS1:40 for n being non zero Nat holds NatDivisors n c= Seg n; registration let n be non zero Nat; cluster NatDivisors n -> finite with_non-empty_elements; end; theorem :: MOEBIUS1:41 NatDivisors 1 = {1}; begin :: The Sum of the Moebius Function definition let X be set; func SMoebius X -> ManySortedSet of NAT means :: MOEBIUS1:def 5 support it = X /\ SCNAT & for k being Element of NAT st k in support it holds it.k = Moebius k; end; registration let X be set; cluster SMoebius X -> real-valued; end; registration let X be finite set; cluster SMoebius X -> finite-support; end; theorem :: MOEBIUS1:42 Sum SMoebius NatDivisors 1 = 1; theorem :: MOEBIUS1:43 for X, Y being finite Subset of NAT st X misses Y holds support SMoebius X \/ support SMoebius Y = support (SMoebius X + SMoebius Y); theorem :: MOEBIUS1:44 for X, Y being finite Subset of NAT st X misses Y holds SMoebius (X \/ Y) = SMoebius X + SMoebius Y; begin :: Prime Factors of a Number definition let n be non zero Nat; func PFactors n -> ManySortedSet of SetPrimes means :: MOEBIUS1:def 6 support it = support pfexp n & for p being Nat st p in support pfexp n holds it.p = p; end; registration let n be non zero Nat; cluster PFactors n -> finite-support natural-valued; end; theorem :: MOEBIUS1:45 PFactors 1 = EmptyBag SetPrimes; theorem :: MOEBIUS1:46 for p being Prime holds (PFactors p) * <*p*> = <*p*>; theorem :: MOEBIUS1:47 for p being Prime, n being non zero Nat holds ( PFactors (p|^n)) * <* p *> = <* p *>; theorem :: MOEBIUS1:48 for p being Prime, n being non zero Nat holds p |-count n = 0 implies (PFactors n).p = 0; theorem :: MOEBIUS1:49 for n being non zero Nat, p being Prime st p |-count n <> 0 holds (PFactors n).p = p; theorem :: MOEBIUS1:50 for m, n being non zero Element of NAT st m, n are_coprime holds PFactors (m * n) = PFactors m + PFactors n; theorem :: MOEBIUS1:51 for n being non zero Element of NAT, A being finite Subset of NAT st A = { k where k is Element of NAT : 0 < k & k divides n & k is square-containing } holds SMoebius A = EmptyBag NAT; begin :: The Radical of a Number definition let n be non zero Nat; func Radical n -> Element of NAT equals :: MOEBIUS1:def 7 Product PFactors n; end; theorem :: MOEBIUS1:52 for n being non zero Nat holds Radical n > 0; registration let n be non zero Nat; cluster Radical n -> non zero; end; theorem :: MOEBIUS1:53 for p being Prime holds p = Radical p; theorem :: MOEBIUS1:54 for p being Prime, n being non zero Element of NAT holds Radical (p |^ n) = p ; theorem :: MOEBIUS1:55 for n being non zero Nat holds Radical n divides n; theorem :: MOEBIUS1:56 for p being Prime, n being non zero Nat holds p divides n iff p divides Radical n; theorem :: MOEBIUS1:57 for k being non zero Nat st k is square-free holds Radical k = k; theorem :: MOEBIUS1:58 for n being non zero Nat holds Radical n <= n; theorem :: MOEBIUS1:59 for p being Prime, n being non zero Nat holds p |-count Radical n <= p |-count n; theorem :: MOEBIUS1:60 for n being non zero Nat holds Radical n = 1 iff n = 1; theorem :: MOEBIUS1:61 for p being Prime, n being non zero Nat holds p |-count Radical n <= 1; registration let n be non zero Nat; cluster Radical n -> square-free; end; theorem :: MOEBIUS1:62 for n being non zero Nat holds Radical Radical n = Radical n; theorem :: MOEBIUS1:63 for n being non zero Element of NAT, p being Prime holds { k where k is Element of NAT : 0 < k & k divides Radical n & p divides k } c= Seg n; theorem :: MOEBIUS1:64 for n being non zero Element of NAT, p being Prime holds { k where k is Element of NAT : 0 < k & k divides Radical n & not p divides k } c= Seg n; theorem :: MOEBIUS1:65 for k, n being non zero Nat holds k divides n & k is square-free iff k divides Radical n; theorem :: MOEBIUS1:66 for n being non zero Nat holds { k where k is Element of NAT : 0 < k & k divides n & k is square-free } = { k where k is Element of NAT : 0 < k & k divides Radical n };