feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map

[wwylele]

This is the volume factor of a linear map

---

I have encountered the expression sqrt(det(T' * T)) a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it.

Zulip thread #Is there code for X? > (norm of) "determinant" of map between inner product spaces

One motivation to define this is to state volume formula under transformations. From Measure theory and fine properties of functions:

• Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$, or in Lean, μHE[n] (L '' A) = L.normDet * volume A
• Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f^{-1}{y}) d\mathcal{H}^n(y)$, where $J f$ is the normDet of the rectangular Jacobian matrix

AI usage disclosure: AI was used in the following parts

• searching for related literature for an appropriate name
• generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me.

[github-actions]

PR summary be85740951

Import changes exceeding 2%

%	File
+14.11%	Mathlib.Analysis.InnerProductSpace.GramMatrix

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.InnerProductSpace.GramMatrix	2140	2442	+302 (+14.11%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.InnerProductSpace.GramMatrix	302
Mathlib.Analysis.InnerProductSpace.NormDet (new file)	2443

---

Declarations diff

+ _root_.ContinuousLinearMap.normDet_sq
+ _root_.LinearIsometry.normDet_eq_one
+ linearIndependent_of_det_gram_ne_zero
+ normDet
+ normDet_codRestrict
+ normDet_comp
+ normDet_comp_of_finrank_eq
+ normDet_eq
+ normDet_eq_norm_det
+ normDet_eq_zero_iff_ker_ne_bot
+ normDet_id
+ normDet_neg
+ normDet_nonneg
+ normDet_of_subsingleton
+ normDet_smul
+ normDet_sq
+ normDet_sq_eq_det_gram
+ normDet_subtype
+ normDet_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
7421	1	backward.isDefEq

Current commit 81ce2de7ae
Reference commit be85740951

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Copilot]

Pull request overview

Adds a new mathlib API entry for the commonly used “rectangular determinant” quantity sqrt(det(Tᴴ * T)), implemented for linear maps between inner product spaces as LinearMap.normDet.

Changes:

• Introduce LinearMap.normDet : (U →ₗ[𝕜] V) → ℝ (via a determinant of the range-restriction matrix in orthonormal bases).
• Prove core properties: basis-independence, vanishing criterion via kernel, compatibility with LinearMap.det for endomorphisms, and the “square equals det(adjoint ∘ f)” lemma (for ContinuousLinearMap and LinearMap).
• Add literature references and wire the new file into the main Mathlib import tree.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.

File	Description
docs/references.bib	Adds bibliography entries cited by the new module docstring.
Mathlib/Analysis/InnerProductSpace/NormDet.lean	New definition LinearMap.normDet plus lemmas relating it to determinants of adjoint ∘ f.
Mathlib.lean	Imports the new NormDet module.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.