The determinant of the least-common-multiple matrix

Lax426240.LcmDeterminant · concepts/Lax426240/LcmDeterminant.lean · lax-426240

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Smith (1875) evaluated the determinant of the N×NN \times N matrix with entries gcd(i,j)\gcd(i, j), and more generally of f(gcd(i,j))f(\gcd(i,j)) when f=g1f = g * 1 is a Dirichlet convolution: it equals kNg(k)\prod_{k \le N} g(k). The matrix of least common multiples is not of that form, but lcm(i,j)gcd(i,j)=ij\mathrm{lcm}(i,j)\gcd(i,j) = ij writes it as DSDD\,S\,D with D=diag(1,,N)D = \mathrm{diag}(1, \dots, N) and Sij=1/gcd(i,j)S_{ij} = 1/\gcd(i,j), and 1/m1/m is a Dirichlet convolution g1g * 1 with g=μ(1/)g = \mu * (1/\cdot) by Möbius inversion. Hence

    det(lcm(i,j))i,jN=(N!)2kNg(k),g(n)=ab=nμ(a)b=1npn(1p),\det\big(\mathrm{lcm}(i,j)\big)_{i,j \le N} = (N!)^2 \prod_{k \le N} g(k), \qquad g(n) = \sum_{ab = n} \frac{\mu(a)}{b} = \frac{1}{n}\prod_{p \mid n}(1 - p),

    so that the determinant is N!kNpk(1p)N! \prod_{k \le N} \prod_{p \mid k} (1 - p). The three statements are the determinant in terms of gg, the closed form of gg, and the closed form of the determinant.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
    2import Mathlib.NumberTheory.ArithmeticFunction.Moebius
    3
    4/-!
    5---
    6title: The determinant of the least-common-multiple matrix
    7type: theorem
    8---
    9Smith (1875) evaluated the determinant of the N×NN \times N matrix with entries
    10gcd(i,j)\gcd(i, j), and more generally of f(gcd(i,j))f(\gcd(i,j)) when f=g1f = g * 1 is a
    11Dirichlet convolution: it equals kNg(k)\prod_{k \le N} g(k). The matrix of least
    12common multiples is not of that form, but lcm(i,j)gcd(i,j)=ij\mathrm{lcm}(i,j)\gcd(i,j) = ij
    13writes it as DSDD\,S\,D with D=diag(1,,N)D = \mathrm{diag}(1, \dots, N) and
    14Sij=1/gcd(i,j)S_{ij} = 1/\gcd(i,j), and 1/m1/m is a Dirichlet convolution g1g * 1 with
    15g=μ(1/)g = \mu * (1/\cdot) by Möbius inversion. Hence
    16
    17det(lcm(i,j))i,jN=(N!)2kNg(k),g(n)=ab=nμ(a)b=1npn(1p),\det\big(\mathrm{lcm}(i,j)\big)_{i,j \le N} = (N!)^2 \prod_{k \le N} g(k), \qquad g(n) = \sum_{ab = n} \frac{\mu(a)}{b} = \frac{1}{n}\prod_{p \mid n}(1 - p),
    18
    19
    20so that the determinant is N!kNpk(1p)N! \prod_{k \le N} \prod_{p \mid k} (1 - p). The
    21three statements are the determinant in terms of gg, the closed form of gg,
    22and the closed form of the determinant.
    23-/
    24
    25namespace Lax426240.LcmDeterminant
    26
    27open Finset
    28open scoped ArithmeticFunction.Moebius
    29
    30/-- The `N × N` matrix with entries `lcm(i, j)` for `1 ≤ i, j ≤ N`, over `ℚ`. -/
    31def lcmMatrix (N : ℕ) : Matrix (Fin N) (Fin N) ℚ :=
    32 fun i j => (Nat.lcm ((i : ℕ) + 1) ((j : ℕ) + 1) : ℚ)
    33
    34/-- The Dirichlet inverse-image of `1/n` under convolution with `1`:
    35`g(n) = ∑_{ab = n} μ(a) / b`. -/
    36noncomputable def g (n : ℕ) : ℚ :=
    37 ∑ x ∈ n.divisorsAntidiagonal, (μ x.1 : ℚ) * (1 / x.2)
    38
    39/-- `det (lcm(i,j)) = (N!)² ∏_{k ≤ N} g(k)`. -/
    40axiom det_lcmMatrix (N : ℕ) :
    41 (lcmMatrix N).det
    42 = (∏ i : Fin N, (((i : ℕ) + 1 : ℕ) : ℚ))
    43 * (∏ i : Fin N, (((i : ℕ) + 1 : ℕ) : ℚ))
    44 * ∏ i : Fin N, g ((i : ℕ) + 1)
    45
    46/-- `g(n) = (1/n) ∏_{p ∣ n} (1 − p)` for `n ≠ 0`. -/
    47axiom g_eq (n : ℕ) (hn : n ≠ 0) :
    48 g n = (1 / (n : ℚ)) * ∏ p ∈ n.primeFactors, (1 - (p : ℚ))
    49
    50/-- `det (lcm(i,j)) = N! ∏_{k ≤ N} ∏_{p ∣ k} (1 − p)`. -/
    51axiom det_lcmMatrix_closed (N : ℕ) :
    52 (lcmMatrix N).det
    53 = (∏ i : Fin N, (((i : ℕ) + 1 : ℕ) : ℚ))
    54 * ∏ i : Fin N, ∏ p ∈ ((i : ℕ) + 1).primeFactors, (1 - (p : ℚ))
    55
    56end Lax426240.LcmDeterminant
    57
    Show ProofShow ProofShow Proof

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…