Grace/Cumulus/Combinatorics/Moebius.g17

Open in Workbench Download source

Imports

DivisorSums · Basics

Declarations

Source

1-- The Möbius function: squarefree numbers, the set and number of prime2-- divisors, μ(n) = (−1)^k at a squarefree n with k prime divisors and 03-- elsewhere, its values at 1, primes, prime squares, and products of two4-- distinct primes, the step μ(p · d) = −μ(d) for a prime p not dividing d,5-- and the key identity ∑_{d ∣ n} μ(d) = 0 for n > 1, proved by pairing each6-- squarefree divisor d with d / p or p · d for a fixed prime p dividing n7-- Part of Cumulus, the Grace17 mathematics library.8-- Copyright (c) 2026 Grant Passmore.9-- Released under the Apache License 2.0. See LICENSE in the repository root.10-- Authors: Grant Passmore1112module Grace.Cumulus.Combinatorics.Moebius13import DivisorSums14import Basics1516-- A natural number is squarefree when no prime square divides it.17predicate Squarefree (n : Nat) := ∀ p ∈ ℕ, Prime(p) → ¬(p * p ∣ n)1819theorem Squarefree.not_divides (n p : Nat)20  requires squarefree : Squarefree(n)21  requires prime : Prime(p)22  shows ¬(p * p ∣ n)23proof24  have pNat : Nat(p) by typecheck25  have pMember := nat.omega.forward with pNat26  exact squarefree with p, pMember, prime2728theorem Squarefree.of_divides (m n : Nat)29  requires squarefree : Squarefree(n)30  requires factor : m ∣ n31  shows Squarefree(m)32proof33  intros p pMember prime square34  have pNat := nat.omega.backward with pMember35  have chained := divides.transitive with square, factor36  have absent := Squarefree.not_divides with squarefree, prime37  exact absent with chained3839theorem Squarefree.nonzero (n : Nat)40  requires squarefree : Squarefree(n)41  shows n ≠ 042proof43  intro zero44  have two := Prime.two45  have four := divides.zero at 2 * 246  rw zero at squarefree47  have absent := Squarefree.not_divides with squarefree, two48  exact absent with four4950theorem Squarefree.one51  shows Squarefree(1)52proof53  intros p pMember prime square54  have pNat := nat.omega.backward with pMember55  have pDivides := divides.of_mul_left with square56  have pOne := divides.one_only at p with pNat, pDivides57  exact Prime.ne_one with prime, pOne5859theorem Squarefree.prime (p : Nat)60  requires prime : Prime(p)61  shows Squarefree(p)62proof63  intros q qMember qPrime square64  have qNat := nat.omega.backward with qMember65  have qDivides := divides.of_mul_left with square66  have same := Prime.divides_prime with qPrime, prime, qDivides67  rw same at square68  have nonzero := Prime.nonzero with prime69  have unit : p * p ∣ p * 170    have shape : p * 1 = p by ring71    rw shape72    exact square73  have cancel := divides.mul_cancel_left at p, p, 1 with nonzero74  have pDividesOne := cancel.forward with unit75  have pOne := divides.one_only at p with *76  exact Prime.ne_one with prime, pOne7778theorem Squarefree.not_prime_square (p : Nat)79  requires prime : Prime(p)80  shows ¬Squarefree(p * p)81proof82  intro squarefree83  have self := divides.reflexive at p * p84  have absent := Squarefree.not_divides with squarefree, prime85  exact absent with self8687-- A prime not dividing a squarefree number keeps the product squarefree.88theorem Squarefree.mul_prime (d p : Nat)89  requires squarefree : Squarefree(d)90  requires prime : Prime(p)91  requires notDivides : ¬(p ∣ d)92  shows Squarefree(p * d)93proof94  intros q qMember qPrime square95  have qNat := nat.omega.backward with qMember96  have alternatives : q = p ∨ q ≠ p by tauto97  cases alternatives with same | different98  . rw same at square99    have nonzero := Prime.nonzero with prime100    have cancel := divides.mul_cancel_left at p, p, d with nonzero101    have pDivides := cancel.forward with square102    exact notDivides with pDivides103  . have qNotDividesP : ¬(q ∣ p)104      intro qDivides105      have equal := Prime.divides_prime with qPrime, prime, qDivides106      exact different with equal107    have coprimeQP := Prime.gcd_of_not_divides with qPrime, qNotDividesP108    have characterization := coprime.mul_iff at q, q, p109    have coprimeSquare := characterization.backward with ⟨coprimeQP, coprimeQP⟩110    have coprimeSym := coprime.symmetric with coprimeSquare111    have commuted : p * d = d * p by ring112    rw commuted at square113    have dividesD := coprime.cancel_right with coprimeSym, square114    have absent := Squarefree.not_divides with squarefree, qPrime115    exact absent with dividesD116117-- Dividing a squarefree number by a prime factor removes that prime.118theorem Squarefree.quotient_not_divides (d p : Nat)119  requires squarefree : Squarefree(d)120  requires prime : Prime(p)121  requires factor : p ∣ d122  shows ¬(p ∣ quotientNat(d, p))123proof124  intro again125  have pNonzero := Prime.nonzero with prime126  have equation := divides.quotient_equation with pNonzero, factor127  have self := divides.reflexive at p128  have square := divides.mul_mono with self, again129  rw ← equation at square130  have absent := Squarefree.not_divides with squarefree, prime131  exact absent with square132133-- The prime divisors of n and their number.134def primeDivisors (n : Nat) : Set := { p ∈ divisors(n) | Prime(p) }135136theorem primeDivisors.subset (n : Nat)137  shows primeDivisors(n) ⊆ divisors(n)138proof139  intros p member140  have both := primeDivisors.membership.forward with member141  exact both.left142143theorem primeDivisors.finite (n : Nat)144  shows Finite(primeDivisors(n))145proof146  have finite := divisors.finite at n147  have subset := primeDivisors.subset at n148  exact Finite.subset with finite, subset149150theorem primeDivisors.one151  shows primeDivisors(1) = ∅152proof153  ext x154  constructor155  . intro member156    have both := primeDivisors.membership.forward with member157    have inOne := both.left158    have prime := both.right159    rw divisors.one at inOne160    have xOne := singleton.membership.forward with inOne161    rw xOne at prime162    have distinct := Prime.ne_one at 1 with prime163    exfalso164    apply distinct165    rfl166  . intro member167    exfalso168    have absent := set.empty at x169    exact absent with member170171theorem primeDivisors.prime (p : Nat)172  requires prime : Prime(p)173  shows primeDivisors(p) = {p}174proof175  have same := divisors.prime with prime176  ext x177  constructor178  . intro member179    have both := primeDivisors.membership.forward with member180    have inDivisors := both.left181    have xPrime := both.right182    rw same at inDivisors183    have alternatives := pair.membership.forward with inDivisors184    cases alternatives with one | self185    . exfalso186      rw one at xPrime187      have distinct := Prime.ne_one at 1 with xPrime188      apply distinct189      rfl190    . rw self191      simp192  . intro member193    have xP := singleton.membership.forward with member194    rw xP195    have self := divisors.self_member at p196    exact primeDivisors.membership.backward with ⟨self, prime⟩197198theorem primeDivisors.mul_prime (d p : Nat)199  requires nonzero : d ≠ 0200  requires prime : Prime(p)201  shows primeDivisors(p * d) = insert(p, primeDivisors(d))202proof203  have pNonzero := Prime.nonzero with prime204  have productNonzero : p * d ≠ 0205    intro zero206    have characterization := mul.eq_zero_iff at p, d207    have alternatives := characterization.forward with zero208    cases alternatives with pZero | dZero209    . exact pNonzero with pZero210    . exact nonzero with dZero211  ext q212  constructor213  . intro member214    have both := primeDivisors.membership.forward with member215    have inDivisors := both.left216    have qPrime := both.right217    have qNat := divisors.natural with inDivisors218    have factor := divisors.divides with inDivisors219    have alternatives := Prime.divides_mul with qPrime, factor220    cases alternatives with dividesP | dividesD221    . have same := Prime.divides_prime with qPrime, prime, dividesP222      rw same223      simp224    . have below := divides.le with dividesD, nonzero225      have characterization := divisors.membership_le at d, q226      have inD := characterization.backward with ⟨below, dividesD⟩227      have characterizationD := primeDivisors.membership at d, q228      have inPrime := characterizationD.backward with ⟨inD, qPrime⟩229      simp230  . intro member231    have alternatives := insert.membership.forward with member232    cases alternatives with same | inD233    . rw same234      have self := divides.mul_left_self at p, d235      have below := divides.le with self, productNonzero236      have characterization := divisors.membership_le at p * d, p237      have inDivisors := characterization.backward with ⟨below, self⟩238      exact primeDivisors.membership.backward with ⟨inDivisors, prime⟩239    . have both := primeDivisors.membership.forward with inD240      have inDivisorsD := both.left241      have qPrime := both.right242      have qNat := divisors.natural with inDivisorsD243      have factor := divisors.divides with inDivisorsD244      have multiple := divides.mul_right_self at d, p245      have chained := divides.transitive with factor, multiple246      have below := divides.le with chained, productNonzero247      have characterization := divisors.membership_le at p * d, q248      have inDivisors := characterization.backward with ⟨below, chained⟩249      exact primeDivisors.membership.backward with ⟨inDivisors, qPrime⟩250251def primeDivisorCount (n : Nat) : Set := cardinality(primeDivisors(n))252253theorem primeDivisorCount.natural (n : Nat)254  shows Nat(primeDivisorCount(n))255proof256  have finite := primeDivisors.finite at n257  have natural := cardinality.nat with finite258  unfold primeDivisorCount259  exact natural260261theorem primeDivisorCount.one262  shows primeDivisorCount(1) = 0263proof264  have same := primeDivisors.one265  have empty := cardinality.empty266  unfold primeDivisorCount267  cc268269theorem primeDivisorCount.prime (p : Nat)270  requires prime : Prime(p)271  shows primeDivisorCount(p) = 1272proof273  have same := primeDivisors.prime with prime274  have single := cardinality.singleton at p275  unfold primeDivisorCount276  cc277278theorem primeDivisorCount.mul_prime (d p : Nat)279  requires nonzero : d ≠ 0280  requires prime : Prime(p)281  requires notDivides : ¬(p ∣ d)282  shows primeDivisorCount(p * d) = primeDivisorCount(d) + 1283proof284  have same := primeDivisors.mul_prime with nonzero, prime285  have finite := primeDivisors.finite at d286  have fresh : ¬(p ∈ primeDivisors(d))287    intro member288    have both := primeDivisors.membership.forward with member289    have factor := divisors.divides with both.left290    exact notDivides with factor291  have count := cardinality.insert_add_one with finite, fresh292  unfold primeDivisorCount293  cc294295-- The squarefree numbers, so that the Möbius function has an indicator.296def squarefreeNumbers : Set := { n ∈ ℕ | Squarefree(n) }297298-- The Möbius function: (−1)^k at a squarefree number with k prime299-- divisors, and 0 at every number with a repeated prime factor.300def moebiusValue (n : Nat) : Set :=301  integerOfNat(indicator(squarefreeNumbers, n)) *302    integerPow(-integerOne, primeDivisorCount(n))303304theorem moebiusValue.integer (n : Nat)305  shows Integer(moebiusValue(n))306proof307  have countNat := primeDivisorCount.natural at n308  have indicatorNat := indicator.natural at squarefreeNumbers, n309  have mask := integerOfNat.integer at indicator(squarefreeNumbers, n)310  have sign := integerPow.integer at -integerOne, primeDivisorCount(n)311  unfold moebiusValue312  exact integerMulValue.integer at integerOfNat(indicator(squarefreeNumbers,313    n)), integerPow(-integerOne, primeDivisorCount(n)) with *314315defgraph moebius (n ∈ ℕ) : ℤ := moebiusValue(n)316proof317  have nNat := nat.omega.backward with member318  exact moebiusValue.integer at n319320theorem moebius.integer (n : Nat)321  shows Integer(moebius(n))322proof323  have nNat : Nat(n) by typecheck324  have nMember := nat.omega.forward with nNat325  have function := moebius.function326  exact FunctionBetween.apply_closed with function, nMember327328theorem moebius.of_squarefree (n : Nat)329  requires squarefree : Squarefree(n)330  shows moebius(n) = integerPow(-integerOne, primeDivisorCount(n))331proof332  have nNat : Nat(n) by typecheck333  have nMember := nat.omega.forward with nNat334  have countNat := primeDivisorCount.natural at n335  have sign := integerPow.integer at -integerOne, primeDivisorCount(n)336  have characterization := squarefreeNumbers.membership at n337  have inSet := characterization.backward with ⟨nMember, squarefree⟩338  have one := indicator.member with inSet339  have value := moebius.value at n340  rw value341  simp [moebiusValue]342  rw integerOfNat.one343  ring344345theorem moebius.of_not_squarefree (n : Nat)346  requires notSquarefree : ¬Squarefree(n)347  shows moebius(n) = integerZero348proof349  have nNat : Nat(n) by typecheck350  have countNat := primeDivisorCount.natural at n351  have sign := integerPow.integer at -integerOne, primeDivisorCount(n)352  have absent : ¬(n ∈ squarefreeNumbers)353    intro inSet354    have both := squarefreeNumbers.membership.forward with inSet355    exact notSquarefree with both.right356  have zero := indicator.absent with absent357  have value := moebius.value at n358  rw value359  simp [moebiusValue]360  rw integerOfNat.zero361  ring362363theorem moebius.one364  shows moebius(1) = integerOne365proof366  have squarefree := Squarefree.one367  have value := moebius.of_squarefree with squarefree368  have count := primeDivisorCount.one369  rw [value, count, integerPow.zero]370  rfl371372theorem moebius.prime (p : Nat)373  requires prime : Prime(p)374  shows moebius(p) = -integerOne375proof376  have squarefree := Squarefree.prime with prime377  have value := moebius.of_squarefree with squarefree378  have count := primeDivisorCount.prime with prime379  rw [value, count, integerPow.one_right]380  rfl381382theorem moebius.prime_square (p : Nat)383  requires prime : Prime(p)384  shows moebius(p * p) = integerZero385proof386  have notSquarefree := Squarefree.not_prime_square with prime387  exact moebius.of_not_squarefree with notSquarefree388389-- Multiplying by a new prime flips the sign of the Möbius function.390theorem moebius.mul_prime (d p : Nat)391  requires prime : Prime(p)392  requires notDivides : ¬(p ∣ d)393  shows moebius(p * d) = -moebius(d)394proof395  have dInteger := moebius.integer at d396  have alternatives : Squarefree(d) ∨ ¬Squarefree(d) by tauto397  cases alternatives with squarefree | notSquarefree398  . have nonzero := Squarefree.nonzero with squarefree399    have productSquarefree := Squarefree.mul_prime with squarefree, prime,400      notDivides401    have valueD := moebius.of_squarefree with squarefree402    have valueProduct := moebius.of_squarefree with productSquarefree403    have count := primeDivisorCount.mul_prime with nonzero, prime, notDivides404    have countNat := primeDivisorCount.natural at d405    have sign := integerPow.integer at -integerOne, primeDivisorCount(d)406    rw [valueProduct, count, integerPow.add_one, valueD]407    ring408  . have productNotSquarefree : ¬Squarefree(p * d)409      intro productSquarefree410      have multiple := divides.mul_right_self at d, p411      have squarefree := Squarefree.of_divides with productSquarefree, multiple412      exact notSquarefree with squarefree413    have valueD := moebius.of_not_squarefree with notSquarefree414    have valueProduct := moebius.of_not_squarefree with productNotSquarefree415    rw [valueProduct, valueD]416    ring417418theorem moebius.prime_product (p q : Nat)419  requires primeP : Prime(p)420  requires primeQ : Prime(q)421  requires distinct : p ≠ q422  shows moebius(p * q) = integerOne423proof424  have notDivides : ¬(p ∣ q)425    intro factor426    have same := Prime.divides_prime with primeP, primeQ, factor427    exact distinct with same428  have flipped := moebius.mul_prime with primeP, notDivides429  have valueQ := moebius.prime with primeQ430  have oneInteger := integerOne.integer431  rw [flipped, valueQ]432  ring433434-- The squarefree divisors of n, the support of μ on divisors(n).435def squarefreeDivisors (n : Nat) : Set := { d ∈ divisors(n) | Squarefree(d) }436437theorem squarefreeDivisors.subset (n : Nat)438  shows squarefreeDivisors(n) ⊆ divisors(n)439proof440  intros d member441  have both := squarefreeDivisors.membership.forward with member442  exact both.left443444theorem squarefreeDivisors.quotient_member (n p d : Nat)445  requires nonzero : n ≠ 0446  requires member : d ∈ squarefreeDivisors(n)447  requires factor : p ∣ d448  shows quotientNat(d, p) ∈ squarefreeDivisors(n)449proof450  have both := squarefreeDivisors.membership.forward with member451  have inDivisors := both.left452  have squarefree := both.right453  have dDivides := divisors.divides with inDivisors454  have dNonzero := divides.nonzero with dDivides, nonzero455  have pNonzero := divides.nonzero with factor, dNonzero456  have quotientDivides := divides.quotient with pNonzero, factor457  have chained := divides.transitive with quotientDivides, dDivides458  have below := divides.le with chained, nonzero459  have characterization := divisors.membership_le at n, quotientNat(d, p)460  have inN := characterization.backward with ⟨below, chained⟩461  have quotientSquarefree := Squarefree.of_divides with squarefree,462    quotientDivides463  exact squarefreeDivisors.membership.backward with ⟨inN, quotientSquarefree⟩464465theorem squarefreeDivisors.mul_member (n p d : Nat)466  requires nonzero : n ≠ 0467  requires prime : Prime(p)468  requires pDivides : p ∣ n469  requires member : d ∈ squarefreeDivisors(n)470  requires notDivides : ¬(p ∣ d)471  shows d * p ∈ squarefreeDivisors(n)472proof473  have both := squarefreeDivisors.membership.forward with member474  have inDivisors := both.left475  have squarefree := both.right476  have dDivides := divisors.divides with inDivisors477  have coprimePD := Prime.gcd_of_not_divides with prime, notDivides478  have coprimeDP := coprime.symmetric with coprimePD479  have productDivides := coprime.mul_divides with coprimeDP, dDivides, pDivides480  have below := divides.le with productDivides, nonzero481  have characterization := divisors.membership_le at n, d * p482  have inN := characterization.backward with ⟨below, productDivides⟩483  have productSquarefree := Squarefree.mul_prime with squarefree, prime,484    notDivides485  have commuted : d * p = p * d by ring486  rw commuted487  rw commuted at inN488  exact squarefreeDivisors.membership.backward with ⟨inN, productSquarefree⟩489490-- The partner of d under p: d / p when p divides d, and d · p otherwise.491def moebiusPartnerValue (p d : Nat) : Nat :=492  chooseNat(equalNat(d % p, 0), quotientNat(d, p), d * p)493494theorem moebiusPartnerValue.of_divides (p d : Nat)495  requires factor : p ∣ d496  shows moebiusPartnerValue(p, d) = quotientNat(d, p)497proof498  have characterization := divides.iff_mod_zero at p, d499  have modZero := characterization.forward with factor500  have flag := equalNat.true_iff.backward with modZero501  clear modZero502  unfold moebiusPartnerValue503  simp [chooseNat, flag]504505theorem moebiusPartnerValue.of_not_divides (p d : Nat)506  requires notDivides : ¬(p ∣ d)507  shows moebiusPartnerValue(p, d) = d * p508proof509  have characterization := divides.iff_mod_zero at p, d510  have modNonzero : d % p ≠ 0511    intro modZero512    apply notDivides513    exact characterization.backward with modZero514  have flag := equalNat.false_iff.backward with modNonzero515  unfold moebiusPartnerValue516  simp [chooseNat, flag]517518-- Pairing the squarefree divisors of n through a prime p dividing n.519defgraph moebiusPartner (n p : Nat) (d ∈ squarefreeDivisors(n)) :520    squarefreeDivisors(n) := moebiusPartnerValue(p, d)521requires nonzero : n ≠ 0522requires prime : Prime(p)523requires factor : p ∣ n524proof525  have both := squarefreeDivisors.membership.forward with member526  have dNat := divisors.natural with both.left527  have alternatives : p ∣ d ∨ ¬(p ∣ d) by tauto528  cases alternatives with divides | notDivides529  . have value := moebiusPartnerValue.of_divides with divides530    rw value531    exact squarefreeDivisors.quotient_member with nonzero, member, divides532  . have value := moebiusPartnerValue.of_not_divides with notDivides533    rw value534    exact squarefreeDivisors.mul_member with nonzero, prime, factor, member,535      notDivides536537theorem moebiusPartner.involution (n p : Nat)538  requires nonzero : n ≠ 0539  requires prime : Prime(p)540  requires factor : p ∣ n541  shows InvolutionOn(moebiusPartner(n, p), squarefreeDivisors(n))542proof543  have function := moebiusPartner.function at n, p with nonzero, prime, factor544  refine ⟨function, _⟩545  intros d hd546  have both := squarefreeDivisors.membership.forward with hd547  have dNat := divisors.natural with both.left548  have squarefree := both.right549  have pNonzero := Prime.nonzero with prime550  have first := moebiusPartner.value at n, p, d with nonzero, prime, factor, hd551  have alternatives : p ∣ d ∨ ¬(p ∣ d) by tauto552  cases alternatives with divides | notDivides553  . have quotientValue := moebiusPartnerValue.of_divides with divides554    have quotientMember := squarefreeDivisors.quotient_member with nonzero,555      hd, divides556    have second := moebiusPartner.value at n, p, quotientNat(d, p) with557      nonzero, prime, factor, quotientMember558    have notAgain := Squarefree.quotient_not_divides with squarefree, prime,559      divides560    have productValue := moebiusPartnerValue.of_not_divides with notAgain561    have equation := divides.quotient_equation with pNonzero, divides562    have quotientNatural := quotientNat.natural at p, d563    have commuted := mul.commutative at p, quotientNat(d, p)564    rw [first, quotientValue, second, productValue]565    cc566  . have productValue := moebiusPartnerValue.of_not_divides with notDivides567    have productMember := squarefreeDivisors.mul_member with nonzero, prime,568      factor, hd, notDivides569    have second := moebiusPartner.value at n, p, d * p with nonzero, prime,570      factor, productMember571    have pDividesProduct := divides.mul_right_self at p, d572    have quotientValue := moebiusPartnerValue.of_divides with pDividesProduct573    have reduced : quotientNat(d * p, p) = d574      have commuted := mul.commutative at p, d575      rw commuted576      exact quotientNat.mul_left with pNonzero577    rw [first, productValue, second, quotientValue, reduced]578    rfl579580theorem moebius.partner (n p : Nat) (d : Set)581  requires nonzero : n ≠ 0582  requires prime : Prime(p)583  requires factor : p ∣ n584  requires member : d ∈ squarefreeDivisors(n)585  shows moebius(moebiusPartner(n, p)(d)) = -moebius(d)586proof587  have both := squarefreeDivisors.membership.forward with member588  have dNat := divisors.natural with both.left589  have squarefree := both.right590  have pNonzero := Prime.nonzero with prime591  have value := moebiusPartner.value at n, p, d with nonzero, prime, factor,592    member593  have alternatives : p ∣ d ∨ ¬(p ∣ d) by tauto594  cases alternatives with divides | notDivides595  . have quotientValue := moebiusPartnerValue.of_divides with divides596    have notAgain := Squarefree.quotient_not_divides with squarefree, prime,597      divides598    have equation := divides.quotient_equation with pNonzero, divides599    have flipped := moebius.mul_prime at quotientNat(d, p), p with prime,600      notAgain601    rw ← equation at flipped602    have quotientInteger := moebius.integer at quotientNat(d, p)603    rw [value, quotientValue, flipped, integerNegValue.involutive]604    rfl605  . have productValue := moebiusPartnerValue.of_not_divides with notDivides606    have flipped := moebius.mul_prime with prime, notDivides607    have commuted := mul.commutative at p, d608    rw [value, productValue, commuted, flipped]609    rfl610611-- The negated weight d ↦ −w(d).612defgraph negatedWeights (w : Set) (d ∈ ℕ) : ℤ := integerNegValue(w(d))613requires weights : w : ℕ → ℤ614proof615  have value := FunctionBetween.apply_closed with weights, member616  exact integerNegValue.integer at w(d) with *617618theorem integerAddValue.self_eq_zero (x : Integer)619  requires doubled : x + x = integerZero620  shows x = integerZero621proof622  have zeroInteger := integerZero.integer623  have collapse : integerZero + integerZero = integerZero by ring624  have alternatives := integerLess.trichotomy at x, integerZero625  rcases alternatives with negative | zero | positive626  . exfalso627    have sum := integerLess.add with negative, negative628    rw [doubled, collapse] at sum629    exact integerLess.irreflexive at integerZero with sum630  . exact zero631  . exfalso632    have sum := integerLess.add with positive, positive633    rw [doubled, collapse] at sum634    exact integerLess.irreflexive at integerZero with sum635636theorem moebius.sum_one637  shows divisorSum(1, moebius) = integerOne638proof639  have function := moebius.function640  have one := divisorSum.one with function641  rw [one, moebius.one]642  rfl643644-- The key identity: the Möbius function sums to zero over the divisors of645-- any n > 1.646theorem moebius.sum_divisors (n : Nat)647  requires aboveOne : 1 < n648  shows divisorSum(n, moebius) = integerZero649proof650  have nonzero : n ≠ 0651    intro zero652    rw zero at aboveOne653    arith654  obtain ⟨p, prime, factor⟩ := natural.exists_prime_divisor with aboveOne655  have pNat := Prime.natural with prime656  have function := moebius.function657  have negatedFunction := negatedWeights.function at moebius with function658  have inner := squarefreeDivisors.subset at n659  have finiteDivisors := divisors.finite at n660  have finite := Finite.subset with finiteDivisors, inner661  have naturals := divisors.subset_naturals at n662  have subset := Subset.transitive with inner, naturals663  have vanishes : ∀ d ∈ divisors(n), ¬(d ∈ squarefreeDivisors(n)) →664      moebius(d) = integerZero665    intros d hd absent666    have dNat := divisors.natural with hd667    have notSquarefree : ¬Squarefree(d)668      intro squarefree669      apply absent670      exact squarefreeDivisors.membership.backward with ⟨hd, squarefree⟩671    exact moebius.of_not_squarefree with notSquarefree672  have restricted := divisorSum.support with function, inner, vanishes673  have involution := moebiusPartner.involution with nonzero, prime, factor674  have bijective := InvolutionOn.bijective with involution675  have partnerFunction := InvolutionOn.function with involution676  have values : ∀ d ∈ squarefreeDivisors(n),677      moebius(d) = negatedWeights(moebius)(moebiusPartner(n, p)(d))678    intros d hd679    have image := FunctionBetween.apply_closed with partnerFunction, hd680    have imageMember := subset with moebiusPartner(n, p)(d), image681    have negValue := negatedWeights.value at moebius, moebiusPartner(n, p)(d)682      with function683    have flipped := moebius.partner with nonzero, prime, factor, hd684    have dMember := subset with d, hd685    have dInteger := FunctionBetween.apply_closed with function, dMember686    rw [negValue, flipped, integerNegValue.involutive]687    rfl688  have reindexed := integerSetSum.reindex at squarefreeDivisors(n),689    squarefreeDivisors(n), ℕ, ℕ, moebius, negatedWeights(moebius),690      moebiusPartner(n, p) with finite, function, negatedFunction, subset,691        subset, bijective, values692  have scaledValues : ∀ d ∈ squarefreeDivisors(n),693      negatedWeights(moebius)(d) = integerMulValue(-integerOne, moebius(d))694    intros d hd695    have dMember := subset with d, hd696    have dInteger := FunctionBetween.apply_closed with function, dMember697    have negValue := negatedWeights.value at moebius, d with function698    rw negValue699    ring700  have scaled := integerSetSum.scale at squarefreeDivisors(n), ℕ, moebius,701    negatedWeights(moebius), -integerOne with finite, function,702      negatedFunction, subset, scaledValues703  have total := integerSetSum.integer with finite, function, subset704  have fixed : integerSetSum(squarefreeDivisors(n), moebius) =705      integerMulValue(-integerOne, integerSetSum(squarefreeDivisors(n),706        moebius)) by cc707  have cancel : integerSetSum(squarefreeDivisors(n), moebius) +708      integerMulValue(-integerOne, integerSetSum(squarefreeDivisors(n),709        moebius)) = integerZero by ring710  have doubled : integerSetSum(squarefreeDivisors(n), moebius) +711      integerSetSum(squarefreeDivisors(n), moebius) = integerZero712    rw ← fixed at cancel713    exact cancel714  have zero := integerAddValue.self_eq_zero with doubled715  rw restricted716  exact zero717