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.

Main results

• ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto: a function f : α → E →WOT[𝕜] F tends to 𝓝 A if and only if fun a ↦ ⟪y, (f a) x⟫_𝕜 tends to 𝓝 ⟪y, A x⟫_𝕜 for all x : E, y : F. Also included are the corresponding characterizations of continuity.
• The adjoint operation is continuous in the weak operator topology, declared as an instance of ContinuousStar (F →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 B : E →WOT[𝕜] F} (h : ∀ (x : E) (y : F), inner 𝕜 y (A x) = inner 𝕜 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 B : E →WOT[𝕜] F} : A = B ↔ ∀ (x : E) (y : F), inner 𝕜 y (A x) = inner 𝕜 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 : α) => 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))

theorem ContinuousLinearMapWOT.continuousWithinAt_iff {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α} : ContinuousWithinAt f s a ↔ ∀ (x : E) (y : F), ContinuousWithinAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s a

theorem ContinuousLinearMapWOT.continuousAt_iff {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α} : ContinuousAt f a ↔ ∀ (x : E) (y : F), ContinuousAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) a

theorem ContinuousLinearMapWOT.continuousOn_iff {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} : ContinuousOn f s ↔ ∀ (x : E) (y : F), ContinuousOn (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s

theorem ContinuousLinearMapWOT.continuous_iff {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} : Continuous f ↔ ∀ (x : E) (y : F), Continuous fun (x_1 : α) => inner 𝕜 y ((f x_1) x)

theorem ContinuousLinearMapWOT.continuousWithinAt {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α} : (∀ (x : E) (y : F), ContinuousWithinAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s a) → ContinuousWithinAt f s a

Alias of the reverse direction of ContinuousLinearMapWOT.continuousWithinAt_iff.

theorem ContinuousLinearMapWOT.continuousWithinAt_inner_apply {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α} : ContinuousWithinAt f s a → ∀ (x : E) (y : F), ContinuousWithinAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s a

Alias of the forward direction of ContinuousLinearMapWOT.continuousWithinAt_iff.

theorem ContinuousLinearMapWOT.continuousOn_inner_apply {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} : ContinuousOn f s → ∀ (x : E) (y : F), ContinuousOn (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s

Alias of the forward direction of ContinuousLinearMapWOT.continuousOn_iff.

theorem ContinuousLinearMapWOT.continuousOn {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} : (∀ (x : E) (y : F), ContinuousOn (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) s) → ContinuousOn f s

Alias of the reverse direction of ContinuousLinearMapWOT.continuousOn_iff.

theorem ContinuousLinearMapWOT.continuousAt {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α} : (∀ (x : E) (y : F), ContinuousAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) a) → ContinuousAt f a

Alias of the reverse direction of ContinuousLinearMapWOT.continuousAt_iff.

theorem ContinuousLinearMapWOT.continuousAt_inner_apply {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α} : ContinuousAt f a → ∀ (x : E) (y : F), ContinuousAt (fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) a

Alias of the forward direction of ContinuousLinearMapWOT.continuousAt_iff.

theorem ContinuousLinearMapWOT.continuous {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} : (∀ (x : E) (y : F), Continuous fun (x_1 : α) => inner 𝕜 y ((f x_1) x)) → Continuous f

Alias of the reverse direction of ContinuousLinearMapWOT.continuous_iff.

theorem ContinuousLinearMapWOT.continuous_inner_apply {𝕜 : 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} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} : Continuous f → ∀ (x : E) (y : F), Continuous fun (x_1 : α) => inner 𝕜 y ((f x_1) x)

Alias of the forward direction of ContinuousLinearMapWOT.continuous_iff.

@[implicit_reducible]

noncomputable instance ContinuousLinearMapWOT.instStarRingId {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : StarRing (F →WOT[𝕜] F)

Equations

• ContinuousLinearMapWOT.instStarRingId = ContinuousLinearMapWOT.equiv.starRing

theorem ContinuousLinearMapWOT.star_apply {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : F →WOT[𝕜] F) (x : F) : (star A) x = (star A.toCLM) x

instance ContinuousLinearMapWOT.instStarModuleId {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : StarModule 𝕜 (F →WOT[𝕜] F)

instance ContinuousLinearMapWOT.instContinuousStarId {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : ContinuousStar (F →WOT[𝕜] F)