feat: star structures on ContinuousLinearMapWOT (#39163)

In particular, with these instances it makes sense to consider the `StarSubalgebra.topologicalClosure` of some `S : StarSubalgebra 𝕜 (F →WOT[𝕜] F)`.

Author: j-loreaux

Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean

@@ -5,6 +5,8 @@ Authors: Frédéric Dupuis
 -/
 module
 
+public import Mathlib.Algebra.Star.TransferInstance
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import Mathlib.Analysis.InnerProductSpace.Dual
 public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 
@@ -14,6 +16,14 @@ public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 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)`.
 -/
 
 public section
@@ -30,18 +40,57 @@ lemma ext_inner {A B : E →WOT[𝕜] F} (h : ∀ x y, ⟪y, A x⟫_𝕜 = ⟪y,
   rw [ContinuousLinearMapWOT.ext_iff]
   exact fun x => ext_inner_left 𝕜 fun y => h x y
 
+variable [CompleteSpace F]
+
 open Filter in
 /-- 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. -/
-lemma tendsto_iff_forall_inner_apply_tendsto [CompleteSpace F] {α : Type*} {l : Filter α}
+lemma tendsto_iff_forall_inner_apply_tendsto {α : Type*} {l : Filter α}
     {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} :
     Tendsto f l (𝓝 A) ↔ ∀ x y, Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜) := by
   simp_rw [tendsto_iff_forall_dual_apply_tendsto]
   exact .symm <| forall_congr' fun _ ↦
     Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl
 
-lemma le_nhds_iff_forall_inner_apply_le_nhds [CompleteSpace F] {l : Filter (E →WOT[𝕜] F)}
+lemma le_nhds_iff_forall_inner_apply_le_nhds {l : Filter (E →WOT[𝕜] F)}
     {A : E →WOT[𝕜] F} : l ≤ 𝓝 A ↔ ∀ x y, l.map (fun T => ⟪y, T x⟫_𝕜) ≤ 𝓝 (⟪y, A x⟫_𝕜) :=
   tendsto_iff_forall_inner_apply_tendsto (f := id)
 
+lemma continuousWithinAt_iff {α : Type*} [TopologicalSpace α]
+    {f : α → E →WOT[𝕜] F} {s : Set α} {a : α} :
+    ContinuousWithinAt f s a ↔ ∀ x y, ContinuousWithinAt (⟪y, f · x⟫_𝕜) s a :=
+  tendsto_iff_forall_inner_apply_tendsto
+
+lemma continuousAt_iff {α : Type*} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α} :
+    ContinuousAt f a ↔ ∀ x y, ContinuousAt (⟪y, f · x⟫_𝕜) a :=
+  tendsto_iff_forall_inner_apply_tendsto
+
+lemma continuousOn_iff {α : Type*} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} :
+    ContinuousOn f s ↔ ∀ x y, ContinuousOn (⟪y, f · x⟫_𝕜) s := by
+  simp_rw [ContinuousOn, forall_comm (α := E), forall_comm (α := F), continuousWithinAt_iff]
+
+lemma continuous_iff {α : Type*} [TopologicalSpace α] {f : α → E →WOT[𝕜] F} :
+    Continuous f ↔ ∀ x y, Continuous (⟪y, f · x⟫_𝕜) := by
+  simp_rw [continuous_iff_continuousAt, forall_comm (α := E), forall_comm (α := F),
+    continuousAt_iff]
+
+@[fun_prop] alias ⟨continuousWithinAt_inner_apply, continuousWithinAt⟩ := continuousWithinAt_iff
+@[fun_prop] alias ⟨continuousOn_inner_apply, continuousOn⟩ := continuousOn_iff
+@[fun_prop] alias ⟨continuousAt_inner_apply, continuousAt⟩ := continuousAt_iff
+@[fun_prop] alias ⟨continuous_inner_apply, continuous⟩ := continuous_iff
+
+noncomputable instance : StarRing (F →WOT[𝕜] F) := equiv.starRing
+
+lemma star_apply (A : F →WOT[𝕜] F) (x : F) : star A x = star (toCLM A) x := rfl
+
+instance : StarModule 𝕜 (F →WOT[𝕜] F) := equiv.starModule 𝕜
+
+instance : ContinuousStar (F →WOT[𝕜] F) where
+  continuous_star := by
+    simp_rw [continuous_iff, star_apply, ContinuousLinearMap.star_eq_adjoint,
+      ContinuousLinearMap.adjoint_inner_right, coe_toCLM]
+    rw [forall_comm]
+    conv in ⟪_, _⟫_𝕜 => rw [← inner_conj_symm, ← RCLike.star_def]
+    fun_prop
+
 end ContinuousLinearMapWOT