Documentation

Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

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} :
A = B ↔ βˆ€ (x : E) (y : F), inner y (A x) = inner y (B x)
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} :
l ≀ nhds A ↔ βˆ€ (x : E) (y : F), Filter.map (fun (T : E β†’WOT[π•œ]F) => inner y (T x)) l ≀ nhds (inner y (A x))