English
An element y belongs to the adjoint domain of T iff the map x ↦ ⟪y, T x⟫ is continuous on T.domain.
Русский
Элемент y принадлежит области сопряженного оператора T тогда и только тогда, когда отображение x ↦ ⟪y, T x⟫ непрерывно на T.domain.
LaTeX
$$y ∈ T†.domain ↔ Continuous ((innerₛₗ 𝕜 y).comp T.toFun)$$
Lean4
/-- The domain of the adjoint operator.
This definition is needed to construct the adjoint operator and the preferred version to use is
`T.adjoint.domain` instead of `T.adjointDomain`. -/
def adjointDomain : Submodule 𝕜 F
where
carrier := {y | Continuous ((innerₛₗ 𝕜 y).comp T.toFun)}
zero_mem' := by
rw [Set.mem_setOf_eq, LinearMap.map_zero, LinearMap.zero_comp]
exact continuous_zero
add_mem' hx hy := by rw [Set.mem_setOf_eq, LinearMap.map_add] at *; exact hx.add hy
smul_mem' a x
hx := by
rw [Set.mem_setOf_eq, LinearMap.map_smulₛₗ] at *
exact hx.const_smul (conj a)
