Transported operator on a pulled vector

Proved

BookProof.ChapterUnitaryTransport.transportOp_apply

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

spectral-theorytimepiece

On a vector pulled back from the original domain, the transported operator $W A W^{-1}$ is just $W$ applied to $A$ .

(W A W^{-1})(W x) = W(A x).

Formalization Note. transportEquiv is the restriction of $W$ to $D$ .

Preamble

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

Formal statement

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

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportOp_apply

View graph