Conjugating an unbounded operator by a unitary

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #64(i), the first of the three pieces that row records itself as waiting on.

★★★ LinearPMap.conjIsometry — U T U⁻¹ for a unitary U and a partially defined operator T, with domain U(dom T), and the two transfers that make it worth having:

• ★★★ LinearPMap.adjoint_conjIsometry — the adjoint conjugates: (U T U⁻¹)† = U T† U⁻¹, hence ★★★ IsSelfAdjoint.conjIsometry — a unitary conjugate of a self-adjoint operator is self-adjoint;
• ★★★ LinearPMap.spectrum_conjIsometry — the spectrum is unchanged, through ★★ LinearPMap.resolventSet_conjIsometry.

Mathlib has LinearMap.compPMap (a bounded map after a partial one, same domain) and LinearPMap.comp (two partial ones, with a domain condition), and nothing that moves an operator across a unitary — which is what a change of representation is. Unitary equivalence is the standard way an unbounded operator becomes tractable: the free Hamiltonian is multiplication by a symbol in the momentum representation and a differential operator in the position one, and this is the bridge.

What makes it short

The ≤ order on LinearPMap does the work. Rather than computing the adjoint's domain through adjointDomain's continuity condition, conjIsometry U T† is shown to be a formal adjoint of conjIsometry U T — a four-step inner-product computation, since a unitary preserves inner products — so IsFormalAdjoint.le_adjoint gives one inclusion. The other comes from the same lemma applied to U⁻¹, through ★ LinearPMap.conjIsometry_symm_conjIsometry (conjugation is an involution) and ★ LinearPMap.conjIsometry_mono (it is monotone), and le_antisymm closes it.

Honest scope

⚠️ Unitary, not merely isometric. U is a LinearIsometryEquiv: the inverse has to exist for the conjugate to be defined on all of U(dom T), and surjectivity is what makes the domain dense again. A non-surjective isometry gives a compression, not a conjugate, and nothing here covers it.

⚠️ Same field. U is 𝕜-linear, so this is not the antiunitary (conjugate-linear) case, which reverses the order of products and is a genuinely different statement.

⚠️ No functional calculus. That the conjugate has the same functional calculus, or that unitary equivalence preserves the spectral measure, is not claimed — only the resolvent set, which is what the spectrum is defined from here.

References: DiagonalOperator.lean (LinearPMap.IsResolventAt, LinearPMap.spectrum), MultiplicationOperator.lean (the multiplication operators this is for), Mathlib/Analysis/InnerProductSpace/LinearPMap.lean (adjoint, IsFormalAdjoint); specs/BACKLOG.md #64.

The conjugate

theorem LinearPMap.symm_mem_of_mem_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (p : Submodule 𝕜 E) {y : F} (hy : y ∈ Submodule.map (↑U.toLinearEquiv) p) : U.symm y ∈ p

The image of a submodule under a unitary, as a set, is the set image — the bridge every membership step below goes through.

def LinearPMap.conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) : F →ₗ.[𝕜] F

U T U⁻¹, with domain U(dom T).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearPMap.conjIsometry_domain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) : (conjIsometry U T).domain = Submodule.map (↑U.toLinearEquiv) T.domain

theorem LinearPMap.conjIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) (y : ↥(conjIsometry U T).domain) : ↑(conjIsometry U T) y = U (↑T ⟨U.symm ↑y, ⋯⟩)

theorem LinearPMap.mem_conjIsometry_domain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) {x : E} (hx : x ∈ T.domain) : U x ∈ (conjIsometry U T).domain

Membership in the conjugate's domain, in the form every proof below wants.

theorem LinearPMap.conjIsometry_apply_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) (x : ↥T.domain) : ↑(conjIsometry U T) ⟨U ↑x, ⋯⟩ = U (↑T x)

The conjugate's value at an image point, which is the computational form.

theorem LinearPMap.conjIsometry_apply_of_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) (x : ↥T.domain) (y : ↥(conjIsometry U T).domain) (hxy : ↑y = U ↑x) : ↑(conjIsometry U T) y = U (↑T x)

The conjugate's value at any element whose coordinate is an image point — the form that avoids rewriting under a membership proof.

theorem LinearPMap.conjIsometry_symm_conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) : conjIsometry U.symm (conjIsometry U T) = T

★ Conjugation is an involution, which is what gives the second half of the adjoint identity.

theorem LinearPMap.conjIsometry_conjIsometry_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (X : F →ₗ.[𝕜] F) : conjIsometry U (conjIsometry U.symm X) = X

The other direction of the involution, which the adjoint identity closes with.

theorem LinearPMap.conjIsometry_mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) {S T : E →ₗ.[𝕜] E} (h : S ≤ T) : conjIsometry U S ≤ conjIsometry U T

★ Conjugation is monotone for the extension order.

theorem LinearPMap.dense_conjIsometry_domain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) (hT : Dense ↑T.domain) : Dense ↑(conjIsometry U T).domain

The conjugate's domain is dense when the original's is, because a unitary is a homeomorphism.

The spectrum is unchanged

def LinearPMap.conjCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (S : E →L[𝕜] E) : F →L[𝕜] F

The conjugate of a bounded operator, as a bounded operator.

Equations

• LinearPMap.conjCLM U S = (↑↑U ∘SL S) ∘SL ↑↑U.symm

@[simp]

theorem LinearPMap.conjCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (S : E →L[𝕜] E) (y : F) : (conjCLM U S) y = U (S (U.symm y))

theorem LinearPMap.IsResolventAt.conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) {T : E →ₗ.[𝕜] E} {z : 𝕜} {S : E →L[𝕜] E} (h : T.IsResolventAt z S) : (LinearPMap.conjIsometry U T).IsResolventAt z (conjCLM U S)

The conjugated resolvent is a resolvent of the conjugate.

theorem LinearPMap.resolventSet_conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) : (conjIsometry U T).resolventSet = T.resolventSet

★★ The resolvent set is unchanged by a unitary conjugation.

theorem LinearPMap.spectrum_conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) : (conjIsometry U T).spectrum = T.spectrum

★★★ The spectrum is unchanged by a unitary conjugation — a change of representation does not move the spectrum.

The adjoint conjugates

theorem LinearPMap.IsFormalAdjoint.conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (U : E ≃ₗᵢ[𝕜] F) {T S : E →ₗ.[𝕜] E} (h : T.IsFormalAdjoint S) : (LinearPMap.conjIsometry U T).IsFormalAdjoint (LinearPMap.conjIsometry U S)

The conjugate of a formal adjoint is a formal adjoint of the conjugate: four inner products, each step a unitary moving across.

theorem LinearPMap.adjoint_conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (U : E ≃ₗᵢ[𝕜] F) (T : E →ₗ.[𝕜] E) (hT : Dense ↑T.domain) : (conjIsometry U T).adjoint = conjIsometry U T.adjoint

★★★ The adjoint conjugates. (U T U⁻¹)† = U T† U⁻¹.

theorem IsSelfAdjoint.conjIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →ₗ.[𝕜] E} (hT : IsSelfAdjoint T) (U : E ≃ₗᵢ[𝕜] F) : IsSelfAdjoint (LinearPMap.conjIsometry U T)

★★★ A unitary conjugate of a self-adjoint operator is self-adjoint.