adjoint — Mathlib

English

The adjoint A† is the unique linear isometry from E to F such that ⟪Ax, y⟫ = ⟪x, A†y⟫ for all x ∈ E, y ∈ F.

Русский

Сопряжённый A† есть уникальное линейное изометрическое отображение, удовлетворяющее ⟪Ax, y⟫ = ⟪x, A†y⟫ для всех x∈E, y∈F.

LaTeX

$$$$ A^{\\dagger} : F \\to E \\quad \\text{is linear isometry with} \\quad \\langle Ax, y \\rangle = \\langle x, A^{\\dagger} y \\rangle. $$$$

Lean4

/-- The adjoint of a bounded operator `A` from a Hilbert space `E` to another Hilbert space `F`,
  denoted as `A†`. -/
def adjoint : (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E :=
  LinearIsometryEquiv.ofSurjective { adjointAux with norm_map' := adjointAux_norm } fun A =>
    ⟨adjointAux A, adjointAux_adjointAux A⟩

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