norm_map_iff_adjoint_comp_self — Mathlib

English

Let H and K be inner product spaces over 𝕜 and let u: H →L[𝕜] K be a bounded linear map. Then u preserves norms for every x ∈ H (i.e., ∥u x∥ = ∥x∥ for all x) if and only if the operator u satisfies u* u = Id_H (i.e., adjoint u composed with u is the identity on H).

Русский

Пусть H и K — пространства с скалярным произведением над 𝕜, и пусть u: H →L[𝕜] K. Тогда ∥u x∥ = ∥x∥ для каждого x ∈ H тогда и только тогда, когда u^* u = Id_H.

LaTeX

$$$\forall x\in H:\; \|u x\| = \|x\| \quad\Leftrightarrow\quad u^{*} u = \mathrm{Id}_H$$$

Lean4

theorem norm_map_iff_adjoint_comp_self (u : H →L[𝕜] K) : (∀ x : H, ‖u x‖ = ‖x‖) ↔ adjoint u ∘L u = 1 := by
  rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_map_iff_adjoint_comp_self]

Похожие утверждения