Strong continuity transports

Proved

BookProof.ChapterUnitaryTransport.tendsto_transportUnitary

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

spectral-theorytimepiece

If $t\mapsto U_t x$ is continuous at $0$ for every $x\in H$ , then $t\mapsto W U_t W^{-1} y$ is continuous at $0$ for every $y\in K$ .

U_t x \to x \quad\Longrightarrow\quad W U_t W^{-1} y \to y \qquad (t\to 0).

Formalization Note. $W$ is continuous, so it preserves the limit.

Preamble

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

Formal statement

theorem BookProof.ChapterUnitaryTransport.tendsto_transportUnitary {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (U : ℝ → H ≃ₗᵢ[ℂ] H) (h : ∀ x : H, Filter.Tendsto (fun t : ℝ => U t x) (nhds 0) (nhds x)) (y : K) : Filter.Tendsto (fun t : ℝ => transportUnitary W (U t) y) (nhds 0) (nhds y) := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem tendsto_transportUnitary

View graph