:: On the Properties of the {M}\"obius Function
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 21, 2006
:: Copyright (c) 2006-2012 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{ F1() -> Element of NAT , F2() -> set , F3( set ) -> set } :
ex f being Function of NAT,F2() st
( f . 0 = F1() & ( for x being non zero Element of NAT holds f . x = F3(x) ) )
provided
A1: F1() in F2() and
A2: for x being non zero Element of NAT holds F3(x) in F2()
proof end;

registration
cluster non zero epsilon-transitive epsilon-connected ordinal natural V11() real V13() non prime finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() for Element of NAT ;
existence
ex b1 being Element of NAT st
( not b1 is prime & not b1 is zero ) by INT_2:29;
end;

theorem Th1: :: MOEBIUS1:1
for n being non zero Nat st n <> 1 holds
n >= 2
proof end;

theorem :: MOEBIUS1:2
for k, n, i being Nat 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 Nat 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 Nat 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 Nat 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 Nat
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 Nat
for N being Rbag of NAT st support N = {n} holds
Sum N = N . n
proof end;

registration
cluster canFS {} -> empty ;
coherence
canFS {} is empty ;
end;

theorem :: MOEBIUS1:13
for n being Nat
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 Nat 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 Nat 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 Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds
m divides n
proof end;

begin

definition
let x be Nat;
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 :
for x being Nat holds
( x is square-containing iff ex p being Prime st p |^ 2 divides x );

theorem Th20: :: 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
proof end;

notation
let x be Nat;
antonym square-free x for square-containing ;
end;

theorem Th21: :: MOEBIUS1:21
0 is square-containing
proof end;

theorem Th22: :: MOEBIUS1:22
1 is square-free
proof end;

theorem Th23: :: MOEBIUS1:23
for p being Prime holds p is square-free
proof end;

registration
cluster prime -> square-free for Element of NAT ;
coherence
for b1 being Element of NAT st b1 is prime holds
b1 is square-free by Th23;
end;

definition
func SCNAT -> Subset of NAT means :Def2: :: MOEBIUS1:def 2
 for n being Nat holds
( n in it iff n is square-free );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff n is square-free )
proof end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff n is square-free ) ) & ( for n being Nat holds
( n in b2 iff n is square-free ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :
for b1 being Subset of NAT holds
( b1 = SCNAT iff for n being Nat holds
( n in b1 iff n is square-free ) );

registration
cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-free for set ;
existence
ex b1 being Nat st b1 is square-free by Th22;
cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-containing for set ;
existence
ex b1 being Nat st b1 is square-containing
proof end;
end;

registration
cluster non trivial natural square -> square-containing for set ;
coherence
for b1 being Nat st b1 is square & not b1 is trivial holds
b1 is square-containing
proof end;
end;

theorem Th24: :: MOEBIUS1:24
for n being Nat st n is square-free holds
for p being Prime holds p |-count n <= 1
proof end;

theorem Th25: :: MOEBIUS1:25
for m, n being Nat st m * n is square-free holds
m is square-free
proof end;

theorem Th26: :: MOEBIUS1:26
for m, n being Nat st m is square-free & n divides m holds
n is square-free
proof end;

theorem Th27: :: MOEBIUS1:27
for p being Prime
for 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 )
proof end;

theorem Th28: :: MOEBIUS1:28
for p being Prime
for m, d being Nat 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 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 ) }
proof end;

begin

definition
let n be Nat;
:: WP: Moebius function
func Moebius n -> real number means :Def3: :: 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))) );
consistency
for b1 being real number holds verum ;
existence
( ( n is square-containing implies ex b1 being real number st b1 = 0 ) & ( not n is square-containing implies ex b1 being real number ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) ) )
proof end;
uniqueness
for b1, b2 being real number holds
( ( n is square-containing & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n is square-containing & ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) & ex n9 being non zero Nat st
( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) implies b1 = b2 ) ) ;
end;

:: deftheorem Def3 defines Moebius MOEBIUS1:def 3 :
for n being Nat
for b2 being real number holds
( ( n is square-containing implies ( b2 = Moebius n iff b2 = 0 ) ) & ( not n is square-containing implies ( b2 = Moebius n iff ex n9 being non zero Nat st
( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) ) ) );

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 Nat st n is square-free holds
Moebius n <> 0
proof end;

registration
let n be square-free Nat;
cluster Moebius n -> non zero real ;
coherence
not Moebius n is empty 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 & n * p is square-free 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 Nat holds
( n in SCNAT iff Moebius n <> 0 )
proof end;

begin

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 ) } ;
coherence
{ k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT
proof end;
end;

:: deftheorem defines NatDivisors MOEBIUS1:def 4 :
for n being Nat holds NatDivisors n = { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;

theorem :: MOEBIUS1:39
for n, k being Nat holds
( k in NatDivisors n iff ( 0 < k & k divides n ) )
proof end;

theorem Th40: :: MOEBIUS1:40
for n being non zero Nat holds NatDivisors n c= Seg n
proof end;

registration
let n be non zero Nat;
cluster NatDivisors n -> finite with_non-empty_elements ;
coherence
( NatDivisors n is finite & NatDivisors n is with_non-empty_elements )
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
ex b1 being ManySortedSet of NAT st
( support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds
b1 . k = Moebius k ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of NAT st support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds
b1 . k = Moebius k ) & support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds
b2 . k = Moebius k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines SMoebius MOEBIUS1:def 5 :
for X being set
for b2 being ManySortedSet of NAT holds
( b2 = SMoebius X iff ( support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds
b2 . k = Moebius k ) ) );

registration
let X be set ;
cluster SMoebius X -> real-valued ;
coherence
SMoebius X is real-valued
proof end;
end;

registration
let X be finite set ;
cluster SMoebius X -> finite-support ;
coherence
SMoebius X is finite-support
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 Nat;
func PFactors n -> ManySortedSet of SetPrimes means :Def6: :: MOEBIUS1:def 6
( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it . p = p ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = PFactors n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p ) ) );

registration
let n be non zero Nat;
cluster PFactors n -> natural-valued finite-support ;
coherence
( PFactors n is finite-support & PFactors n is natural-valued )
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 Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>
proof end;

theorem Th48: :: MOEBIUS1:48
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
(PFactors n) . p = 0
proof end;

theorem Th49: :: MOEBIUS1:49
for n being non zero Nat
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 Nat;
func Radical n -> Element of NAT equals :: MOEBIUS1:def 7
 Product (PFactors n);
coherence
Product (PFactors n) is Element of NAT ;
end;

:: deftheorem defines Radical MOEBIUS1:def 7 :
for n being non zero Nat holds Radical n = Product (PFactors n);

theorem Th52: :: MOEBIUS1:52
for n being non zero Nat holds Radical n > 0
proof end;

registration
let n be non zero Nat;
cluster Radical n -> non zero ;
coherence
not Radical n is empty 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 Nat holds Radical n divides n
proof end;

theorem Th56: :: MOEBIUS1:56
for p being Prime
for n being non zero Nat holds
( p divides n iff p divides Radical n )
proof end;

theorem Th57: :: MOEBIUS1:57
for k being non zero Nat st k is square-free holds
Radical k = k
proof end;

theorem :: MOEBIUS1:58
for n being non zero Nat holds Radical n <= n by Th55, NAT_D:7;

theorem :: MOEBIUS1:59
for p being Prime
for n being non zero Nat holds p |-count (Radical n) <= p |-count n by Th55, NAT_3:30;

theorem :: MOEBIUS1:60
for n being non zero Nat holds
( Radical n = 1 iff n = 1 )
proof end;

theorem Th61: :: MOEBIUS1:61
for p being Prime
for n being non zero Nat holds p |-count (Radical n) <= 1
proof end;

Lm3: for n being non zero Nat
for p being Prime holds not p |^ 2 divides Radical n
proof end;

Lm4: for n being non zero Nat holds Radical n is square-free
proof end;

registration
let n be non zero Nat;
cluster Radical n -> square-free ;
coherence
not Radical n is square-containing by Lm4;
end;

theorem :: MOEBIUS1:62
for n being non zero Nat 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 & m is square-free holds
m divides Radical n
proof end;

theorem Th65: :: MOEBIUS1:65
for k, n being non zero Nat holds
( ( k divides n & k is square-free ) iff k divides Radical n )
proof end;

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 ) }
proof end;