Grace/Cumulus/Combinatorics/MoebiusMultiplicative.g17

Open in Workbench Download source

Imports

Moebius

Declarations

Source

1-- Multiplicativity of the Möbius function: a product of coprime squarefree2-- numbers is squarefree, the prime divisors of a product are the union of3-- the prime divisors of the factors, disjoint for coprime factors, and4-- μ(a · b) = μ(a) · μ(b) whenever gcd(a, b) = 15-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.MoebiusMultiplicative11import Moebius1213theorem Squarefree.mul (a b : Nat)14  requires squarefreeA : Squarefree(a)15  requires squarefreeB : Squarefree(b)16  requires coprime : gcd(a, b) = 117  shows Squarefree(a * b)18proof19  intros q qMember qPrime square20  have qNat := nat.omega.backward with qMember21  have qDivides := divides.of_mul_left with square22  have alternatives := Prime.divides_mul with qPrime, qDivides23  cases alternatives with dividesA | dividesB24  . have notB : ¬(q ∣ b)25      intro dividesB26      have one := coprime.divisor_one with coprime, dividesA, dividesB27      exact Prime.ne_one with qPrime, one28    have coprimeQB := Prime.gcd_of_not_divides with qPrime, notB29    have characterization := coprime.mul_iff at q, q, b30    have coprimeSquare := characterization.backward with ⟨coprimeQB, coprimeQB⟩31    have coprimeSym := coprime.symmetric with coprimeSquare32    have squareDividesA := coprime.cancel_right with coprimeSym, square33    have absent := Squarefree.not_divides with squarefreeA, qPrime34    exact absent with squareDividesA35  . have notA : ¬(q ∣ a)36      intro dividesA37      have one := coprime.divisor_one with coprime, dividesA, dividesB38      exact Prime.ne_one with qPrime, one39    have coprimeQA := Prime.gcd_of_not_divides with qPrime, notA40    have characterization := coprime.mul_iff at q, q, a41    have coprimeSquare := characterization.backward with ⟨coprimeQA, coprimeQA⟩42    have coprimeSym := coprime.symmetric with coprimeSquare43    have commuted : a * b = b * a by ring44    rw commuted at square45    have squareDividesB := coprime.cancel_right with coprimeSym, square46    have absent := Squarefree.not_divides with squarefreeB, qPrime47    exact absent with squareDividesB4849theorem primeDivisors.mul (a b : Nat)50  requires nonzeroA : a ≠ 051  requires nonzeroB : b ≠ 052  shows primeDivisors(a * b) = primeDivisors(a) ∪ primeDivisors(b)53proof54  have productNonzero : a * b ≠ 055    intro zero56    have characterization := mul.eq_zero_iff at a, b57    have alternatives := characterization.forward with zero58    cases alternatives with aZero | bZero59    . exact nonzeroA with aZero60    . exact nonzeroB with bZero61  ext q62  constructor63  . intro member64    have both := primeDivisors.membership.forward with member65    have inDivisors := both.left66    have qPrime := both.right67    have qNat := divisors.natural with inDivisors68    have factor := divisors.divides with inDivisors69    have alternatives := Prime.divides_mul with qPrime, factor70    apply union2.membership.backward71    cases alternatives with dividesA | dividesB72    . left73      have below := divides.le with dividesA, nonzeroA74      have characterization := divisors.membership_le at a, q75      have inA := characterization.backward with ⟨below, dividesA⟩76      have membershipA := primeDivisors.membership at a, q77      exact membershipA.backward with ⟨inA, qPrime⟩78    . right79      have below := divides.le with dividesB, nonzeroB80      have characterization := divisors.membership_le at b, q81      have inB := characterization.backward with ⟨below, dividesB⟩82      have membershipB := primeDivisors.membership at b, q83      exact membershipB.backward with ⟨inB, qPrime⟩84  . intro member85    have alternatives := union2.membership.forward with member86    have membershipProduct := primeDivisors.membership at a * b, q87    cases alternatives with inA | inB88    . have both := primeDivisors.membership.forward with inA89      have inDivisors := both.left90      have qPrime := both.right91      have qNat := divisors.natural with inDivisors92      have factor := divisors.divides with inDivisors93      have multiple := divides.mul_left_self at a, b94      have chained := divides.transitive with factor, multiple95      have below := divides.le with chained, productNonzero96      have characterization := divisors.membership_le at a * b, q97      have inProduct := characterization.backward with ⟨below, chained⟩98      exact membershipProduct.backward with ⟨inProduct, qPrime⟩99    . have both := primeDivisors.membership.forward with inB100      have inDivisors := both.left101      have qPrime := both.right102      have qNat := divisors.natural with inDivisors103      have factor := divisors.divides with inDivisors104      have multiple := divides.mul_right_self at b, a105      have chained := divides.transitive with factor, multiple106      have below := divides.le with chained, productNonzero107      have characterization := divisors.membership_le at a * b, q108      have inProduct := characterization.backward with ⟨below, chained⟩109      exact membershipProduct.backward with ⟨inProduct, qPrime⟩110111theorem primeDivisors.disjoint (a b : Nat)112  requires coprime : gcd(a, b) = 1113  shows Disjoint(primeDivisors(a), primeDivisors(b))114proof115  apply Disjoint.iff.backward116  intros q inA inB117  have bothA := primeDivisors.membership.forward with inA118  have bothB := primeDivisors.membership.forward with inB119  have qNat := divisors.natural with bothA.left120  have qPrime := bothA.right121  have dividesA := divisors.divides with bothA.left122  have dividesB := divisors.divides with bothB.left123  have one := coprime.divisor_one with coprime, dividesA, dividesB124  exact Prime.ne_one with qPrime, one125126theorem primeDivisorCount.mul_coprime (a b : Nat)127  requires nonzeroA : a ≠ 0128  requires nonzeroB : b ≠ 0129  requires coprime : gcd(a, b) = 1130  shows primeDivisorCount(a * b) = primeDivisorCount(a) + primeDivisorCount(b)131proof132  have same := primeDivisors.mul with nonzeroA, nonzeroB133  have disjoint := primeDivisors.disjoint with coprime134  have finiteA := primeDivisors.finite at a135  have finiteB := primeDivisors.finite at b136  have count := cardinality.union_disjoint with finiteA, finiteB, disjoint137  unfold primeDivisorCount138  cc139140-- The Möbius function is multiplicative.141theorem moebius.multiplicative (a b : Nat)142  requires coprime : gcd(a, b) = 1143  shows moebius(a * b) = integerMulValue(moebius(a), moebius(b))144proof145  have aInteger := moebius.integer at a146  have bInteger := moebius.integer at b147  have alternativesA : Squarefree(a) ∨ ¬Squarefree(a) by tauto148  cases alternativesA with squarefreeA | notA149  . have alternativesB : Squarefree(b) ∨ ¬Squarefree(b) by tauto150    cases alternativesB with squarefreeB | notB151    . have nonzeroA := Squarefree.nonzero with squarefreeA152      have nonzeroB := Squarefree.nonzero with squarefreeB153      have squarefreeProduct := Squarefree.mul with squarefreeA, squarefreeB,154        coprime155      have valueA := moebius.of_squarefree with squarefreeA156      have valueB := moebius.of_squarefree with squarefreeB157      have valueProduct := moebius.of_squarefree with squarefreeProduct158      have count := primeDivisorCount.mul_coprime with nonzeroA, nonzeroB,159        coprime160      have countA := primeDivisorCount.natural at a161      have countB := primeDivisorCount.natural at b162      have split := integerPow.add at -integerOne, primeDivisorCount(a),163        primeDivisorCount(b)164      rw [valueProduct, count, split, valueA, valueB]165      rfl166    . have notProduct : ¬Squarefree(a * b)167        intro squarefreeProduct168        have multiple := divides.mul_right_self at b, a169        have squarefreeB := Squarefree.of_divides with squarefreeProduct,170          multiple171        exact notB with squarefreeB172      have valueB := moebius.of_not_squarefree with notB173      have valueProduct := moebius.of_not_squarefree with notProduct174      rw [valueProduct, valueB]175      ring176  . have notProduct : ¬Squarefree(a * b)177      intro squarefreeProduct178      have multiple := divides.mul_left_self at a, b179      have squarefreeA := Squarefree.of_divides with squarefreeProduct, multiple180      exact notA with squarefreeA181    have valueA := moebius.of_not_squarefree with notA182    have valueProduct := moebius.of_not_squarefree with notProduct183    rw [valueProduct, valueA]184    ring185