Symmetry transports along a unitary

Open

BookProof.ChapterUnitaryTransport.transportOp_symmetric

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

spectral-theorytimepiece

If $A$ is symmetric on $D$ , the conjugated operator $W A W^{-1}$ is symmetric on $W(D)$ .

\langle A\psi,\phi\rangle=\langle\psi,A\phi\rangle \quad\Longrightarrow\quad \langle WAW^{-1} y, z\rangle=\langle y, WAW^{-1} z\rangle.

Formalization Note. IsSymmetricOn is the platform pairing identity.

Preamble

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

Formal statement

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

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportOp_symmetric

View graph