Grace/Cumulus/Combinatorics/DivisorSums.g17

Open in Workbench Download source

Imports

IntegerSum · NumberTheory

Declarations

Source

1-- Sums over the divisors of a natural number: ∑_{d ∣ n} w(d) for an2-- integer-valued weight w, its value at n = 1, congruence, scaling,3-- vanishing, restriction to a support, the complementary divisor d ↦ n / d4-- as an involution of divisors(n) with the reflection of a divisor sum along5-- it, the Dirichlet summands a(d) · b(n / d), and the summatory function6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Combinatorics.DivisorSums12import IntegerSum13import NumberTheory1415-- Arithmetic of the quotient of a number by one of its divisors.16theorem divides.quotient_ne_zero (d n : Nat)17  requires nonzero : n ≠ 018  requires factor : d ∣ n19  shows quotientNat(n, d) ≠ 020proof21  have dNonzero := divides.nonzero with factor, nonzero22  have equation := divides.quotient_equation with dNonzero, factor23  intro zero24  rw zero at equation25  have product : d * 0 = 0 by ring26  have same : n = 0 by cc27  exact nonzero with same2829theorem quotientNat.mul_left (a b : Nat)30  requires nonzero : a ≠ 031  shows quotientNat(a * b, a) = b32proof33  have factor := divides.mul_left_self at a, b34  have equation := divides.quotient_equation with nonzero, factor35  symm36  exact mul.left_cancel_positive with nonzero, equation3738theorem quotientNat.complement (d n : Nat)39  requires nonzero : n ≠ 040  requires factor : d ∣ n41  shows quotientNat(n, quotientNat(n, d)) = d42proof43  have dNonzero := divides.nonzero with factor, nonzero44  have equation := divides.quotient_equation with dNonzero, factor45  have quotientNonzero := divides.quotient_ne_zero with nonzero, factor46  have commuted := mul.commutative at d, quotientNat(n, d)47  have shape : n = quotientNat(n, d) * d by cc48  have reduced := quotientNat.mul_left at quotientNat(n, d), d with49    quotientNonzero50  cc5152theorem divides.mul_iff_quotient (d e n : Nat)53  requires nonzero : n ≠ 054  requires factor : d ∣ n55  shows d * e ∣ n ↔ e ∣ quotientNat(n, d)56proof57  have dNonzero := divides.nonzero with factor, nonzero58  have equation := divides.quotient_equation with dNonzero, factor59  have cancel := divides.mul_cancel_left at d, e, quotientNat(n, d) with60    dNonzero61  rw ← equation at cancel62  exact cancel6364theorem divisors.quotient_member (n d : Nat)65  requires nonzero : n ≠ 066  requires member : d ∈ divisors(n)67  shows quotientNat(n, d) ∈ divisors(n)68proof69  have factor := divisors.divides with member70  have dNonzero := divides.nonzero with factor, nonzero71  have quotientDivides := divides.quotient with dNonzero, factor72  have below := divides.le with quotientDivides, nonzero73  have characterization := divisors.membership_le at n, quotientNat(n, d)74  exact characterization.backward with ⟨below, quotientDivides⟩7576theorem divisors.quotient_subset (n d : Nat)77  requires nonzero : n ≠ 078  requires factor : d ∣ n79  shows divisors(quotientNat(n, d)) ⊆ divisors(n)80proof81  have dNonzero := divides.nonzero with factor, nonzero82  have quotientDivides := divides.quotient with dNonzero, factor83  exact divisors.subset_of_divides with nonzero, quotientDivides8485-- The sum ∑_{d ∣ n} w(d) of an integer-valued weight over the divisors of n.86def divisorSum (n : Nat, w : Set) : Set := integerSetSum(divisors(n), w)8788theorem divisorSum.integer (n : Nat, w : Set)89  requires weights : w : ℕ → ℤ90  shows Integer(divisorSum(n, w))91proof92  have finite := divisors.finite at n93  have subset := divisors.subset_naturals at n94  have total := integerSetSum.integer with finite, weights, subset95  unfold divisorSum96  exact total9798theorem divisorSum.one (w : Set)99  requires weights : w : ℕ → ℤ100  shows divisorSum(1, w) = w(1)101proof102  have oneNat : Nat(1) by typecheck103  have oneMember := nat.omega.forward with oneNat104  have single := integerSetSum.singleton with weights, oneMember105  have same := divisors.one106  unfold divisorSum107  cc108109theorem divisorSum.congr (n : Nat, w v : Set)110  requires weightsW : w : ℕ → ℤ111  requires weightsV : v : ℕ → ℤ112  requires values : ∀ d ∈ divisors(n), w(d) = v(d)113  shows divisorSum(n, w) = divisorSum(n, v)114proof115  have subset := divisors.subset_naturals at n116  have same := integerSetSum.congr with weightsW, weightsV, subset, values117  unfold divisorSum118  cc119120theorem divisorSum.scale (n : Nat, w v : Set) (a : Integer)121  requires weightsW : w : ℕ → ℤ122  requires weightsV : v : ℕ → ℤ123  requires values : ∀ d ∈ divisors(n), v(d) = integerMulValue(a, w(d))124  shows divisorSum(n, v) = integerMulValue(a, divisorSum(n, w))125proof126  have finite := divisors.finite at n127  have subset := divisors.subset_naturals at n128  have scaled := integerSetSum.scale with finite, weightsW, weightsV, subset,129    values130  unfold divisorSum131  cc132133theorem divisorSum.zero (n : Nat, w : Set)134  requires weights : w : ℕ → ℤ135  requires values : ∀ d ∈ divisors(n), w(d) = integerZero136  shows divisorSum(n, w) = integerZero137proof138  have finite := divisors.finite at n139  have subset := divisors.subset_naturals at n140  have vanishing := integerSetSum.zero with finite, weights, subset, values141  unfold divisorSum142  cc143144theorem divisorSum.support (n : Nat, S w : Set)145  requires weights : w : ℕ → ℤ146  requires inner : S ⊆ divisors(n)147  requires vanishes : ∀ d ∈ divisors(n), ¬(d ∈ S) → w(d) = integerZero148  shows divisorSum(n, w) = integerSetSum(S, w)149proof150  have finite := divisors.finite at n151  have subset := divisors.subset_naturals at n152  have restricted := integerSetSum.support with finite, weights, subset, inner,153    vanishes154  unfold divisorSum155  cc156157-- A weight vanishing at every proper divisor of n sums to its value at n.158theorem divisorSum.single (n : Nat, w : Set)159  requires weights : w : ℕ → ℤ160  requires vanishes : ∀ d ∈ divisors(n), d ≠ n → w(d) = integerZero161  shows divisorSum(n, w) = w(n)162proof163  have self := divisors.self_member at n164  have inner : {n} ⊆ divisors(n) by simp165  have nNat : Nat(n) by typecheck166  have nMember := nat.omega.forward with nNat167  have outside : ∀ d ∈ divisors(n), ¬(d ∈ {n}) → w(d) = integerZero168    intros d hd absent169    have different : d ≠ n170      intro same171      apply absent172      rw same173      simp174    exact vanishes with d, hd, different175  have restricted := divisorSum.support with weights, inner, outside176  have single := integerSetSum.singleton with weights, nMember177  rw [restricted, single]178  rfl179180-- The complementary divisor n / d of a divisor d of n.181defgraph complementaryDivisor (n : Nat) (d ∈ divisors(n)) : divisors(n) :=182  quotientNat(n, d)183requires nonzero : n ≠ 0184proof185  have dNat := divisors.natural with member186  exact divisors.quotient_member with nonzero, member187188theorem complementaryDivisor.involution (n : Nat)189  requires nonzero : n ≠ 0190  shows InvolutionOn(complementaryDivisor(n), divisors(n))191proof192  have function := complementaryDivisor.function at n with nonzero193  refine ⟨function, _⟩194  intros d hd195  have dNat := divisors.natural with hd196  have factor := divisors.divides with hd197  have image := divisors.quotient_member with nonzero, hd198  have first := complementaryDivisor.value at n, d with nonzero, hd199  have second := complementaryDivisor.value at n, quotientNat(n, d) with200    nonzero, image201  have twice := quotientNat.complement with nonzero, factor202  rw [first, second, twice]203  rfl204205theorem complementaryDivisor.bijective (n : Nat)206  requires nonzero : n ≠ 0207  shows BijectiveBetween(complementaryDivisor(n), divisors(n), divisors(n))208proof209  have involution := complementaryDivisor.involution with nonzero210  exact InvolutionOn.bijective with involution211212-- The weight d ↦ w(n / d).213defgraph complementaryWeights (n : Nat) (w : Set) (d ∈ ℕ) : ℤ :=214  w(quotientNat(n, d))215requires weights : w : ℕ → ℤ216proof217  have dNat := nat.omega.backward with member218  have quotientNatural := quotientNat.natural at d, n219  have quotientMember := nat.omega.forward with quotientNatural220  exact FunctionBetween.apply_closed with weights, quotientMember221222-- Summing w(n / d) over the divisors d of n is summing w over them.223theorem divisorSum.reflect (n : Nat, w : Set)224  requires nonzero : n ≠ 0225  requires weights : w : ℕ → ℤ226  shows divisorSum(n, complementaryWeights(n, w)) = divisorSum(n, w)227proof228  have finite := divisors.finite at n229  have subset := divisors.subset_naturals at n230  have reflected := complementaryWeights.function at n, w with weights231  have bijective := complementaryDivisor.bijective with nonzero232  have values : ∀ d ∈ divisors(n),233      complementaryWeights(n, w)(d) = w(complementaryDivisor(n)(d))234    intros d hd235    have dMember := subset with d, hd236    have value := complementaryWeights.value at n, w, d with weights237    have image := complementaryDivisor.value at n, d with nonzero, hd238    cc239  have sum := integerSetSum.reindex at divisors(n), divisors(n), ℕ, ℕ,240    complementaryWeights(n, w), w, complementaryDivisor(n) with finite,241      reflected, weights, subset, subset, bijective, values242  unfold divisorSum243  cc244245-- The summands a(d) · b(n / d) of a Dirichlet convolution at n.246defgraph dirichletTerms (a b : Set) (n : Nat) (d ∈ ℕ) : ℤ :=247  integerMulValue(a(d), b(quotientNat(n, d)))248requires weightsA : a : ℕ → ℤ249requires weightsB : b : ℕ → ℤ250proof251  have dNat := nat.omega.backward with member252  have quotientNatural := quotientNat.natural at d, n253  have quotientMember := nat.omega.forward with quotientNatural254  have left := FunctionBetween.apply_closed with weightsA, member255  have right := FunctionBetween.apply_closed with weightsB, quotientMember256  exact integerMulValue.integer at a(d), b(quotientNat(n, d)) with *257258-- The summatory function n ↦ ∑_{d ∣ n} w(d) of an integer-valued weight.259defgraph summatory (w : Set) (n ∈ ℕ) : ℤ := divisorSum(n, w)260requires weights : w : ℕ → ℤ261proof262  have nNat := nat.omega.backward with member263  exact divisorSum.integer with weights264