Norm determinant of a linear map

Given a rectangular matrix $T$, it is common to talk about $\sqrt{det(T^{H}T)}$, where $T^{H}$ is the conjugate transpose of $T$, as a generalization to the determinant of a square matrix. It is the $m$-dimensional volume factor for linear maps $\mathbb{R}^m \to \mathbb{R}^n$. It is given various names in the literature:

• "Jacobian" (definition 3.4 of [EG25]), in the context of volume factor for a non-linear map. However, we choose to reserve this name for the matrix consisting of derivatives.
• "Gram determinant", which is already used by Matrix.gram, and it is often referring to $det(T^{H}T)$ without the square root.
• "Nonnegative determinant" (definition 1 of [YTI06]).

Without a standardized name, we give a descriptive name LinearMap.normDet to reflect its definition and show that it is a generalization of ‖(f : LinearMap 𝕜 U U).det‖ (See LinearMap.normDet_eq_norm_det). We also construct this on linear maps between inner product spaces instead of matrices, and allow the codomain to have infinite dimension.

Main definition

• LinearMap.normDet : the norm determinant of a linear map.

Main result

• ContinuousLinearMap.normDet_sq and LinearMap.normDet_sq: The square of f.normDet equals to the determinant of f.adjoint ∘ₗ f.
• LinearMap.normDet_sq_eq_det_gram: The square of LinearMap.normDet equals to the determinant of the Gram matrix formed by vectors mapped from an orthonormal basis.
• LinearMap.normDet_eq_prod_singularValues: LinearMap.normDet equals to the product of singular values.
• LinearMap.hausdorffMeasure_image: LinearMap.normDet is the volume factor for Hausdorff measure.

noncomputable def LinearMap.normDet {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : ℝ

The norm determinant of a linear map f : U →ₗ[𝕜] V is defined as the norm of the determinant of the square matrix representing the linear map U →ₗ[𝕜] f.range over a pair of orthonormal basis of equal dimensions. (See LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict for using arbitrary orthonormal basis)

If such basis doesn't exist (e.g. the map is not injective), the norm determinant is zero. (See LinearMap.normDet_eq_zero_iff_ker_ne_bot)

Equations

• f.normDet = if h : Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range) then ‖((LinearMap.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis h.some.toBasis) f.rangeRestrict).det‖ else 0

theorem LinearMap.normDet_nonneg {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : 0 ≤ f.normDet

theorem LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (f : U →ₗ[𝕜] V) (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 ↥f.range) : f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

LinearMap.normDet is well-defined under any pair of orthonormal basis.

theorem LinearMap.normDet_eq_zero_iff_ker_ne_bot {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {f : U →ₗ[𝕜] V} : f.normDet = 0 ↔ f.ker ≠ ⊥

LinearMap.normDet vanishes iff the map is not injective.

theorem LinearMap.normDet_eq_zero_iff_rank_range_ne {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {f : U →ₗ[𝕜] V} : f.normDet = 0 ↔ Module.finrank 𝕜 ↥f.range ≠ Module.finrank 𝕜 U

theorem LinearMap.normDet_ne_zero_tfae {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : [f.normDet ≠ 0, f.ker = ⊥, Module.finrank 𝕜 ↥f.range = Module.finrank 𝕜 U, Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE

theorem LinearMap.normDet_eq_zero_tfae {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : [f.normDet = 0, f.ker ≠ ⊥, Module.finrank 𝕜 ↥f.range ≠ Module.finrank 𝕜 U, Module.finrank 𝕜 ↥f.range < Module.finrank 𝕜 U, IsEmpty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range), ¬Function.Injective ⇑f].TFAE

theorem LinearMap.normDet_eq_norm_det_toMatrix {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (f : U →ₗ[𝕜] V) (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 V) : f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

LinearMap.normDet can be calculated with any pair of orthonormal basis if the domain and the codomain have equal dimension.

theorem LinearMap.normDet_eq_norm_det {𝕜 : Type u_1} {U : Type u_2} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] (f : U →ₗ[𝕜] U) : f.normDet = ‖LinearMap.det f‖

LinearMap.normDet equals the norm of LinearMap.det for an endomorphism.

@[simp]

theorem LinearIsometry.normDet_eq_one {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗᵢ[𝕜] V) : f.normDet = 1

LinearMap.normDet of a linear isometry is 1.

@[simp]

theorem LinearMap.normDet_id {𝕜 : Type u_1} {U : Type u_2} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] : id.normDet = 1

@[simp]

theorem LinearMap.normDet_subtype {𝕜 : Type u_1} {U : Type u_2} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] (p : Submodule 𝕜 U) : p.subtype.normDet = 1

@[simp]

theorem LinearMap.normDet_of_subsingleton {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [Subsingleton U] (f : U →ₗ[𝕜] V) : f.normDet = 1

@[simp]

theorem LinearMap.normDet_zero {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] : normDet 0 = 0 ^ Module.finrank 𝕜 U

@[simp]

theorem LinearMap.normDet_smul {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) (c : 𝕜) : (c • f).normDet = ‖c‖ ^ Module.finrank 𝕜 U * f.normDet

@[simp]

theorem LinearMap.normDet_neg {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : (-f).normDet = f.normDet

theorem ContinuousLinearMap.normDet_sq {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (f : U →L[𝕜] V) : ↑((↑f).normDet ^ 2) = (adjoint f ∘SL f).det

The square of f.normDet equals the determinant of f.adjoint ∘L f.

theorem LinearMap.normDet_sq {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V) : ↑(f.normDet ^ 2) = LinearMap.det (adjoint f ∘ₗ f)

The square of f.normDet equals the determinant of f.adjoint ∘ₗ f when the codomain is finite dimensional.

theorem LinearMap.normDet_sq_eq_det_gram {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (f : U →ₗ[𝕜] V) (b : OrthonormalBasis ι 𝕜 U) : ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun (x : ι) => f (b x)).det

The square of f.normDet equals the determinant of the Gram matrix formed by vectors mapped from an orthonormal basis.

theorem LinearMap.normDet_comp {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (f : U →ₗ[𝕜] V) (g : V →ₗ[𝕜] W) : (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

theorem LinearMap.normDet_comp_of_finrank_eq {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V) (g : V →ₗ[𝕜] W) (h : Module.finrank 𝕜 U = Module.finrank 𝕜 V) : (g ∘ₗ f).normDet = g.normDet * f.normDet

@[simp]

theorem LinearMap.normDet_codRestrict {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {p : Submodule 𝕜 V} {f : U →ₗ[𝕜] V} (h : ∀ (c : U), f c ∈ p) : (codRestrict p f h).normDet = f.normDet

theorem LinearMap.normDet_eq_prod_singularValues {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V) : f.normDet = ∏ i ∈ Finset.range (Module.finrank 𝕜 U), f.singularValues i

theorem LinearMap.normDet_eq_abs_det {U : Type u_5} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] (f : U →ₗ[ℝ] U) : f.normDet = |LinearMap.det f|

theorem LinearMap.hausdorffMeasure_image {U : Type u_5} {V : Type u_6} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] (f : U →ₗ[ℝ] V) (s : Set U) : (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ U)) (⇑f '' s) = ENNReal.ofReal f.normDet * (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ U)) s

Using Hausdorff measure with the domain dimension, the volume of the image is scaled by LinearMap.normDet.

theorem LinearMap.euclideanHausdorffMeasure_image {U : Type u_5} {V : Type u_6} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] (f : U →ₗ[ℝ] V) (s : Set U) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (⇑f '' s) = ENNReal.ofReal f.normDet * (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) s

Using Euclidean Hausdorff measure with the domain dimension, the volume of the image is scaled by LinearMap.normDet.

theorem LinearMap.euclideanHausdorffMeasure_image_eq_normDet_mul_volume {U : Type u_5} {V : Type u_6} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] (f : U →ₗ[ℝ] V) (s : Set U) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (⇑f '' s) = ENNReal.ofReal f.normDet * MeasureTheory.volume s

The volume of the image measured by Euclidean Hausdorff measure is equal to the Lebesgue measure scaled by LinearMap.normDet.