Operator polar decomposition A = U |A| (Sub-dev III)

For an operator A on a finite-dimensional inner product space, A = U |A|, where |A| = (A⋆A)^{1/2} is the modulus and U is a partial isometry with initial space (ker A)ᗮ and ker U = ker A. When A is invertible, U is unitary and U = A |A|⁻¹.

• RCLike route (E →ₗ[𝕜] E, ℝ and ℂ): |A| built from the spectral square root (TauCeti.IsPositive.sqrt). Serves Davis's real-symmetric application directly.
• CFC route / headline (E →L[ℂ] E): |A| = CFC.abs A literally, transported across the definitional LinearMap ↔ ContinuousLinearMap adjoint bridge.

Sources: Horn & Johnson, Matrix Analysis 2nd ed., Thm 7.3.1 (statement; A = UQ, Q = (A⋆A)^{1/2}, U unitary, unique iff nonsingular). Conway, A Course in Functional Analysis 2nd ed., VI.3.9 (the partial-isometry construction A = U|A|, ker U = ker A — the route mathlib can follow, since HJ's SVD proof route is unavailable: mathlib has no SVD factorization).

The three polar factors, and how they relate

Documented here because none of the three named the others, so a reviewer could not tell a designed hierarchy from three independent attempts. The separating hypotheses are the carrier and whether the modulus is invertible:

• TauCeti.polarFactor, in Polar/Decomposition.lean — square E →ₗ[𝕜] E, RCLike, finite dimension; a genuine unitary factor.
• TauCeti.polarPartial, in Polar/PartialIsometry.lean — rectangular E →L[𝕜] F over RCLike, no invertibility assumed; a partial isometry.
• TauCeti.polarIsometryOfIsUnitModulus, in Polar/Isometry.lean — rectangular E →L[𝕜] F over RCLike and the modulus a unit; then the factor is an isometry.

Read down the list: dropping finite dimension costs the unitary and leaves a partial isometry; adding invertibility of the modulus buys it back as an isometry. That is the whole hierarchy.

The modulus |A| (RCLike, LinearMap)

There are two canonical realizations of the same rectangular source modulus:

• TauCeti.operatorAbs, below, is RCLike-generic and finite-dimensional, built from the spectral square root of A⋆A;
• ContinuousLinearMap.modulus is dimension-free, built from the real continuous functional calculus on bounded operators.

Both accept a rectangular map E → F and return an endomorphism of the source E. Polar.CFCBridge proves that converting the finite-dimensional construction to a bounded operator gives ContinuousLinearMap.modulus.

The name is operatorAbs, not abs: a bare abs collides with the lattice absolute value that |·| denotes in Lean, while modulus is the bounded-operator spelling.

noncomputable def TauCeti.operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : E →ₗ[𝕜] E

The modulus |A| = (A⋆A)^{1/2} of an operator, via the spectral square root of the positive operator A⋆A. HJ 7.3.1 (Q = (A⋆A)^{1/2}).

Equations

• TauCeti.operatorAbs A = ⋯.sqrt

@[simp]

theorem TauCeti.isPositive_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (operatorAbs A).IsPositive

The modulus is a positive operator, being a positive square root.

theorem TauCeti.operatorAbs_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : operatorAbs A ∘ₗ operatorAbs A = LinearMap.adjoint A ∘ₗ A

|A|² = A⋆A.

@[simp]

theorem TauCeti.norm_operatorAbs_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : ‖(operatorAbs A) x‖ = ‖A x‖

The polar norm identity ‖|A| x‖ = ‖A x‖. Not in HJ (SVD route); this is the seed of the isometry route (Conway VI.3.9).

theorem TauCeti.ker_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (operatorAbs A).ker = A.ker

ker |A| = ker A.

theorem TauCeti.range_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (operatorAbs A).range = A.kerᗮ

range |A| = (ker A)ᗮ — the initial space of the polar factor.

theorem TauCeti.operatorAbs_apply_mem_orthogonal_ker {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : (operatorAbs A) x ∈ A.kerᗮ

Elementwise form of range_operatorAbs: every value of the modulus lies in the initial space.

theorem TauCeti.operatorAbs_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : operatorAbs (-A) = operatorAbs A

The modulus does not see a sign. |-A| = |A|, because the two Gram operators (-A)⋆(-A) and A⋆A are literally the same operator and the positive square root of a positive operator is unique.

theorem TauCeti.operatorAbs_adjoint_of_normal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hnormal : LinearMap.adjoint A ∘ₗ A = A ∘ₗ LinearMap.adjoint A) : operatorAbs (LinearMap.adjoint A) = operatorAbs A

A normal operator and its adjoint have the same modulus. Normality says the two Gram operators A⋆A and AA⋆ agree, and |A⋆| is by definition the positive square root of the second.

The polar factor U and the decomposition

noncomputable def TauCeti.operatorAbsRestrict {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : ↥A.kerᗮ ≃ₗ[𝕜] ↥A.kerᗮ

The restriction of the modulus |A| to (ker A)ᗮ = range |A|, as a linear automorphism of (ker A)ᗮ — the invertible core of |A|, which the polar factor inverts.

Equations

• TauCeti.operatorAbsRestrict A = LinearEquiv.ofBijective ((TauCeti.operatorAbs A).restrict ⋯) ⋯

noncomputable def TauCeti.polarFactor {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : E →ₗ[𝕜] E

The polar factor U of A: the partial isometry that is the isometry |A| x ↦ A x on range |A| = (ker A)ᗮ, extended by 0 on ker A. Conway VI.3.9.

Equations

• TauCeti.polarFactor A = A ∘ₗ A.kerᗮ.subtype ∘ₗ ↑(TauCeti.operatorAbsRestrict A).symm ∘ₗ ↑A.kerᗮ.orthogonalProjectionOnto

@[simp]

theorem TauCeti.polarFactor_apply_operatorAbs_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) (x : E) : (polarFactor A) ((operatorAbs A) x) = A x

The defining property of the polar factor: U (|A| x) = A x.

theorem TauCeti.polar_decomposition {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : A = polarFactor A ∘ₗ operatorAbs A

Polar decomposition A = U |A|. Conway VI.3.9; HJ 7.3.1.

theorem TauCeti.ker_polarFactor {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : (polarFactor A).ker = A.ker

ker U = ker A.

theorem TauCeti.range_polarFactor {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : (polarFactor A).range = A.range

range U = range A — the final space of the polar factor.

theorem TauCeti.norm_polarFactor_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} {x : E} (hx : x ∈ A.kerᗮ) : ‖(polarFactor A) x‖ = ‖x‖

U restricted to range |A| = (ker A)ᗮ is isometric.

theorem TauCeti.isPartialIsometry_polarFactor {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : IsPartialIsometry (polarFactor A)

U is a partial isometry.

Invertible case: U is unitary

noncomputable def TauCeti.polarUnitaryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : IsUnit A) : E ≃ₗᵢ[𝕜] E

When A is invertible, |A| is invertible and the polar factor is the unitary U = A |A|⁻¹, packaged as a LinearIsometryEquiv. HJ 7.3.1(b) (U uniquely determined if A nonsingular).

Equations

• TauCeti.polarUnitaryEquiv hA = { toLinearEquiv := LinearEquiv.ofBijective (TauCeti.polarFactor A) ⋯, norm_map' := ⋯ }

@[simp]

theorem TauCeti.coe_polarUnitaryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : IsUnit A) : ↑↑↑(polarUnitaryEquiv hA) = polarFactor A

The bundled polar unitary acts as the chosen one.

theorem TauCeti.polar_decomposition_of_isUnit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : IsUnit A) : A = ↑↑↑(polarUnitaryEquiv hA) ∘ₗ operatorAbs A

Polar decomposition for an operator with invertible modulus: A = U |A| with U unitary.

General square case: a kernel-completed unitary

Even for a singular A, the partial isometry polarFactor A extends to a genuine unitary E ≃ₗᵢ[𝕜] E — map the initial space (ker A)ᗮ by polarFactor A (isometrically onto range A) and complete ker A isometrically onto (range A)ᗮ (equal dimensions by rank–nullity). The identity A = U |A| survives, and U is a true unitary; this is the factor the orthogonal-Procrustes alignment argument needs (polarUnitaryEquiv above requires invertibility).

The completion is a choice, not a canonical construction. When ker A ≠ ⊥ any unitary from ker A onto (range A)ᗮ completes polarFactor A, and LinearIsometry.extend merely selects one; only the restriction to (ker A)ᗮ is determined by A. Hence the name choosePolarUnitary rather than polarUnitary: the invertible case, where the unitary factor really is unique, is polarUnitaryEquiv above.

Users who need only some unitary factor should prefer exists_polar_decomposition_unitary, which states the theorem without committing to the selection.

noncomputable def TauCeti.polarIsometryOnOrthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : ↥A.kerᗮ →ₗᵢ[𝕜] E

The polar factor restricted to (ker A)ᗮ, its initial space, where it is a genuine linear isometry.

Equations

• TauCeti.polarIsometryOnOrthogonal A = { toLinearMap := TauCeti.polarFactor A ∘ₗ A.kerᗮ.subtype, norm_map' := ⋯ }

noncomputable def TauCeti.choosePolarUnitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : E ≃ₗᵢ[𝕜] E

A selected polar unitary (general square case). A kernel-completed unitary extending polarFactor A; unitary for every A, singular or not.

Not canonical when A is singular — see the section note above.

Equations

• TauCeti.choosePolarUnitary A = LinearIsometryEquiv.ofSurjective (TauCeti.polarIsometryOnOrthogonal A).extend ⋯

@[simp]

theorem TauCeti.choosePolarUnitary_apply_operatorAbs_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) (x : E) : (choosePolarUnitary A) ((operatorAbs A) x) = A x

The chosen polar unitary satisfies the defining identity U (|A| x) = A x. It is a choice -- see choosePolarUnitary -- but every choice satisfies this.

theorem TauCeti.polar_decomposition_choosePolarUnitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : A = ↑↑↑(choosePolarUnitary A) ∘ₗ operatorAbs A

Polar decomposition with a unitary factor (general square case), A = U |A| at the selected witness U = choosePolarUnitary A.

For the statement that does not name a witness, use exists_polar_decomposition_unitary.

theorem TauCeti.exists_polar_decomposition_unitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : ∃ (U : E ≃ₗᵢ[𝕜] E), A = ↑↑↑U ∘ₗ operatorAbs A

Polar decomposition with a unitary factor, existential form.

This is the honest general-case statement: every square operator on a finite-dimensional space factors as a unitary times its modulus. It says nothing about which unitary, which is the point — for singular A the factor is not unique. choosePolarUnitary provides a witness when a concrete one is needed.

theorem TauCeti.operatorAbs_comm_of_normal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hnormal : LinearMap.adjoint A ∘ₗ A = A ∘ₗ LinearMap.adjoint A) : A ∘ₗ operatorAbs A = operatorAbs A ∘ₗ A

The modulus of a normal finite-dimensional operator commutes with the operator. This is the finite RCLike substitute for the corresponding CFC commutation theorem.

theorem TauCeti.polarFactor_eq_of_isUnit_eq_comp_positive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A H : E →ₗ[𝕜] E} (hA : IsUnit A) (U : E ≃ₗᵢ[𝕜] E) (hH : H.IsPositive) (hdecomp : A = ↑U.toLinearEquiv ∘ₗ H) : polarFactor A = ↑U.toLinearEquiv

Uniqueness of the unitary factor in an invertible polar decomposition. If A = U H with U unitary and H positive, then the canonical polar factor of A is U.

theorem TauCeti.polarFactor_adjoint_of_isUnit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : IsUnit A) : polarFactor (LinearMap.adjoint A) = LinearMap.adjoint (polarFactor A)

For an invertible operator the polar factor of the adjoint is the adjoint of the polar factor: from A = U|A| one gets A⋆ = U⋆ ∘ (U|A|U⋆) with the conjugated modulus positive, and polar uniqueness identifies the factors.