The weak operator topology in Hilbert spaces #
This file gives a few properties of the weak operator topology that are specific to operators on Hilbert spaces. This mostly involves using the FrΓ©chet-Riesz representation to convert between applications of elements of the dual and inner products with vectors in the space.
theorem
ContinuousLinearMapWOT.ext_inner_iff
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike π]
[AddCommGroup E]
[TopologicalSpace E]
[Module π E]
[NormedAddCommGroup F]
[InnerProductSpace π F]
{A : E βWOT[π]F}
{B : E βWOT[π]F}
:
theorem
ContinuousLinearMapWOT.ext_inner
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike π]
[AddCommGroup E]
[TopologicalSpace E]
[Module π E]
[NormedAddCommGroup F]
[InnerProductSpace π F]
{A : E βWOT[π]F}
{B : E βWOT[π]F}
(h : β (x : E) (y : F), inner y (A x) = inner y (B x))
:
A = B
theorem
ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike π]
[AddCommGroup E]
[TopologicalSpace E]
[Module π E]
[NormedAddCommGroup F]
[InnerProductSpace π F]
[CompleteSpace F]
{Ξ± : Type u_4}
{l : Filter Ξ±}
{f : Ξ± β E βWOT[π]F}
{A : E βWOT[π]F}
:
Filter.Tendsto f l (nhds A) β β (x : E) (y : F), Filter.Tendsto (fun (a : Ξ±) => inner y ((f a) x)) l (nhds (inner y (A x)))
The defining property of the weak operator topology: a function f
tends to
A : E βWOT[π] F
along filter l
iff βͺy, (f a) xβ«
tends to βͺy, A xβ«
along the same filter.
theorem
ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[RCLike π]
[AddCommGroup E]
[TopologicalSpace E]
[Module π E]
[NormedAddCommGroup F]
[InnerProductSpace π F]
[CompleteSpace F]
{l : Filter (E βWOT[π]F)}
{A : E βWOT[π]F}
: