Grace/Cumulus/Combinatorics/DivisorInterchange.g17

Open in Workbench Download source

Imports

DivisorSums

Declarations

Source

1-- Interchanging a double sum over divisors: for a weight F on pairs of2-- naturals and n ≠ 0, ∑_{d ∣ n} ∑_{e ∣ n/d} F(d, e) = ∑_{e ∣ n} ∑_{d ∣ n/e}3-- F(d, e), both being the sum of F over the pairs of divisors whose product4-- divides n, computed by rows and by columns of a matrix on5-- divisors(n) × divisors(n) that vanishes off those pairs6-- 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.DivisorInterchange12import DivisorSums1314-- The row e ↦ F(d, e) and the column d ↦ F(d, e) of a weight on pairs.15defgraph rowTerms (F d : Set) (e ∈ ℕ) : ℤ := F((d, e))16requires weights : F : ℕ × ℕ → ℤ17requires rowIndex : d ∈ ℕ18proof19  have pair := product.pair with rowIndex, member20  exact FunctionBetween.apply_closed with weights, pair2122defgraph columnTerms (F e : Set) (d ∈ ℕ) : ℤ := F((d, e))23requires weights : F : ℕ × ℕ → ℤ24requires columnIndex : e ∈ ℕ25proof26  have pair := product.pair with member, columnIndex27  exact FunctionBetween.apply_closed with weights, pair2829-- The inner sums d ↦ ∑_{e ∣ n/d} F(d, e) and e ↦ ∑_{d ∣ n/e} F(d, e).30defgraph rowDivisorSums (F : Set) (n : Nat) (d ∈ ℕ) : ℤ :=31  divisorSum(quotientNat(n, d), rowTerms(F, d))32requires weights : F : ℕ × ℕ → ℤ33proof34  have dNat := nat.omega.backward with member35  have quotientNatural := quotientNat.natural at d, n36  have rows := rowTerms.function at F, d with weights, member37  exact divisorSum.integer at quotientNat(n, d), rowTerms(F, d) with rows3839defgraph columnDivisorSums (F : Set) (n : Nat) (e ∈ ℕ) : ℤ :=40  divisorSum(quotientNat(n, e), columnTerms(F, e))41requires weights : F : ℕ × ℕ → ℤ42proof43  have eNat := nat.omega.backward with member44  have quotientNatural := quotientNat.natural at e, n45  have columns := columnTerms.function at F, e with weights, member46  exact divisorSum.integer at quotientNat(n, e), columnTerms(F, e) with47    columns4849-- The pairs of divisors of n whose product divides n.50def dividingPairs (n : Nat) : Set :=51  { q ∈ divisors(n) × divisors(n) |52    ∃ d ∈ divisors(n), ∃ e ∈ divisors(n), q = (d, e) ∧ mul(d, e) ∣ n }5354theorem dividingPairs.pair (n : Nat, d e : Set)55  shows (d, e) ∈ dividingPairs(n) ↔56    d ∈ divisors(n) ∧ e ∈ divisors(n) ∧ mul(d, e) ∣ n57proof58  have characterization := dividingPairs.membership at n, (d, e)59  constructor60  . intro member61    have unpacked := characterization.forward with member62    obtain ⟨pairMember, x, hx, y, hy, shape, factor⟩ := unpacked63    obtain ⟨dEq, eEq⟩ := orderedPair.injective with shape64    rw [dEq, eEq]65    exact ⟨hx, hy, factor⟩66  . intro triple67    rcases triple with ⟨hd, he, factor⟩68    have pairMember := product.pair with hd, he69    apply characterization.backward70    refine ⟨pairMember, d, hd, e, he, rfl, factor⟩7172theorem dividingPairs.symmetric (n : Nat, d e : Set)73  requires member : (d, e) ∈ dividingPairs(n)74  shows (e, d) ∈ dividingPairs(n)75proof76  have triple := dividingPairs.pair.forward with member77  rcases triple with ⟨hd, he, factor⟩78  have dNat := divisors.natural with hd79  have eNat := divisors.natural with he80  have commuted := mul.commutative at e, d81  rw commuted at factor82  exact dividingPairs.pair.backward with ⟨he, hd, factor⟩8384theorem dividingPairs.iff_quotient (n : Nat, d e : Set)85  requires nonzero : n ≠ 086  requires member : d ∈ divisors(n)87  shows (d, e) ∈ dividingPairs(n) ↔ e ∈ divisors(quotientNat(n, d))88proof89  have dNat := divisors.natural with member90  have factor := divisors.divides with member91  have quotientNonzero := divides.quotient_ne_zero with nonzero, factor92  have inner := divisors.quotient_subset with nonzero, factor93  constructor94  . intro pairMember95    have triple := dividingPairs.pair.forward with pairMember96    rcases triple with ⟨_, he, product⟩97    have eNat := divisors.natural with he98    have characterization := divides.mul_iff_quotient at d, e, n with nonzero,99      factor100    have quotientDivides := characterization.forward with product101    have below := divides.le with quotientDivides, quotientNonzero102    have membership := divisors.membership_le at quotientNat(n, d), e103    exact membership.backward with ⟨below, quotientDivides⟩104  . intro quotientMember105    have he := inner with e, quotientMember106    have eNat := divisors.natural with he107    have quotientDivides := divisors.divides with quotientMember108    have characterization := divides.mul_iff_quotient at d, e, n with nonzero,109      factor110    have product := characterization.backward with quotientDivides111    exact dividingPairs.pair.backward with ⟨member, he, product⟩112113-- The matrix F(d, e) · [d · e ∣ n] on divisors(n) × divisors(n).114defgraph divisorMatrix (F : Set) (n : Nat) (q ∈ divisors(n) × divisors(n)) :115    ℤ := integerMulValue(F(q), integerOfNat(indicator(dividingPairs(n), q)))116requires weights : F : ℕ × ℕ → ℤ117proof118  have naturals := divisors.subset_naturals at n119  have subset := product.monotone with naturals, naturals120  have inNaturals := subset with q, member121  have value := FunctionBetween.apply_closed with weights, inNaturals122  have indicatorNat := indicator.natural at dividingPairs(n), q123  have mask := integerOfNat.integer at indicator(dividingPairs(n), q)124  exact integerMulValue.integer at F(q),125    integerOfNat(indicator(dividingPairs(n), q)) with *126127theorem divisorMatrix.inside (F : Set) (n : Nat) (d e : Set)128  requires weights : F : ℕ × ℕ → ℤ129  requires member : (d, e) ∈ dividingPairs(n)130  shows divisorMatrix(F, n)((d, e)) = F((d, e))131proof132  have triple := dividingPairs.pair.forward with member133  rcases triple with ⟨hd, he, _⟩134  have naturals := divisors.subset_naturals at n135  have pairMember := product.pair with hd, he136  have dMember := naturals with d, hd137  have eMember := naturals with e, he138  have inNaturals := product.pair with dMember, eMember139  have value := FunctionBetween.apply_closed with weights, inNaturals140  have entry := divisorMatrix.value at F, n, (d, e) with weights, pairMember141  have one := indicator.member with member142  rw [entry, one, integerOfNat.one]143  ring144145theorem divisorMatrix.outside (F : Set) (n : Nat) (d e : Set)146  requires weights : F : ℕ × ℕ → ℤ147  requires pairMember : (d, e) ∈ divisors(n) × divisors(n)148  requires absent : ¬((d, e) ∈ dividingPairs(n))149  shows divisorMatrix(F, n)((d, e)) = integerZero150proof151  have naturals := divisors.subset_naturals at n152  have subset := product.monotone with naturals, naturals153  have inNaturals := subset with (d, e), pairMember154  have value := FunctionBetween.apply_closed with weights, inNaturals155  have entry := divisorMatrix.value at F, n, (d, e) with weights, pairMember156  have zero := indicator.absent with absent157  rw [entry, zero, integerOfNat.zero]158  ring159160-- Row d of the matrix sums to ∑_{e ∣ n/d} F(d, e).161theorem divisorMatrix.row (F : Set) (n : Nat) (d : Set)162  requires nonzero : n ≠ 0163  requires weights : F : ℕ × ℕ → ℤ164  requires member : d ∈ divisors(n)165  shows finiteRowSums(divisors(n), divisors(n), ℤ, integerAdd, integerZero,166      integerNeg, integerMul, integerOne, divisorMatrix(F, n))(d) =167    rowDivisorSums(F, n)(d)168proof169  have ring := integers.comm_ring170  have finite := divisors.finite at n171  have naturals := divisors.subset_naturals at n172  have matrix := divisorMatrix.function at F, n with weights173  have rowValue := finiteRowSums.value at divisors(n), divisors(n), ℤ,174    integerAdd, integerZero, integerNeg, integerMul, integerOne,175      divisorMatrix(F, n), d with ring, finite, matrix, member176  have dNat := divisors.natural with member177  have dMember := naturals with d, member178  have factor := divisors.divides with member179  have rows := rowTerms.function at F, d with weights, dMember180  have target := rowDivisorSums.value at F, n, d with weights181  have inner := divisors.quotient_subset with nonzero, factor182  have innerNaturals := divisors.subset_naturals at quotientNat(n, d)183  have rowWeights := finiteRowWeights.function at divisors(n), divisors(n), ℤ,184    divisorMatrix(F, n), d with matrix, member185  have restrictedRows := restrict.domain_function with rows, innerNaturals186  have agreement : ∀ s ∈ divisors(quotientNat(n, d)),187      finiteRowWeights(divisors(n), divisors(n), ℤ, divisorMatrix(F, n), d)(s) =188        restrict(rowTerms(F, d), divisors(quotientNat(n, d)))(s)189    intros s hs190    have sMemberD := inner with s, hs191    have sMember := naturals with s, sMemberD192    have entry := finiteRowWeights.value at divisors(n), divisors(n), ℤ,193      divisorMatrix(F, n), d, s with matrix, member, sMemberD194    have characterization := dividingPairs.iff_quotient at n, d, s with nonzero,195      member196    have pairIn := characterization.backward with hs197    have inside := divisorMatrix.inside with weights, pairIn198    have termValue := rowTerms.value at F, d, s with weights, dMember199    have restricted := restrict.domain_apply with rows, innerNaturals, hs200    cc201  have vanishes : ∀ s ∈ divisors(n), ¬(s ∈ divisors(quotientNat(n, d))) →202      finiteRowWeights(divisors(n), divisors(n), ℤ, divisorMatrix(F, n), d)(s) =203        integerZero204    intros s hs outside205    have entry := finiteRowWeights.value at divisors(n), divisors(n), ℤ,206      divisorMatrix(F, n), d, s with matrix, member, hs207    have characterization := dividingPairs.iff_quotient at n, d, s with nonzero,208      member209    have notPair : ¬((d, s) ∈ dividingPairs(n))210      intro pairIn211      apply outside212      exact characterization.forward with pairIn213    have pairMember := product.pair with member, hs214    have zero := divisorMatrix.outside with weights, pairMember, notPair215    cc216  have extension := finiteRingSum.zero_extension with ring, finite, rowWeights,217    restrictedRows, inner, agreement, vanishes218  rw [rowValue, target]219  simp [divisorSum, integerSetSum]220221-- Row e of the transposed matrix sums to ∑_{d ∣ n/e} F(d, e).222theorem divisorMatrix.column (F : Set) (n : Nat) (e : Set)223  requires nonzero : n ≠ 0224  requires weights : F : ℕ × ℕ → ℤ225  requires member : e ∈ divisors(n)226  shows finiteRowSums(divisors(n), divisors(n), ℤ, integerAdd, integerZero,227      integerNeg, integerMul, integerOne, transposedMatrix(divisors(n),228        divisors(n), ℤ, divisorMatrix(F, n)))(e) =229    columnDivisorSums(F, n)(e)230proof231  have ring := integers.comm_ring232  have finite := divisors.finite at n233  have naturals := divisors.subset_naturals at n234  have matrix := divisorMatrix.function at F, n with weights235  have transposed := transposedMatrix.function at divisors(n), divisors(n), ℤ,236    divisorMatrix(F, n) with matrix237  have rowValue := finiteRowSums.value at divisors(n), divisors(n), ℤ,238    integerAdd, integerZero, integerNeg, integerMul, integerOne,239      transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)), e240        with ring, finite, transposed, member241  have eNat := divisors.natural with member242  have eMember := naturals with e, member243  have factor := divisors.divides with member244  have columns := columnTerms.function at F, e with weights, eMember245  have target := columnDivisorSums.value at F, n, e with weights246  have inner := divisors.quotient_subset with nonzero, factor247  have innerNaturals := divisors.subset_naturals at quotientNat(n, e)248  have rowWeights := finiteRowWeights.function at divisors(n), divisors(n), ℤ,249    transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)), e with250      transposed, member251  have restrictedColumns := restrict.domain_function with columns,252    innerNaturals253  have agreement : ∀ s ∈ divisors(quotientNat(n, e)),254      finiteRowWeights(divisors(n), divisors(n), ℤ,255        transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)),256          e)(s) =257        restrict(columnTerms(F, e), divisors(quotientNat(n, e)))(s)258    intros s hs259    have sMemberD := inner with s, hs260    have sMember := naturals with s, sMemberD261    have entry := finiteRowWeights.value at divisors(n), divisors(n), ℤ,262      transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)), e, s263        with transposed, member, sMemberD264    have swapped := transposedMatrix.pair at divisors(n), divisors(n), ℤ,265      divisorMatrix(F, n), s, e with matrix, sMemberD, member266    have characterization := dividingPairs.iff_quotient at n, e, s with nonzero,267      member268    have pairIn := characterization.backward with hs269    have symmetric := dividingPairs.symmetric with pairIn270    have inside := divisorMatrix.inside with weights, symmetric271    have termValue := columnTerms.value at F, e, s with weights, eMember272    have restricted := restrict.domain_apply with columns, innerNaturals, hs273    cc274  have vanishes : ∀ s ∈ divisors(n), ¬(s ∈ divisors(quotientNat(n, e))) →275      finiteRowWeights(divisors(n), divisors(n), ℤ,276        transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)),277          e)(s) = integerZero278    intros s hs outside279    have entry := finiteRowWeights.value at divisors(n), divisors(n), ℤ,280      transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)), e, s281        with transposed, member, hs282    have swapped := transposedMatrix.pair at divisors(n), divisors(n), ℤ,283      divisorMatrix(F, n), s, e with matrix, hs, member284    have characterization := dividingPairs.iff_quotient at n, e, s with nonzero,285      member286    have notPair : ¬((s, e) ∈ dividingPairs(n))287      intro pairIn288      apply outside289      have symmetric := dividingPairs.symmetric with pairIn290      exact characterization.forward with symmetric291    have pairMember := product.pair with hs, member292    have zero := divisorMatrix.outside with weights, pairMember, notPair293    cc294  have extension := finiteRingSum.zero_extension with ring, finite, rowWeights,295    restrictedColumns, inner, agreement, vanishes296  rw [rowValue, target]297  simp [divisorSum, integerSetSum]298299-- Summing by rows and by columns agrees:300-- ∑_{d ∣ n} ∑_{e ∣ n/d} F(d, e) = ∑_{e ∣ n} ∑_{d ∣ n/e} F(d, e).301theorem divisorSum.interchange (F : Set) (n : Nat)302  requires nonzero : n ≠ 0303  requires weights : F : ℕ × ℕ → ℤ304  shows divisorSum(n, rowDivisorSums(F, n)) =305    divisorSum(n, columnDivisorSums(F, n))306proof307  have ring := integers.comm_ring308  have finite := divisors.finite at n309  have naturals := divisors.subset_naturals at n310  have matrix := divisorMatrix.function at F, n with weights311  have transposed := transposedMatrix.function at divisors(n), divisors(n), ℤ,312    divisorMatrix(F, n) with matrix313  have rowsFunction := rowDivisorSums.function at F, n with weights314  have columnsFunction := columnDivisorSums.function at F, n with weights315  have restrictedRows := restrict.domain_function with rowsFunction, naturals316  have restrictedColumns := restrict.domain_function with columnsFunction,317    naturals318  have rowSums := finiteRowSums.function at divisors(n), divisors(n), ℤ,319    integerAdd, integerZero, integerNeg, integerMul, integerOne,320      divisorMatrix(F, n) with ring, finite, matrix321  have columnSums := finiteRowSums.function at divisors(n), divisors(n), ℤ,322    integerAdd, integerZero, integerNeg, integerMul, integerOne,323      transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)) with324        ring, finite, transposed325  have interchange := finiteDoubleSum.interchange with ring, finite, finite,326    matrix327  have leftAgree : ∀ d ∈ divisors(n), restrict(rowDivisorSums(F, n),328      divisors(n))(d) = finiteRowSums(divisors(n), divisors(n), ℤ, integerAdd,329        integerZero, integerNeg, integerMul, integerOne, divisorMatrix(F, n))(d)330    intros d hd331    have row := divisorMatrix.row with nonzero, weights, hd332    have restricted := restrict.domain_apply with rowsFunction, naturals, hd333    cc334  have rightAgree : ∀ e ∈ divisors(n), restrict(columnDivisorSums(F, n),335      divisors(n))(e) = finiteRowSums(divisors(n), divisors(n), ℤ, integerAdd,336        integerZero, integerNeg, integerMul, integerOne,337          transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n)))(e)338    intros e he339    have column := divisorMatrix.column with nonzero, weights, he340    have restricted := restrict.domain_apply with columnsFunction, naturals, he341    cc342  have leftSum := finiteRingSum.congr with ring, finite, restrictedRows,343    rowSums, leftAgree344  have rightSum := finiteRingSum.congr with ring, finite, restrictedColumns,345    columnSums, rightAgree346  have leftDouble : finiteDoubleSum(divisors(n), divisors(n), ℤ, integerAdd,347      integerZero, integerNeg, integerMul, integerOne, divisorMatrix(F, n)) =348    finiteRingSum(divisors(n), ℤ, integerAdd, integerZero, integerNeg,349      integerMul, integerOne, finiteRowSums(divisors(n), divisors(n), ℤ,350        integerAdd, integerZero, integerNeg, integerMul, integerOne,351          divisorMatrix(F, n)))352    unfold finiteDoubleSum353    rfl354  have rightDouble : finiteDoubleSum(divisors(n), divisors(n), ℤ, integerAdd,355      integerZero, integerNeg, integerMul, integerOne,356        transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n))) =357    finiteRingSum(divisors(n), ℤ, integerAdd, integerZero, integerNeg,358      integerMul, integerOne, finiteRowSums(divisors(n), divisors(n), ℤ,359        integerAdd, integerZero, integerNeg, integerMul, integerOne,360          transposedMatrix(divisors(n), divisors(n), ℤ, divisorMatrix(F, n))))361    unfold finiteDoubleSum362    rfl363  unfold divisorSum364  unfold integerSetSum365  cc366