Continuity, adjoints, one-dimensional values, and orthogonal extensions of the Jacobian normDet

For finite-dimensional real inner product spaces U and V, the m-dimensional Jacobian LinearMap.normDet of a linear map U →L[ℝ] V, m = dim U, depends continuously on the map. This follows from normDet² = det (A† A) (ContinuousLinearMap.normDet_sq). Consequently, near an injective linear map the Jacobian is controlled up to any factor τ > 1, uniformly with the antilipschitz constant.

Between spaces of equal finite dimension, a linear map and its adjoint have the same Jacobian. Consequently the Jacobian of the adjoint of a surjective map is the Jacobian of its restriction to the orthogonal complement of the kernel; this is the Jacobian of the coarea formula.

Extending a linear map T : U → V to the Euclidean product ℝ × U by sending the new direction to a unit vector orthogonal to the range of T does not change the Jacobian. This is the linear algebra behind cones: for t > 0, the Jacobian of (t, u) ↦ t • ψ u for a parametrization ψ of a piece of the unit sphere is tᵐ times the Jacobian of ψ.

The Jacobian of the linear normal graph x ↦ (A x, x) of a functional A is sqrt (1 + ‖A‖²): its Gram matrix in an orthonormal basis is a rank-one perturbation of the identity.

Main declarations

• ContinuousLinearMap.continuous_normDet: the Jacobian normDet is continuous.
• LinearMap.normDet_eq_norm_apply_one: for a map from ℝ, the Jacobian is the norm of the image of 1.
• LinearMap.normDet_adjoint: between spaces of equal dimension, the adjoint has the same Jacobian.
• LinearMap.normDet_adjoint_eq_normDet_comp_subtype: the Jacobian of the adjoint of a surjective map is the Jacobian of its restriction to the orthogonal complement of the kernel.
• LinearMap.normDet_adjoint_pos_iff: the Jacobian of the adjoint is positive exactly for surjective maps.
• ContinuousLinearMap.normDet_adjoint_eq_norm: the Jacobian of the adjoint of a linear functional is its norm.
• LinearMap.normDet_coprod_of_orthogonal: the Jacobian of a sum of maps with orthogonal ranges on a Euclidean product is the product of their Jacobians.
• ContinuousLinearMap.exists_ball_antilipschitzWith_normDet_le: around an injective linear map there is a ball with a uniform antilipschitz constant on which normDet varies by a factor at most τ.
• LinearMap.normDet_toSpanSingleton_coprod: an orthogonal unit extension of a linear map has the same Jacobian.
• ContinuousLinearMap.normDet_normalGraphL: the Jacobian of a linear normal graph.

theorem LinearMap.normDet_eq_norm_apply_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : ℝ →ₗ[ℝ] V) : A.normDet = ‖A 1‖

The one-dimensional geometric Jacobian of a linear map is the norm of the image of 1.

theorem LinearMap.normDet_adjoint {𝕜 : Type u_2} {U : Type u_3} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (f : U →ₗ[𝕜] W) (h : Module.finrank 𝕜 U = Module.finrank 𝕜 W) : (adjoint f).normDet = f.normDet

Between spaces of the same finite dimension, a linear map and its adjoint have the same Jacobian normDet. The dimension hypothesis is necessary: an injective map into a larger space has positive Jacobian, while its adjoint has a nontrivial kernel.

theorem LinearMap.normDet_adjoint_eq_normDet_comp_subtype {𝕜 : Type u_2} {U : Type u_3} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (f : U →ₗ[𝕜] W) (hf : Function.Surjective ⇑f) : (adjoint f).normDet = (f ∘ₗ f.kerᗮ.subtype).normDet

The Jacobian of the adjoint of a surjective linear map is the Jacobian of the restriction of the map to the orthogonal complement of its kernel. This restriction is a linear isomorphism onto the codomain.

theorem LinearMap.normDet_adjoint_pos_iff {𝕜 : Type u_2} {U : Type u_3} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] {f : U →ₗ[𝕜] W} : 0 < (adjoint f).normDet ↔ Function.Surjective ⇑f

The Jacobian of the adjoint of a linear map is positive exactly when the map is surjective.

theorem LinearMap.normDet_coprod_of_orthogonal {𝕜 : Type u_2} {U : Type u_3} {W : Type u_4} {V : Type u_5} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (A : U →ₗ[𝕜] V) (B : W →ₗ[𝕜] V) (horth : ∀ (u : U) (w : W), inner 𝕜 (A u) (B w) = 0) : (A.coprod B ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (U × W))).normDet = A.normDet * B.normDet

The norm determinant of (u, w) ↦ A u + B w on the Euclidean product is the product of the norm determinants of A and B when their ranges are orthogonal. The codomain need not be finite dimensional.

theorem ContinuousLinearMap.continuous_normDet {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : Continuous fun (A : U →L[ℝ] V) => (↑A).normDet

The m-dimensional Jacobian normDet of a linear map U →L[ℝ] V, m = dim U, depends continuously on the map.

theorem ContinuousLinearMap.exists_ball_antilipschitzWith_normDet_le {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (B : U →L[ℝ] V) (hB : Function.Injective ⇑B) {τ : ℝ} (hτ : 1 < τ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∃ (K : NNReal), ∀ (C : U →L[ℝ] V), dist C B < ρ → AntilipschitzWith K ⇑C ∧ (↑C).normDet ≤ τ * (↑B).normDet ∧ (↑B).normDet ≤ τ * (↑C).normDet

Around an injective linear map B there is a ball on which the antilipschitz constant is uniform and the Jacobian varies by a factor at most τ: every C within distance ρ of B is K-antilipschitz, and C.normDet and B.normDet agree up to the factor τ.

theorem LinearMap.normDet_toSpanSingleton_coprod {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {e : V} (he : ‖e‖ = 1) {T : U →ₗ[ℝ] V} (hT : ∀ (u : U), inner ℝ e (T u) = 0) : ((toSpanSingleton ℝ V e).coprod T ∘ₗ ↑(WithLp.linearEquiv 2 ℝ (ℝ × U))).normDet = T.normDet

Extending T : U →ₗ[ℝ] V to the Euclidean product WithLp 2 (ℝ × U) by a unit vector e orthogonal to the range of T, (a, u) ↦ a • e + T u, does not change the Jacobian normDet.

theorem ContinuousLinearMap.normDet_normalGraphL {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] (A : U →L[ℝ] ℝ) : (↑A.normalGraphL).normDet = √(1 + ‖A‖ ^ 2)

The geometric Jacobian of the linear normal graph x ↦ (A x, x) is sqrt (1 + ‖A‖²).

theorem ContinuousLinearMap.normDet_adjoint_eq_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (A : U →L[ℝ] ℝ) : (↑(adjoint A)).normDet = ‖A‖

The Jacobian of the adjoint of a linear functional is its norm. This is the coarea Jacobian of a real-valued map, the norm of its gradient.