Grace/Cumulus/Combinatorics/CoprimeDivisors.g17

Open in Workbench Download source

Imports

DivisorSums

Declarations

Source

1-- Divisor sums over a coprime product: through the bijection2-- (d, e) ↦ d · e from divisors(a) × divisors(b) onto divisors(a · b)3-- (NumberTheory/DivisorSum), a sum over the divisors of a · b is the sum4-- over such pairs5-- 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.CoprimeDivisors11import DivisorSums1213-- The weight (d, e) ↦ w(d · e) on pairs of divisors.14defgraph pairedWeights (a b : Nat) (w : Set) (q ∈ divisors(a) × divisors(b)) :15    ℤ := w(divisorMul(a, b)(q))16requires nonzeroA : a ≠ 017requires nonzeroB : b ≠ 018requires weights : w : ℕ → ℤ19proof20  have function := divisorMul.function at a, b with nonzeroA, nonzeroB21  have image := FunctionBetween.apply_closed with function, member22  have naturals := divisors.subset_naturals at a * b23  have imageMember := naturals with divisorMul(a, b)(q), image24  exact FunctionBetween.apply_closed with weights, imageMember2526-- A sum over the divisors of a coprime product a · b is the sum of27-- w(d · e) over the pairs of divisors d ∣ a, e ∣ b.28theorem divisorSum.mul_coprime (a b : Nat, w : Set)29  requires nonzeroA : a ≠ 030  requires nonzeroB : b ≠ 031  requires coprime : gcd(a, b) = 132  requires weights : w : ℕ → ℤ33  shows divisorSum(a * b, w) =34    integerSetSum(divisors(a) × divisors(b), pairedWeights(a, b, w))35proof36  have finiteA := divisors.finite at a37  have finiteB := divisors.finite at b38  have finite := Finite.product with finiteA, finiteB39  have paired := pairedWeights.function at a, b, w with nonzeroA, nonzeroB,40    weights41  have bijective := divisorMul.bijective with nonzeroA, nonzeroB, coprime42  have selfSubset := Subset.reflexive at divisors(a) × divisors(b)43  have naturals := divisors.subset_naturals at a * b44  have values : ∀ q ∈ divisors(a) × divisors(b),45      pairedWeights(a, b, w)(q) = w(divisorMul(a, b)(q))46    intros q hq47    exact pairedWeights.value at a, b, w, q with nonzeroA, nonzeroB, weights,48      hq49  have sum := integerSetSum.reindex at divisors(a) × divisors(b),50    divisors(a * b), divisors(a) × divisors(b), ℕ, pairedWeights(a, b, w), w,51      divisorMul(a, b) with finite, paired, weights, selfSubset, naturals,52        bijective, values53  symm54  simp [divisorSum]55