The determinant of the least-common-multiple matrix
Lax426240.LcmDeterminant · concepts/Lax426240/LcmDeterminant.lean · lax-426240
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Smith (1875) evaluated the determinant of the matrix with entries , and more generally of when is a Dirichlet convolution: it equals . The matrix of least common multiples is not of that form, but writes it as with and , and is a Dirichlet convolution with by Möbius inversion. Hence
so that the determinant is . The three statements are the determinant in terms of , the closed form of , and the closed form of the determinant.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.LinearAlgebra.Matrix.Determinant.Basic |
| 2 | import Mathlib.NumberTheory.ArithmeticFunction.Moebius |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The determinant of the least-common-multiple matrix |
| 7 | type: theorem |
| 8 | --- |
| 9 | Smith (1875) evaluated the determinant of the matrix with entries |
| 10 | , and more generally of when is a |
| 11 | Dirichlet convolution: it equals . The matrix of least |
| 12 | common multiples is not of that form, but |
| 13 | writes it as with and |
| 14 | , and is a Dirichlet convolution with |
| 15 | by Möbius inversion. Hence |
| 16 | |
| 17 | |
| 18 | |
| 19 | |
| 20 | so that the determinant is . The |
| 21 | three statements are the determinant in terms of , the closed form of , |
| 22 | and the closed form of the determinant. |
| 23 | -/ |
| 24 | |
| 25 | namespace Lax426240.LcmDeterminant |
| 26 | |
| 27 | open Finset |
| 28 | open scoped ArithmeticFunction.Moebius |
| 29 | |
| 30 | /-- The `N × N` matrix with entries `lcm(i, j)` for `1 ≤ i, j ≤ N`, over `ℚ`. -/ |
| 31 | def 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`. -/ |
| 36 | noncomputable def g (n : ℕ) : ℚ := |
| 37 | ∑ x ∈ n.divisorsAntidiagonal, (μ x.1 : ℚ) * (1 / x.2) |
| 38 | |
| 39 | /-- `det (lcm(i,j)) = (N!)² ∏_{k ≤ N} g(k)`. -/ |
| 40 | axiom 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`. -/ |
| 47 | axiom 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)`. -/ |
| 51 | axiom 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 | |
| 56 | end Lax426240.LcmDeterminant |
| 57 |
Builds on
none
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments