:: On the Properties of the {M}\"obius Function
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 21, 2006
:: Copyright (c) 2006-2016 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 };