The polar factorization of an injective map #
Let A : E → F be an injective linear map between finite-dimensional real or complex inner
product spaces. Its modulus |A| = √(A† A) (LinearMap.operatorAbs) has the same pointwise norms
as A, so it is injective, hence invertible. The map W = A |A|⁻¹ is then an isometric
embedding of E into F, and A = W |A|. In other words A factors as an isometric embedding,
the orthonormalization of A, after an invertible positive coordinate change on its source.
The isometric factor is the canonical polar factor LinearMap.polarFactor, bundled as an
isometry. It has the same range as A, and the factorization is unique among factorizations
A = W C with W isometric and C positive.
A lower frame bound ‖x‖ ≤ c ‖A x‖ controls the inverse coordinate change:
‖|A|⁻¹ y‖ ≤ c ‖y‖. Consequently, composing with |A|⁻¹ on the right costs at most a factor c
in every unitarily invariant seminorm. This is how estimates proved for isometric embeddings
transfer to arbitrary injective maps, such as a basis of a trial subspace in subspace
perturbation theory.
Main declarations #
LinearMap.operatorAbsEquiv: the modulus of an injective map, as a linear automorphism.LinearMap.isUnit_operatorAbs: the modulus of an injective map is invertible.LinearMap.polarIsometry: the canonical polar factorA |A|⁻¹of an injective map, as an isometric embedding.LinearMap.polarFactor_mul_self_of_adjoint_eq_neg: the polar factor of an injective skew-adjoint endomorphism is a complex structure,U² = -1.LinearMap.coe_polarIsometry: the isometric factor isLinearMap.polarFactor, so the factorizationA = W |A|comes from the polar-factor API.LinearMap.range_polarIsometry: the isometric factor has the same range asA.LinearMap.IsPositive.eq_operatorAbs_of_comp_eq,LinearMap.eq_polarIsometry_of_comp_eq: uniqueness of the factorization, including the invertible endomorphism caseA = U PwithUunitary andPpositive.LinearMap.norm_operatorAbsEquiv_symm_apply_le: a lower frame bound forAbounds|A|⁻¹.TauCeti.UnitarilyInvariantSeminorm.map_comp_operatorAbsEquiv_symm_le: the resulting cost of composing with|A|⁻¹in a unitarily invariant seminorm.
References #
- R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Theorem 7.3.1.
- The invertible unitary uniqueness statement also appears as
TauCeti.polarFactor_eq_of_isUnit_eq_comp_positiveinForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.leanof the AIQ-Kitware DKPS formalization (Apache-2.0; Copyright (c) 2026 Kitware, Inc.; Jon Crall and Claude Opus 4.8).
The modulus |A| of an injective map A, as a linear automorphism of the source.
Instances For
The modulus of an injective map is invertible.
The isometric polar factor A |A|⁻¹ of an injective map A: the canonical polar factor
A.polarFactor, bundled as an isometric embedding.
Instances For
The isometric polar factor of A has the same range as A.
Uniqueness of the positive factor. If A = W C with W an isometric embedding and C
positive, then C = A.operatorAbs. In particular, this identifies the positive factor in an
invertible unitary-positive factorization A = U P.
Uniqueness of the isometric factor. If A = W C with W an isometric embedding and C
positive, then W is the isometric polar factor of A. For an injective endomorphism factored
as A = U P with U a linear isometric equivalence and P positive, applying this to
U.toLinearIsometry gives U.toLinearMap = A.polarFactor via polarIsometry_toLinearMap.
Polar factors of skew-adjoint maps. The canonical polar factor U of an injective
skew-adjoint endomorphism A squares to -1: it is an orthogonal complex structure.
Inverse-coordinate bound. If A satisfies the lower frame bound ‖x‖ ≤ c ‖A x‖, then the
inverse of its modulus satisfies ‖|A|⁻¹ y‖ ≤ c ‖y‖. For ε > 0, the frame bound
ε ‖x‖ ≤ ‖A x‖ is the case c = ε⁻¹.
Composition cost of the inverse modulus. If the injective map A : E → F satisfies the
lower frame bound ‖x‖ ≤ c ‖A x‖, then N (B |A|⁻¹) ≤ c N(B) for every map B : E → G and every
unitarily invariant seminorm N.