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 {𝕜 : 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), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜) : A = B

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), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜

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 : α) => ⟪y, (f a) x⟫_𝕜) l (nhds ⟪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) => ⟪y, T x⟫_𝕜) l ≤ nhds ⟪y, A x⟫_𝕜