Grace/Cumulus/Combinatorics/MoebiusInversion.g17

Open in Workbench Download source

Imports

Moebius · DivisorInterchange

Declarations

Source

1-- Möbius inversion: if g(n) = ∑_{d ∣ n} f(d) for every n ≥ 1 then2-- f(n) = ∑_{d ∣ n} μ(d) · g(n / d) for every n ≥ 1, and conversely, proved3-- by interchanging the double sum over divisors and the key identity4-- ∑_{d ∣ m} μ(d) = [m = 1]5-- 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.MoebiusInversion11import Moebius12import DivisorInterchange1314-- The weight (d, e) ↦ a(d) · b(e) on pairs of naturals.15defgraph productWeights (a b : Set) (q ∈ ℕ × ℕ) : ℤ :=16  integerMulValue(a(firstProjection(ℕ, ℕ)(q)), b(secondProjection(ℕ, ℕ)(q)))17requires weightsA : a : ℕ → ℤ18requires weightsB : b : ℕ → ℤ19proof20  have firstFunction := firstProjection.function at ℕ, ℕ21  have secondFunction := secondProjection.function at ℕ, ℕ22  have firstMember := FunctionBetween.apply_closed with firstFunction, member23  have secondMember := FunctionBetween.apply_closed with secondFunction, member24  have left := FunctionBetween.apply_closed with weightsA, firstMember25  have right := FunctionBetween.apply_closed with weightsB, secondMember26  exact integerMulValue.integer at a(firstProjection(ℕ, ℕ)(q)),27    b(secondProjection(ℕ, ℕ)(q)) with *2829theorem productWeights.pair (a b d e : Set)30  requires weightsA : a : ℕ → ℤ31  requires weightsB : b : ℕ → ℤ32  requires dMember : d ∈ ℕ33  requires eMember : e ∈ ℕ34  shows productWeights(a, b)((d, e)) = integerMulValue(a(d), b(e))35proof36  have pairMember := product.pair with dMember, eMember37  have value := productWeights.value at a, b, (d, e) with weightsA, weightsB,38    pairMember39  have firstValue := firstProjection.pair at ℕ, ℕ, d, e with dMember, eMember40  have secondValue := secondProjection.pair at ℕ, ℕ, d, e with dMember, eMember41  rw [value, firstValue, secondValue]42  rfl4344-- Row d of the pairs μ(d) · f(e) sums to μ(d) · ∑_{e ∣ n/d} f(e).45theorem moebiusRow.value (f : Set) (n : Nat) (d : Set)46  requires weightsF : f : ℕ → ℤ47  requires nonzero : n ≠ 048  requires member : d ∈ divisors(n)49  shows rowDivisorSums(productWeights(moebius, f), n)(d) =50    integerMulValue(moebius(d), divisorSum(quotientNat(n, d), f))51proof52  have moebiusFunction := moebius.function53  have pairWeights := productWeights.function at moebius, f with54    moebiusFunction, weightsF55  have naturals := divisors.subset_naturals at n56  have dNat := divisors.natural with member57  have dMember := naturals with d, member58  have quotientNatural := quotientNat.natural at d, n59  have innerNaturals := divisors.subset_naturals at quotientNat(n, d)60  have rowValue := rowDivisorSums.value at productWeights(moebius, f), n, d61    with pairWeights62  have rows := rowTerms.function at productWeights(moebius, f), d with63    pairWeights, dMember64  have scaledValues : ∀ e ∈ divisors(quotientNat(n, d)),65      rowTerms(productWeights(moebius, f), d)(e) =66        integerMulValue(moebius(d), f(e))67    intros e he68    have eMember := innerNaturals with e, he69    have termValue := rowTerms.value at productWeights(moebius, f), d, e with70      pairWeights, dMember71    have pairValue := productWeights.pair at moebius, f, d, e with72      moebiusFunction, weightsF, dMember, eMember73    cc74  have dInteger := moebius.integer at d75  have scaled := divisorSum.scale at quotientNat(n, d), f,76    rowTerms(productWeights(moebius, f), d), moebius(d) with weightsF, rows,77      scaledValues78  rw [rowValue, scaled]79  rfl8081-- Column e of the pairs μ(d) · f(e) sums to f(e) · ∑_{d ∣ n/e} μ(d).82theorem moebiusColumn.value (f : Set) (n : Nat) (e : Set)83  requires weightsF : f : ℕ → ℤ84  requires nonzero : n ≠ 085  requires member : e ∈ divisors(n)86  shows columnDivisorSums(productWeights(moebius, f), n)(e) =87    integerMulValue(f(e), divisorSum(quotientNat(n, e), moebius))88proof89  have moebiusFunction := moebius.function90  have pairWeights := productWeights.function at moebius, f with91    moebiusFunction, weightsF92  have naturals := divisors.subset_naturals at n93  have eNat := divisors.natural with member94  have eMember := naturals with e, member95  have eInteger := FunctionBetween.apply_closed with weightsF, eMember96  have quotientNatural := quotientNat.natural at e, n97  have innerNaturals := divisors.subset_naturals at quotientNat(n, e)98  have columnValue := columnDivisorSums.value at productWeights(moebius, f), n,99    e with pairWeights100  have columns := columnTerms.function at productWeights(moebius, f), e with101    pairWeights, eMember102  have scaledValues : ∀ d ∈ divisors(quotientNat(n, e)),103      columnTerms(productWeights(moebius, f), e)(d) =104        integerMulValue(f(e), moebius(d))105    intros d hd106    have dMember := innerNaturals with d, hd107    have dNat := nat.omega.backward with dMember108    have dInteger := moebius.integer at d109    have termValue := columnTerms.value at productWeights(moebius, f), e, d110      with pairWeights, eMember111    have pairValue := productWeights.pair at moebius, f, d, e with112      moebiusFunction, weightsF, dMember, eMember113    rw [termValue, pairValue]114    ring115  have scaled := divisorSum.scale at quotientNat(n, e), moebius,116    columnTerms(productWeights(moebius, f), e), f(e) with moebiusFunction,117      columns, scaledValues118  rw [columnValue, scaled]119  rfl120121theorem moebiusColumn.vanishes (f : Set) (n : Nat) (e : Set)122  requires weightsF : f : ℕ → ℤ123  requires nonzero : n ≠ 0124  requires member : e ∈ divisors(n)125  requires different : e ≠ n126  shows columnDivisorSums(productWeights(moebius, f), n)(e) = integerZero127proof128  have value := moebiusColumn.value with weightsF, nonzero, member129  have eNat := divisors.natural with member130  have factor := divisors.divides with member131  have eNonzero := divides.nonzero with factor, nonzero132  have quotientNonzero := divides.quotient_ne_zero with nonzero, factor133  have quotientNatural := quotientNat.natural at e, n134  have quotientNotOne : quotientNat(n, e) ≠ 1135    intro one136    have equation := divides.quotient_equation with eNonzero, factor137    rw one at equation138    have unit := mul.right_unit at e139    have same : e = n by cc140    exact different with same141  have characterization := LessEqual.one_iff_ne_zero at quotientNat(n, e)142  have positive := characterization.backward with quotientNonzero143  have alternatives := LessEqual.cases with positive144  have aboveOne : 1 < quotientNat(n, e)145    cases alternatives with strict | same146    . exact strict147    . exfalso148      apply quotientNotOne149      symm150      exact same151  have key := moebius.sum_divisors with aboveOne152  have naturals := divisors.subset_naturals at n153  have eMember := naturals with e, member154  have eInteger := FunctionBetween.apply_closed with weightsF, eMember155  rw [value, key]156  ring157158theorem moebiusColumn.at_self (f : Set) (n : Nat)159  requires weightsF : f : ℕ → ℤ160  requires nonzero : n ≠ 0161  shows columnDivisorSums(productWeights(moebius, f), n)(n) = f(n)162proof163  have self := divisors.self_member at n164  have value := moebiusColumn.value with weightsF, nonzero, self165  have selfQuotient : quotientNat(n, n) = 1166    have unit := mul.right_unit at n167    have reduced := quotientNat.mul_left at n, 1 with nonzero168    cc169  have one := moebius.sum_one170  have nNat : Nat(n) by typecheck171  have nMember := nat.omega.forward with nNat172  have nInteger := FunctionBetween.apply_closed with weightsF, nMember173  have oneInteger := integerOne.integer174  rw [value, selfQuotient, one]175  ring176177-- Möbius inversion: g(n) = ∑_{d ∣ n} f(d) for all n ≥ 1 gives178-- f(n) = ∑_{d ∣ n} μ(d) · g(n / d) for all n ≥ 1.179theorem moebius.inversion (f g : Set)180  requires weightsF : f : ℕ → ℤ181  requires weightsG : g : ℕ → ℤ182  requires sums : ∀ n ∈ ℕ, n ≠ 0 → g(n) = divisorSum(n, f)183  shows ∀ n ∈ ℕ, n ≠ 0 → f(n) = divisorSum(n, dirichletTerms(moebius, g, n))184proof185  intros n nMember nonzero186  have nNat := nat.omega.backward with nMember187  have moebiusFunction := moebius.function188  have pairWeights := productWeights.function at moebius, f with189    moebiusFunction, weightsF190  have naturals := divisors.subset_naturals at n191  have terms := dirichletTerms.function at moebius, g, n with moebiusFunction,192    weightsG193  have rows := rowDivisorSums.function at productWeights(moebius, f), n with194    pairWeights195  have columns := columnDivisorSums.function at productWeights(moebius, f), n196    with pairWeights197  have rowsAgree : ∀ d ∈ divisors(n), dirichletTerms(moebius, g, n)(d) =198      rowDivisorSums(productWeights(moebius, f), n)(d)199    intros d hd200    have dNat := divisors.natural with hd201    have dMember := naturals with d, hd202    have factor := divisors.divides with hd203    have quotientNonzero := divides.quotient_ne_zero with nonzero, factor204    have quotientNatural := quotientNat.natural at d, n205    have quotientMember := nat.omega.forward with quotientNatural206    have termValue := dirichletTerms.value at moebius, g, n, d with207      moebiusFunction, weightsG208    have rowValue := moebiusRow.value with weightsF, nonzero, hd209    have gValue := sums with quotientNat(n, d), quotientMember, quotientNonzero210    rw [termValue, rowValue, gValue]211    rfl212  have leftSum := divisorSum.congr with terms, rows, rowsAgree213  have interchange := divisorSum.interchange at productWeights(moebius, f), n214    with nonzero, pairWeights215  have vanishing : ∀ e ∈ divisors(n), e ≠ n →216      columnDivisorSums(productWeights(moebius, f), n)(e) = integerZero217    intros e he different218    exact moebiusColumn.vanishes with weightsF, nonzero, he, different219  have single := divisorSum.single with columns, vanishing220  have atSelf := moebiusColumn.at_self with weightsF, nonzero221  rw [leftSum, interchange, single, atSelf]222  rfl223224-- Successive quotients by two divisors commute.225theorem quotientNat.swap (n d c : Nat)226  requires nonzero : n ≠ 0227  requires factor : d ∣ n228  requires inner : c ∣ quotientNat(n, d)229  shows quotientNat(quotientNat(n, d), c) = quotientNat(quotientNat(n, c), d)230proof231  have dNonzero := divides.nonzero with factor, nonzero232  have quotientNonzero := divides.quotient_ne_zero with nonzero, factor233  have cNonzero := divides.nonzero with inner, quotientNonzero234  have outerEquation := divides.quotient_equation with dNonzero, factor235  have innerEquation := divides.quotient_equation with cNonzero, inner236  have innerNatural := quotientNat.natural at c, quotientNat(n, d)237  have rearranged : d * (c * quotientNat(quotientNat(n, d), c)) =238      c * (d * quotientNat(quotientNat(n, d), c)) by ring239  have shape : n = c * (d * quotientNat(quotientNat(n, d), c)) by cc240  have outer := quotientNat.mul_left at c, d * quotientNat(quotientNat(n, d),241    c) with cNonzero242  have reduced := quotientNat.mul_left at d, quotientNat(quotientNat(n, d), c)243    with dNonzero244  cc245246-- The weight (d, c) ↦ μ(c) · g((n / d) / c): the Möbius summands at n / d.247defgraph nestedTerms (g : Set) (n : Nat) (q ∈ ℕ × ℕ) : ℤ :=248  dirichletTerms(moebius, g, quotientNat(n,249    firstProjection(ℕ, ℕ)(q)))(secondProjection(ℕ, ℕ)(q))250requires weightsG : g : ℕ → ℤ251proof252  have moebiusFunction := moebius.function253  have firstFunction := firstProjection.function at ℕ, ℕ254  have secondFunction := secondProjection.function at ℕ, ℕ255  have firstMember := FunctionBetween.apply_closed with firstFunction, member256  have secondMember := FunctionBetween.apply_closed with secondFunction, member257  have firstNat := nat.omega.backward with firstMember258  have quotientNatural := quotientNat.natural at firstProjection(ℕ, ℕ)(q), n259  have terms := dirichletTerms.function at moebius, g, quotientNat(n,260    firstProjection(ℕ, ℕ)(q)) with moebiusFunction, weightsG261  exact FunctionBetween.apply_closed with terms, secondMember262263theorem nestedTerms.pair (g : Set) (n : Nat) (d c : Set)264  requires weightsG : g : ℕ → ℤ265  requires dMember : d ∈ ℕ266  requires cMember : c ∈ ℕ267  shows nestedTerms(g, n)((d, c)) =268    dirichletTerms(moebius, g, quotientNat(n, d))(c)269proof270  have pairMember := product.pair with dMember, cMember271  have value := nestedTerms.value at g, n, (d, c) with weightsG, pairMember272  have firstValue := firstProjection.pair at ℕ, ℕ, d, c with dMember, cMember273  have secondValue := secondProjection.pair at ℕ, ℕ, d, c with dMember, cMember274  rw [value, firstValue, secondValue]275  rfl276277-- The converse: f(n) = ∑_{d ∣ n} μ(d) · g(n / d) for all n ≥ 1 gives278-- g(n) = ∑_{d ∣ n} f(d) for all n ≥ 1.279theorem moebius.inversion_converse (f g : Set)280  requires weightsF : f : ℕ → ℤ281  requires weightsG : g : ℕ → ℤ282  requires inverted : ∀ n ∈ ℕ, n ≠ 0 →283    f(n) = divisorSum(n, dirichletTerms(moebius, g, n))284  shows ∀ n ∈ ℕ, n ≠ 0 → g(n) = divisorSum(n, f)285proof286  intros n nMember nonzero287  have nNat := nat.omega.backward with nMember288  have moebiusFunction := moebius.function289  have naturals := divisors.subset_naturals at n290  have summatoryFunction := summatory.function at g with weightsG291  have sumsG : ∀ m ∈ ℕ, m ≠ 0 → summatory(g)(m) = divisorSum(m, g)292    intros m hm mNonzero293    have mNat := nat.omega.backward with hm294    exact summatory.value at g, m with weightsG295  have forward := moebius.inversion with weightsG, summatoryFunction, sumsG296  have gValue := forward with n, nMember, nonzero297  have nested := nestedTerms.function at g, n with weightsG298  have reflected := complementaryWeights.function at n, f with weightsF299  have rows := rowDivisorSums.function at nestedTerms(g, n), n with nested300  have columns := columnDivisorSums.function at nestedTerms(g, n), n with301    nested302  have convolved := dirichletTerms.function at moebius, summatory(g), n with303    moebiusFunction, summatoryFunction304  have rowsAgree : ∀ d ∈ divisors(n), complementaryWeights(n, f)(d) =305      rowDivisorSums(nestedTerms(g, n), n)(d)306    intros d hd307    have dNat := divisors.natural with hd308    have dMember := naturals with d, hd309    have factor := divisors.divides with hd310    have quotientNonzero := divides.quotient_ne_zero with nonzero, factor311    have quotientNatural := quotientNat.natural at d, n312    have quotientMember := nat.omega.forward with quotientNatural313    have innerNaturals := divisors.subset_naturals at quotientNat(n, d)314    have reflectedValue := complementaryWeights.value at n, f, d with weightsF315    have fValue := inverted with quotientNat(n, d), quotientMember,316      quotientNonzero317    have rowValue := rowDivisorSums.value at nestedTerms(g, n), n, d with318      nested319    have rowTermsFunction := rowTerms.function at nestedTerms(g, n), d with320      nested, dMember321    have innerTerms := dirichletTerms.function at moebius, g, quotientNat(n, d)322      with moebiusFunction, weightsG323    have agree : ∀ c ∈ divisors(quotientNat(n, d)),324        rowTerms(nestedTerms(g, n), d)(c) =325          dirichletTerms(moebius, g, quotientNat(n, d))(c)326      intros c hc327      have cMember := innerNaturals with c, hc328      have termValue := rowTerms.value at nestedTerms(g, n), d, c with nested,329        dMember330      have pairValue := nestedTerms.pair at g, n, d, c with weightsG, dMember,331        cMember332      cc333    have same := divisorSum.congr at quotientNat(n, d),334      rowTerms(nestedTerms(g, n), d), dirichletTerms(moebius, g,335        quotientNat(n, d)) with rowTermsFunction, innerTerms, agree336    rw [reflectedValue, fValue, rowValue, same]337    rfl338  have leftSum := divisorSum.congr with reflected, rows, rowsAgree339  have reflect := divisorSum.reflect with nonzero, weightsF340  have interchange := divisorSum.interchange at nestedTerms(g, n), n with341    nonzero, nested342  have columnsAgree : ∀ c ∈ divisors(n),343      columnDivisorSums(nestedTerms(g, n), n)(c) =344        dirichletTerms(moebius, summatory(g), n)(c)345    intros c hc346    have cNat := divisors.natural with hc347    have cMember := naturals with c, hc348    have cFactor := divisors.divides with hc349    have cQuotientNonzero := divides.quotient_ne_zero with nonzero, cFactor350    have cQuotientNatural := quotientNat.natural at c, n351    have innerC := divisors.quotient_subset with nonzero, cFactor352    have columnValue := columnDivisorSums.value at nestedTerms(g, n), n, c353      with nested354    have columnTermsFunction := columnTerms.function at nestedTerms(g, n), c355      with nested, cMember356    have reflectedG := complementaryWeights.function at quotientNat(n, c), g357      with weightsG358    have cInteger := moebius.integer at c359    have scaledValues : ∀ d ∈ divisors(quotientNat(n, c)),360        columnTerms(nestedTerms(g, n), c)(d) = integerMulValue(moebius(c),361          complementaryWeights(quotientNat(n, c), g)(d))362      intros d hd363      have dInN := innerC with d, hd364      have dNat := divisors.natural with dInN365      have dMember := naturals with d, dInN366      have dFactor := divisors.divides with dInN367      have dQuotientNatural := quotientNat.natural at d, n368      have termValue := columnTerms.value at nestedTerms(g, n), c, d with369        nested, cMember370      have pairValue := nestedTerms.pair at g, n, d, c with weightsG, dMember,371        cMember372      have innerValue := dirichletTerms.value at moebius, g, quotientNat(n, d),373        c with moebiusFunction, weightsG374      have reflectedValue := complementaryWeights.value at quotientNat(n, c),375        g, d with weightsG376      have dDividesQuotient := divisors.divides with hd377      have characterizationC := divides.mul_iff_quotient at c, d, n with378        nonzero, cFactor379      have product := characterizationC.backward with dDividesQuotient380      have commuted := mul.commutative at c, d381      rw ← commuted at product382      have characterizationD := divides.mul_iff_quotient at d, c, n with383        nonzero, dFactor384      have cDividesQuotient := characterizationD.forward with product385      have swapped := quotientNat.swap with nonzero, dFactor, cDividesQuotient386      rw [termValue, pairValue, innerValue, reflectedValue, swapped]387      rfl388    have scaled := divisorSum.scale at quotientNat(n, c),389      complementaryWeights(quotientNat(n, c), g),390        columnTerms(nestedTerms(g, n), c), moebius(c) with reflectedG,391          columnTermsFunction, scaledValues392    have reflectG := divisorSum.reflect at quotientNat(n, c), g with393      cQuotientNonzero, weightsG394    have summatoryValue := summatory.value at g, quotientNat(n, c) with395      weightsG396    have convolvedValue := dirichletTerms.value at moebius, summatory(g), n, c397      with moebiusFunction, summatoryFunction398    rw [columnValue, scaled, reflectG, convolvedValue, summatoryValue]399    rfl400  have rightSum := divisorSum.congr with columns, convolved, columnsAgree401  rw [← reflect, leftSum, interchange, rightSum]402  exact gValue403