MOEBIUS1: On the Properties of the {M}\"obius Function

:: On the Properties of the {M}\"obius Function
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 21, 2006
:: Copyright (c) 2006-2011 Association of Mizar Users

begin

Lm1: for X, Y, Z, x being set st X misses Y & x in X /\ Z holds
not x in Y /\ Z

proof end;

scheme :: MOEBIUS1:sch 1
LambdaNATC{ F₁() -> Element of NAT , F₂() -> set , F₃( set ) -> set } :

ex f being Function of NAT,F₂() st
( f . 0 = F₁() & ( for x being non zero Element of NAT holds f . x = F₃(x) ) )

provided

A1: F₁() in F₂() and
A2: for x being non zero Element of NAT holds F₃(x) in F₂()

proof end;

registration

cluster non zero epsilon-transitive epsilon-connected ordinal natural complex real V16() non prime finite cardinal V46() V80() V81() V82() V83() V84() V85() ext-real non negative V208() V209() V210() Element of NAT ;
existence by INT_2:46;

end;

theorem Th1: :: MOEBIUS1:1

for n being non zero natural number st n <> 1 holds
n >= 2

proof end;

theorem :: MOEBIUS1:2

for k, n, i being natural number st 1 <= k holds
( i in Seg n iff k * i in Seg (k * n) )

proof end;

theorem :: MOEBIUS1:3

for m, n being Element of NAT holds
( not m,n are_relative_prime or m > 0 or n > 0 )

proof end;

Lm2: for n being natural number st n <> 1 holds
ex p being Prime st p divides n

proof end;

theorem Th4: :: MOEBIUS1:4

for n being non prime Element of NAT st n <> 1 holds
ex p being Prime st
( p divides n & p <> n )

proof end;

theorem Th5: :: MOEBIUS1:5

for n being natural number st n <> 1 holds
ex p being Prime st p divides n

proof end;

theorem Th6: :: MOEBIUS1:6

for p being Prime
for n being non zero natural number holds
( p divides n iff p |-count n > 0 )

proof end;

theorem Th7: :: MOEBIUS1:7

support (ppf 1) = {}

proof end;

theorem Th8: :: MOEBIUS1:8

for p being Prime holds support (ppf p) = {p}

proof end;

theorem Th9: :: MOEBIUS1:9

for n, m being natural number
for p being Prime st n <> 0 & m <= p |-count n holds
p |^ m divides n

proof end;

theorem Th10: :: MOEBIUS1:10

for a being Element of NAT
for p being Prime st p |^ 2 divides a holds
p divides a

proof end;

theorem Th11: :: MOEBIUS1:11

for p being prime Element of NAT
for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n

proof end;

theorem Th12: :: MOEBIUS1:12

for n being natural number
for N being Rbag of NAT st support N = {n} holds
Sum N = N . n

proof end;

registration

cluster canFS {} -> empty ;
coherence ;

end;

theorem :: MOEBIUS1:13

for n being natural number
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 ) }

proof end;

theorem Th14: :: MOEBIUS1:14

for n being non zero natural number ex k being Element of NAT st support (ppf n) c= Seg k

proof end;

theorem Th15: :: MOEBIUS1:15

for n being non zero Element of NAT
for p being Prime st not p in support (ppf n) holds
p |-count n = 0

proof end;

theorem Th16: :: MOEBIUS1:16

for k being Element of NAT
for 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

proof end;

theorem Th17: :: MOEBIUS1:17

for m, n being non zero natural number st ( for p being Prime holds p |-count m <= p |-count n ) holds
support (ppf m) c= support (ppf n)

proof end;

theorem Th18: :: MOEBIUS1:18

for k being Element of NAT
for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds
ex m being non zero Element of NAT ex 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 ) ) ) )

proof end;

theorem Th19: :: MOEBIUS1:19

for m, n being non zero natural number st ( for p being Prime holds p |-count m <= p |-count n ) holds
m divides n

proof end;

begin

definition

let x be natural number ;
attr x is square-containing means :Def1: :: MOEBIUS1:def 1
ex p being Prime st p |^ 2 divides x;

end;

:: deftheorem Def1 defines square-containing MOEBIUS1:def 1 :

theorem Th20: :: MOEBIUS1:20

for n being natural number st ex p being non zero natural number st
( p <> 1 & p |^ 2 divides n ) holds
n is square-containing

proof end;

notation

let x be natural number ;
antonym square-free x for square-containing ;

end;

theorem Th21: :: MOEBIUS1:21

0 is square-containing

proof end;

theorem Th22: :: MOEBIUS1:22

not 1 is square-containing

proof end;

theorem Th23: :: MOEBIUS1:23

for p being Prime holds not p is square-containing

proof end;

registration

cluster prime -> square-free Element of NAT ;
coherence by Th23;

end;

definition

func SCNAT -> Subset of NAT means :Def2: :: MOEBIUS1:def 2
for n being natural number holds
( n in it iff not n is square-containing );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :

registration

cluster epsilon-transitive epsilon-connected ordinal natural complex real V16() finite cardinal ext-real non negative square-free set ;
existence by Th22;
cluster epsilon-transitive epsilon-connected ordinal natural complex real V16() finite cardinal ext-real non negative square-containing set ;
existence

proof end;

end;

registration

cluster non trivial natural square -> natural square-containing set ;
coherence

proof end;

end;

theorem Th24: :: MOEBIUS1:24

for n being natural number st not n is square-containing holds
for p being Prime holds p |-count n <= 1

proof end;

theorem Th25: :: MOEBIUS1:25

for m, n being natural number st not m * n is square-containing holds
not m is square-containing

proof end;

theorem Th26: :: MOEBIUS1:26

for m, n being natural number st not m is square-containing & n divides m holds
not n is square-containing

proof end;

theorem Th27: :: MOEBIUS1:27

for p being Prime
for m, d being natural number st not m is square-containing & p divides m & d divides m div p holds
( d divides m & not p divides d )

proof end;

theorem Th28: :: MOEBIUS1:28

for p being Prime
for m, d being natural number st p divides m & d divides m & not p divides d holds
d divides m div p

proof end;

theorem :: MOEBIUS1:29

for p being Prime
for m being natural number st not m is square-containing & 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 ) }

proof end;

begin

definition

let n be natural number ;
func Moebius n -> real number means :Def3: :: MOEBIUS1:def 3
it = 0 if n is square-containing
otherwise ex n9 being non zero natural number st
( n9 = n & it = (- 1) |^ (card (support (ppf n9))) );
consistency ;
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines Moebius MOEBIUS1:def 3 :

theorem Th30: :: MOEBIUS1:30

Moebius 1 = 1

proof end;

theorem :: MOEBIUS1:31

Moebius 2 = - 1

proof end;

theorem :: MOEBIUS1:32

Moebius 3 = - 1

proof end;

theorem Th33: :: MOEBIUS1:33

for n being natural number st not n is square-containing holds
Moebius n <> 0

proof end;

registration

let n be natural square-free number ;
cluster Moebius n -> non zero real ;
coherence by Th33;

end;

theorem Th34: :: MOEBIUS1:34

for p being Prime holds Moebius p = - 1

proof end;

theorem Th35: :: MOEBIUS1:35

for m, n being non zero Element of NAT st m,n are_relative_prime holds
Moebius (m * n) = (Moebius m) * (Moebius n)

proof end;

theorem :: MOEBIUS1:36

for p being Prime
for n being Element of NAT st 1 <= n & not n * p is square-containing holds
Moebius (n * p) = - (Moebius n)

proof end;

theorem :: MOEBIUS1:37

for m, n being non zero Element of NAT st not m,n are_relative_prime holds
Moebius (m * n) = 0

proof end;

theorem Th38: :: MOEBIUS1:38

for n being natural number holds
( n in SCNAT iff Moebius n <> 0 )

proof end;

begin

definition

let n be natural number ;
func NatDivisors n -> Subset of NAT equals :: MOEBIUS1:def 4
{ k where k is Element of NAT : ( k <> 0 & k divides n ) } ;
coherence

proof end;

end;

:: deftheorem defines NatDivisors MOEBIUS1:def 4 :

theorem :: MOEBIUS1:39

for n, k being natural number holds
( k in NatDivisors n iff ( 0 < k & k divides n ) )

proof end;

theorem Th40: :: MOEBIUS1:40

for n being non zero natural number holds NatDivisors n c= Seg n

proof end;

registration

let n be non zero natural number ;
cluster NatDivisors n -> with_non-empty_elements finite ;
coherence

proof end;

end;

theorem Th41: :: MOEBIUS1:41

NatDivisors 1 = {1}

proof end;

begin

definition

let X be set ;
func SMoebius X -> ManySortedSet of NAT means :Def5: :: MOEBIUS1:def 5
( support it = X /\ SCNAT & ( for k being Element of NAT st k in support it holds
it . k = Moebius k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines SMoebius MOEBIUS1:def 5 :

registration

let X be set ;
cluster SMoebius X -> real-valued ;
coherence

proof end;

end;

registration

let X be finite set ;
cluster SMoebius X -> finite-support ;
coherence

proof end;

end;

theorem :: MOEBIUS1:42

Sum (SMoebius (NatDivisors 1)) = 1

proof end;

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))

proof end;

theorem :: MOEBIUS1:44

for X, Y being finite Subset of NAT st X misses Y holds
SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)

proof end;

begin

definition

let n be non zero natural number ;
func PFactors n -> ManySortedSet of SetPrimes means :Def6: :: MOEBIUS1:def 6
( support it = support (pfexp n) & ( for p being natural number st p in support (pfexp n) holds
it . p = p ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :

registration

let n be non zero natural number ;
cluster PFactors n -> natural-valued finite-support ;
coherence

proof end;

end;

theorem Th45: :: MOEBIUS1:45

PFactors 1 = EmptyBag SetPrimes

proof end;

theorem Th46: :: MOEBIUS1:46

for p being Prime holds (PFactors p) * <*p*> = <*p*>

proof end;

theorem Th47: :: MOEBIUS1:47

for p being Prime
for n being non zero natural number holds (PFactors (p |^ n)) * <*p*> = <*p*>

proof end;

theorem Th48: :: MOEBIUS1:48

for p being Prime
for n being non zero natural number st p |-count n = 0 holds
(PFactors n) . p = 0

proof end;

theorem Th49: :: MOEBIUS1:49

for n being non zero natural number
for p being Prime st p |-count n <> 0 holds
(PFactors n) . p = p

proof end;

theorem Th50: :: MOEBIUS1:50

for m, n being non zero Element of NAT st m,n are_relative_prime holds
PFactors (m * n) = (PFactors m) + (PFactors n)

proof end;

theorem :: MOEBIUS1:51

for n being non zero Element of NAT
for 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

proof end;

begin

definition

let n be non zero natural number ;
func Radical n -> Element of NAT equals :: MOEBIUS1:def 7
Product (PFactors n);
coherence ;

end;

:: deftheorem defines Radical MOEBIUS1:def 7 :

theorem Th52: :: MOEBIUS1:52

for n being non zero natural number holds Radical n > 0

proof end;

registration

let n be non zero natural number ;
cluster Radical n -> non zero ;
coherence by Th52;

end;

theorem :: MOEBIUS1:53

for p being Prime holds p = Radical p

proof end;

theorem Th54: :: MOEBIUS1:54

for p being Prime
for n being non zero Element of NAT holds Radical (p |^ n) = p

proof end;

theorem Th55: :: MOEBIUS1:55

for n being non zero natural number holds Radical n divides n

proof end;

theorem Th56: :: MOEBIUS1:56

for p being Prime
for n being non zero natural number holds
( p divides n iff p divides Radical n )

proof end;

theorem Th57: :: MOEBIUS1:57

for k being non zero natural number st not k is square-containing holds
Radical k = k

proof end;

theorem :: MOEBIUS1:58

for n being non zero natural number holds Radical n <= n by Th55, NAT_D:7;

theorem :: MOEBIUS1:59

for p being Prime
for n being non zero natural number holds p |-count (Radical n) <= p |-count n by Th55, NAT_3:30;

theorem :: MOEBIUS1:60

for n being non zero natural number holds
( Radical n = 1 iff n = 1 )

proof end;

theorem Th61: :: MOEBIUS1:61

for p being Prime
for n being non zero natural number holds p |-count (Radical n) <= 1

proof end;

Lm3: for n being non zero natural number
for p being Prime holds not p |^ 2 divides Radical n

proof end;

Lm4: for n being non zero natural number holds not Radical n is square-containing

proof end;

registration

let n be non zero natural number ;
cluster Radical n -> square-free ;
coherence by Lm4;

end;

theorem :: MOEBIUS1:62

for n being non zero natural number holds Radical (Radical n) = Radical n by Th57;

theorem :: MOEBIUS1:63

for n being non zero Element of NAT
for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n

proof end;

theorem :: MOEBIUS1:64

for n being non zero Element of NAT
for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n

proof end;

Lm5: for m, n being non zero Element of NAT st m divides n & not m is square-containing holds
m divides Radical n

proof end;

theorem Th65: :: MOEBIUS1:65

for k, n being non zero natural number holds
( ( k divides n & not k is square-containing ) iff k divides Radical n )

proof end;

theorem :: MOEBIUS1:66

for n being non zero natural number holds { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }

proof end;