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-2021 Association of Mizar Users

Lm1: for X, Y, Z, x being set st X misses Y & x in X /\ Z holds
not x in Y /\ Z
by XBOOLE_1:76, XBOOLE_0:3;

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

ex f being sequence of 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 V9() V10() V11() V15() non zero complex V20() V21() V22() non prime finite cardinal ext-real non negative V69() for Element of NAT ;

existence 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_coprime 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 m, n 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_coprime & 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 ;

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

definition

let x be Nat;

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

end;

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :

registration

cluster V9() V10() V11() V15() complex V20() V21() V22() finite cardinal ext-real non negative square-free for set ;

existence by Th22;

cluster V9() V10() V11() V15() complex V20() V21() V22() finite cardinal ext-real non negative square-containing for set ;

existence

proof end;

end;

registration

cluster non trivial V15() square -> square-containing for set ;

coherence

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 by NAT_D:9;

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;

definition

let n be Nat;

Moebius function

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

proof end;

registration

let n be square-free Nat;

cluster Moebius n -> non zero ;

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_coprime 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_coprime 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;

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

proof end;

end;

:: deftheorem defines NatDivisors MOEBIUS1:def 4 :

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

proof end;

end;

theorem Th41: :: MOEBIUS1:41

NatDivisors 1 = {1}

proof end;

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :

registration

let n be non zero Nat;

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 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_coprime 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;

definition

let n be non zero Nat;

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 Nat holds Radical n > 0

proof end;

registration

let n be non zero Nat;

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 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
by Lm3;

registration

let n be non zero Nat;

cluster Radical n -> square-free ;

coherence 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;