Grace/Cumulus/NumberTheory/DivisorSum.g17

Open in Workbench Download source

Imports

Cardinal.NaturalSumLaws · Divisors · LCM

Declarations

Source

1-- The sum of divisors σ(n) = ∑_{d ∣ n} d: its values at 0, 1, and a prime,2-- the split σ(n) = n + 1 + (sum over the divisors strictly between), the3-- characterisation of primes by σ(p) = p + 1, and multiplicativity4-- σ(m · n) = σ(m) · σ(n) for coprime m and n through the bijection5-- (d, e) ↦ d · e from divisors(m) × divisors(n) onto divisors(m · n)6-- 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.NumberTheory.DivisorSum12import Cardinal.NaturalSumLaws13import Divisors14import LCM1516-- The identity on ℕ as the weight of a divisor.17theorem identityWeight.natural (d : Nat)18  shows identity(ℕ)(d) ∈ ℕ19proof20  have dNat : Nat(d) by typecheck21  have dIn := nat.omega.forward with dNat22  have value := identity.apply at d, ℕ with dIn23  rw value24  exact dIn2526theorem identityWeight.value (d : Nat)27  shows identity(ℕ)(d) = d28proof29  have dNat : Nat(d) by typecheck30  have dIn := nat.omega.forward with dNat31  exact identity.apply at d, ℕ with dIn3233theorem divisors.weights (n : Nat)34  shows ∀ d ∈ divisors(n), identity(ℕ)(d) ∈ ℕ35proof36  intros d hd37  have dNat := divisors.natural with hd38  exact identityWeight.natural at d3940-- The sum of the divisors.41def sigma (n : Nat) : Nat := natSum(divisors(n), identity(ℕ))42proof43  have finite := divisors.finite at n44  have weights := divisors.weights at n45  unfold sigma46  exact natSum.natural with finite, weights4748theorem sigma.definition (n : Nat)49  shows sigma(n) = natSum(divisors(n), identity(ℕ))50proof51  simp [sigma]5253theorem sigma.natural (n : Nat)54  shows Nat(sigma(n))55proof56  typecheck5758theorem sigma.zero59  shows sigma(0) = 060proof61  have weight := identityWeight.natural at 062  have value := identityWeight.value at 063  have single := natSum.singleton with weight64  rw [sigma.definition, divisors.zero, single, value]65  rfl6667theorem sigma.one68  shows sigma(1) = 169proof70  have weight := identityWeight.natural at 171  have value := identityWeight.value at 172  have single := natSum.singleton with weight73  rw [sigma.definition, divisors.one, single, value]74  rfl7576theorem sigma.prime (p : Nat)77  requires prime : Prime(p)78  shows sigma(p) = p + 179proof80  have same := divisors.prime with prime81  have aboveOne := Prime.greater_than_one with prime82  have distinct : 1 ≠ p83    intro equal84    rw ← equal at aboveOne85    exact Less.irreflexive at 1 with aboveOne86  have weightOne := identityWeight.natural at 187  have weightP := identityWeight.natural at p88  have valueOne := identityWeight.value at 189  have valueP := identityWeight.value at p90  have paired := natSum.pair with weightOne, weightP, distinct91  rw [sigma.definition, same, paired, valueOne, valueP]92  exact add.commutative at p, 19394-- The divisors strictly between 1 and n.95def innerDivisors (n : Nat) : Set := divisors(n) ∖ {1, n}9697theorem innerDivisors.membership (n : Nat, d : Set)98  shows d ∈ innerDivisors(n) ↔ d ∈ divisors(n) ∧ ¬(d = 1 ∨ d = n)99proof100  simp [innerDivisors, difference.membership, pair.membership]101102theorem innerDivisors.subset (n : Nat)103  shows innerDivisors(n) ⊆ divisors(n)104proof105  intros d hd106  have parts := innerDivisors.membership.forward with hd107  exact parts.left108109theorem innerDivisors.finite (n : Nat)110  shows Finite(innerDivisors(n))111proof112  have finite := divisors.finite at n113  have subset := innerDivisors.subset at n114  exact Finite.subset with finite, subset115116theorem innerDivisors.weights (n : Nat)117  shows ∀ d ∈ innerDivisors(n), identity(ℕ)(d) ∈ ℕ118proof119  intros d hd120  have subset := innerDivisors.subset at n121  have member := subset with d, hd122  have dNat := divisors.natural with member123  exact identityWeight.natural at d124125-- The sum of the divisors strictly between 1 and n.126def innerSum (n : Nat) : Nat := natSum(innerDivisors(n), identity(ℕ))127proof128  have finite := innerDivisors.finite at n129  have weights := innerDivisors.weights at n130  unfold innerSum131  exact natSum.natural with finite, weights132133theorem innerSum.definition (n : Nat)134  shows innerSum(n) = natSum(innerDivisors(n), identity(ℕ))135proof136  simp [innerSum]137138theorem innerDivisors.disjoint (n : Nat)139  shows Disjoint({1, n}, innerDivisors(n))140proof141  apply Disjoint.iff.backward142  intros d hd inside143  have parts := innerDivisors.membership.forward with inside144  have alternatives := pair.membership.forward with hd145  exact parts.right with alternatives146147theorem divisors.split (n : Nat)148  requires nonzero : n ≠ 0149  shows divisors(n) = {1, n} ∪ innerDivisors(n)150proof151  have oneMember := divisors.one_member at n with nonzero152  have selfMember := divisors.self_member at n153  ext d154  constructor155  . intro member156    have decided : d = 1 ∨ d = n ∨ ¬(d = 1 ∨ d = n) by tauto157    apply union2.membership.backward158    rcases decided with one | self | neither159    . left160      rw one161      exact pair.left at 1, n162    . left163      rw self164      exact pair.right at 1, n165    . right166      exact innerDivisors.membership.backward with ⟨member, neither⟩167  . intro member168    have split := union2.membership.forward with member169    cases split with inPair | inner170    . have alternatives := pair.membership.forward with inPair171      cases alternatives with one | self172      . rw one173        exact oneMember174      . rw self175        exact selfMember176    . have parts := innerDivisors.membership.forward with inner177      exact parts.left178179-- σ(n) = n + 1 + the sum of the divisors strictly between.180theorem sigma.split (n : Nat)181  requires aboveOne : 1 < n182  shows sigma(n) = n + 1 + innerSum(n)183proof184  have positive : 0 < n by arith185  have nonzero := Less.ne_zero_of_positive with positive186  have split := divisors.split with nonzero187  have distinct : 1 ≠ n188    intro equal189    rw ← equal at aboveOne190    exact Less.irreflexive at 1 with aboveOne191  have oneMember := divisors.one_member at n with nonzero192  have selfMember := divisors.self_member at n193  have characterization := pair.subset_iff at 1, n, divisors(n)194  have pairSubset := characterization.backward with ⟨oneMember, selfMember⟩195  have finite := divisors.finite at n196  have finitePair := Finite.subset with finite, pairSubset197  have finiteInner := innerDivisors.finite at n198  have weights := divisors.weights at n199  have weightsPair : ∀ d ∈ {1, n}, identity(ℕ)(d) ∈ ℕ200    intros d hd201    exact weights with d, (pairSubset with d, hd)202  have weightsInner := innerDivisors.weights at n203  have disjoint := innerDivisors.disjoint at n204  have added := natSum.union_disjoint with finitePair, finiteInner, weightsPair,205    weightsInner, disjoint206  have weightOne := identityWeight.natural at 1207  have weightN := identityWeight.natural at n208  have valueOne := identityWeight.value at 1209  have valueN := identityWeight.value at n210  have paired := natSum.pair with weightOne, weightN, distinct211  have innerNat := natSum.natural with finiteInner, weightsInner212  have swapped : 1 + n = n + 1 := add.commutative at n, 1213  rw [sigma.definition, innerSum.definition, split, added, paired, valueOne,214    valueN, swapped]215  rfl216217theorem innerDivisors.le_sum (n d : Nat)218  requires member : d ∈ innerDivisors(n)219  shows d ≤ innerSum(n)220proof221  rw innerSum.definition222  have finite := innerDivisors.finite at n223  have weights := innerDivisors.weights at n224  have characterization := singleton.subset_iff at d, innerDivisors(n)225  have single := characterization.backward with member226  have bounded := natSum.monotone with finite, single, weights227  have weight := identityWeight.natural at d228  have value := identityWeight.value at d229  have point := natSum.singleton with weight230  rw [point, value] at bounded231  exact bounded232233theorem innerDivisors.two_le (n d : Nat)234  requires nonzero : n ≠ 0235  requires member : d ∈ innerDivisors(n)236  shows 2 ≤ d237proof238  have parts := innerDivisors.membership.forward with member239  have factor := divisors.divides with parts.left240  have dNonzero := divides.nonzero with factor, nonzero241  have notOne : d ≠ 1242    intro one243    apply parts.right244    left245    exact one246  have characterization := Less.one_lt_iff at d247  have aboveOne := characterization.backward with ⟨dNonzero, notOne⟩248  arith249250theorem innerDivisors.member (n d : Nat)251  requires nonzero : n ≠ 0252  requires factor : d ∣ n253  requires notOne : d ≠ 1254  requires notSelf : d ≠ n255  shows d ∈ innerDivisors(n)256proof257  have below := divides.le with factor, nonzero258  have characterization := divisors.membership_le at n, d259  have member := characterization.backward with ⟨below, factor⟩260  have neither : ¬(d = 1 ∨ d = n)261    intro either262    cases either with one | self263    . exact notOne with one264    . exact notSelf with self265  exact innerDivisors.membership.backward with ⟨member, neither⟩266267-- A number above 1 with σ(n) = n + 1 has no divisor strictly between.268theorem Prime.of_sigma (n : Nat)269  requires aboveOne : 1 < n270  requires sum : sigma(n) = n + 1271  shows Prime(n)272proof273  have positive : 0 < n by arith274  have nonzero := Less.ne_zero_of_positive with positive275  have split := sigma.split with aboveOne276  rw sum at split277  have bounded : innerSum(n) ≤ 0 by arith278  have innerZero := LessEqual.eq_zero with bounded279  have innerEmpty : innerDivisors(n) = ∅280    ext d281    constructor282    . intro member283      have subset := innerDivisors.subset at n284      have dNat := divisors.natural with (subset with d, member)285      have twoLe := innerDivisors.two_le with nonzero, member286      have bound := innerDivisors.le_sum with member287      rw innerZero at bound288      exfalso289      arith290    . intro member291      exfalso292      exact empty.membership with d, member293  have decomposed := divisors.split with nonzero294  rw [innerEmpty, union2.right_empty] at decomposed295  exact Prime.of_divisors with aboveOne, decomposed296297theorem sigma.prime_iff (p : Nat)298  requires aboveOne : 1 < p299  shows Prime(p) ↔ sigma(p) = p + 1300proof301  constructor302  . intro prime303    exact sigma.prime with prime304  . intro sum305    exact Prime.of_sigma with aboveOne, sum306307-- Divisors of coprime numbers are coprime.308theorem coprime.of_divides (a b d e : Nat)309  requires coprime : gcd(a, b) = 1310  requires left : d ∣ a311  requires right : e ∣ b312  shows gcd(d, e) = 1313proof314  have characterization := gcd.eq_one_iff at d, e315  apply characterization.backward316  intros k kNat kd ke317  have ka := divides.transitive with kd, left318  have kb := divides.transitive with ke, right319  exact coprime.divisor_one with coprime, ka, kb320321-- A divisor of a coprime product is the product of its parts in each322-- factor.323theorem divides.coprime_split (a b d : Nat)324  requires nonzeroA : a ≠ 0325  requires nonzeroB : b ≠ 0326  requires coprime : gcd(a, b) = 1327  requires factor : d ∣ a * b328  shows d = gcd(d, a) * gcd(d, b)329proof330  have gNonzero := gcd.nonzero_right at d, a with nonzeroA331  have gNat := gcd.natural at d, a332  have hNat := gcd.natural at d, b333  have gDividesD := gcd.divides_left at d, a334  have gDividesA := gcd.divides_right at d, a335  have hDividesD := gcd.divides_left at d, b336  have hDividesB := gcd.divides_right at d, b337  obtain ⟨e, eNat, dProduct⟩ := gDividesD338  obtain ⟨p, pNat, aProduct⟩ := gDividesA339  have cofactors := gcd.cofactor_coprime at d, a, e, p with gNonzero, dProduct,340    aProduct341  have rearranged : gcd(d, a) * p * b = gcd(d, a) * (p * b) by ring342  have expanded : a * b = gcd(d, a) * (p * b) by cc343  have scaled : gcd(d, a) * e ∣ gcd(d, a) * (p * b)344    rw [dProduct, ← expanded]345    exact factor346  have cancel := divides.mul_cancel_left at gcd(d, a), e, p * b with gNonzero347  have eDivides := cancel.forward with scaled348  have commuted : p * b = b * p by ring349  rw commuted at eDivides350  have coprimePE := coprime.symmetric with cofactors351  have eDividesB := coprime.cancel_right with coprimePE, eDivides352  have eDividesD := divides.mul_right_self at e, gcd(d, a)353  rw dProduct at eDividesD354  have eDividesH := gcd.greatest with eDividesD, eDividesB355  have gSelf := divides.reflexive at gcd(d, a)356  have forward := divides.mul_mono with gSelf, eDividesH357  rw dProduct at forward358  have gDividesD2 := gcd.divides_left at d, a359  have coprimeGH := coprime.of_divides with coprime, gDividesA, hDividesB360  have backward := coprime.mul_divides with coprimeGH, gDividesD2, hDividesD361  exact divides.antisymmetric with forward, backward362363-- The product (d, e) ↦ d · e of a divisor of a and a divisor of b.364defgraph divisorMul (a b : Nat) (q ∈ divisors(a) × divisors(b)) :365    divisors(a * b) := mul(fst(q), snd(q))366requires nonzeroA : a ≠ 0367requires nonzeroB : b ≠ 0368proof369  obtain ⟨bound, d, hd, e, he, shape⟩ :=370    product.membership.forward with member371  have dNat := divisors.natural with hd372  have eNat := divisors.natural with he373  have dDivides := divisors.divides with hd374  have eDivides := divisors.divides with he375  have productDivides := divides.mul_mono with dDivides, eDivides376  have productNonzero := mul.nonzero with nonzeroA, nonzeroB377  have below := divides.le with productDivides, productNonzero378  have characterization := divisors.membership_le at a * b, mul(d, e)379  rw [shape, fst.pair, snd.pair]380  exact characterization.backward with ⟨below, productDivides⟩381382theorem divisorMul.pair (a b : Nat) (d e : Set)383  requires nonzeroA : a ≠ 0384  requires nonzeroB : b ≠ 0385  requires hd : d ∈ divisors(a)386  requires he : e ∈ divisors(b)387  shows divisorMul(a, b)((d, e)) = mul(d, e)388proof389  have pairMember := product.pair with hd, he390  have value := divisorMul.value at a, b, (d, e) with nonzeroA, nonzeroB,391    pairMember392  rw [value, fst.pair, snd.pair]393  rfl394395theorem divisorMul.injective (a b : Nat)396  requires nonzeroA : a ≠ 0397  requires nonzeroB : b ≠ 0398  requires coprime : gcd(a, b) = 1399  shows InjectiveBetween(divisorMul(a, b), divisors(a) × divisors(b),400    divisors(a * b))401proof402  have function := divisorMul.function at a, b with nonzeroA, nonzeroB403  refine ⟨function, _⟩404  intros x hx y hy z hz relatesX relatesY405  obtain ⟨boundX, d1, hd1, d2, hd2, xEq⟩ :=406    product.membership.forward with hx407  obtain ⟨boundY, e1, he1, e2, he2, yEq⟩ :=408    product.membership.forward with hy409  have d1Nat := divisors.natural with hd1410  have d2Nat := divisors.natural with hd2411  have e1Nat := divisors.natural with he1412  have e2Nat := divisors.natural with he2413  have d1Divides := divisors.divides with hd1414  have d2Divides := divisors.divides with hd2415  have e1Divides := divisors.divides with he1416  have e2Divides := divisors.divides with he2417  have valueX := FunctionBetween.apply_value with function, hx, relatesX418  have valueY := FunctionBetween.apply_value with function, hy, relatesY419  have pairX := divisorMul.pair with nonzeroA, nonzeroB, hd1, hd2420  have pairY := divisorMul.pair with nonzeroA, nonzeroB, he1, he2421  rw xEq at valueX422  rw yEq at valueY423  have same : mul(d1, d2) = mul(e1, e2) by cc424  have d1DividesProduct : d1 ∣ mul(e1, e2)425    rw ← same426    exact divides.mul_left_self at d1, d2427  have e1DividesProduct : e1 ∣ mul(d1, d2)428    rw same429    exact divides.mul_left_self at e1, e2430  have coprimeD1E2 := coprime.of_divides with coprime, d1Divides, e2Divides431  have coprimeE2D1 := coprime.symmetric with coprimeD1E2432  have d1DividesE1 := coprime.cancel_right with coprimeE2D1, d1DividesProduct433  have coprimeE1D2 := coprime.of_divides with coprime, e1Divides, d2Divides434  have coprimeD2E1 := coprime.symmetric with coprimeE1D2435  have e1DividesD1 := coprime.cancel_right with coprimeD2E1, e1DividesProduct436  have firstEqual := divides.antisymmetric with d1DividesE1, e1DividesD1437  have e1Nonzero := divides.nonzero with e1Divides, nonzeroA438  rw firstEqual at same439  have secondEqual := mul.left_cancel_positive with e1Nonzero, same440  rw [xEq, yEq, firstEqual, secondEqual]441  rfl442443theorem divisorMul.surjective (a b : Nat)444  requires nonzeroA : a ≠ 0445  requires nonzeroB : b ≠ 0446  requires coprime : gcd(a, b) = 1447  shows SurjectiveBetween(divisorMul(a, b), divisors(a) × divisors(b),448    divisors(a * b))449proof450  have function := divisorMul.function at a, b with nonzeroA, nonzeroB451  refine ⟨function, _⟩452  intros z hz453  have zNat := divisors.natural with hz454  have factor := divisors.divides with hz455  have split := divides.coprime_split with nonzeroA, nonzeroB, coprime, factor456  have gNat := gcd.natural at z, a457  have hNat := gcd.natural at z, b458  have gDividesA := gcd.divides_right at z, a459  have hDividesB := gcd.divides_right at z, b460  have gBelow := divides.le with gDividesA, nonzeroA461  have hBelow := divides.le with hDividesB, nonzeroB462  have characterizationA := divisors.membership_le at a, gcd(z, a)463  have characterizationB := divisors.membership_le at b, gcd(z, b)464  have inA := characterizationA.backward with ⟨gBelow, gDividesA⟩465  have inB := characterizationB.backward with ⟨hBelow, hDividesB⟩466  have pairMember := product.pair with inA, inB467  have value := divisorMul.pair with nonzeroA, nonzeroB, inA, inB468  have relates := FunctionBetween.relates_apply with function, pairMember469  rw [value, ← split] at relates470  exact ⟨(gcd(z, a), gcd(z, b)), pairMember, relates⟩471472-- The divisors of a coprime product are the products of divisors of the473-- factors, each exactly once.474theorem divisorMul.bijective (a b : Nat)475  requires nonzeroA : a ≠ 0476  requires nonzeroB : b ≠ 0477  requires coprime : gcd(a, b) = 1478  shows BijectiveBetween(divisorMul(a, b), divisors(a) × divisors(b),479    divisors(a * b))480proof481  have injective := divisorMul.injective with nonzeroA, nonzeroB, coprime482  have surjective := divisorMul.surjective with nonzeroA, nonzeroB, coprime483  exact ⟨injective, surjective⟩484485theorem sigma.multiplicative_of_nonzero (m n : Nat)486  requires nonzeroM : m ≠ 0487  requires nonzeroN : n ≠ 0488  requires coprime : gcd(m, n) = 1489  shows sigma(m * n) = sigma(m) * sigma(n)490proof491  have finiteM := divisors.finite at m492  have finiteN := divisors.finite at n493  have finitePairs := Finite.product with finiteM, finiteN494  have weightsM := divisors.weights at m495  have weightsN := divisors.weights at n496  have weightsProduct := divisors.weights at m * n497  have bijective := divisorMul.bijective with nonzeroM, nonzeroN, coprime498  have values : ∀ q ∈ divisors(m) × divisors(n),499      weightProduct(divisors(m), divisors(n), identity(ℕ), identity(ℕ))(q) =500        identity(ℕ)(divisorMul(m, n)(q))501    intros q hq502    obtain ⟨bound, d, hd, e, he, shape⟩ :=503      product.membership.forward with hq504    have dNat := divisors.natural with hd505    have eNat := divisors.natural with he506    have left := weightProduct.pair with weightsM, weightsN, hd, he507    have right := divisorMul.pair with nonzeroM, nonzeroN, hd, he508    have valueD := identityWeight.value at d509    have valueE := identityWeight.value at e510    have valueDE := identityWeight.value at mul(d, e)511    rw [shape, left, right, valueD, valueE, valueDE]512    rfl513  have reindexed := natSum.reindex with finitePairs, bijective, weightsProduct,514    values515  have product := natSum.product with finiteM, finiteN, weightsM, weightsN516  rw [sigma.definition, sigma.definition, sigma.definition, reindexed, product]517  rfl518519-- σ is multiplicative.520theorem sigma.multiplicative (m n : Nat)521  requires coprime : gcd(m, n) = 1522  shows sigma(m * n) = sigma(m) * sigma(n)523proof524  have casesM : m = 0 ∨ m ≠ 0 by tauto525  have casesN : n = 0 ∨ n ≠ 0 by tauto526  cases casesM with mZero | mNonzero527  . have nOne : n = 1528      rw [mZero, gcd.zero_left] at coprime529      exact coprime530    rw [mZero, nOne, mul.left_zero, sigma.zero, sigma.one, mul.left_zero]531    rfl532  . cases casesN with nZero | nNonzero533    . have mOne : m = 1534        rw [nZero, gcd.zero_right] at coprime535        exact coprime536      rw [nZero, mOne, mul.right_zero, sigma.zero, sigma.one, mul.right_zero]537      rfl538    . exact sigma.multiplicative_of_nonzero with mNonzero, nNonzero, coprime539