Adjoint domain is the unitary image

Proved

BookProof.ChapterUnitaryTransport.transport_adjointDomain

by hitme development · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

The adjoint domain of $W A W^{-1}$ is the image under $W$ of the adjoint domain of $A$ .

\mathcal{D}((WAW^{-1})^*) = W\bigl(\mathcal{D}(A^*)\bigr).

Formalization Note. adjointDomain is the set of vectors for which $\psi\mapsto\langle A\psi,\phi\rangle$ is represented by an inner product.

Preamble

import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace

Formal statement

theorem BookProof.ChapterUnitaryTransport.transport_adjointDomain {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (D : Submodule ℂ H) (A : D →ₗ[ℂ] H) : adjointDomain (transportDomain W D) (transportOp W D A) = W '' adjointDomain D A := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transport_adjointDomain

View graph