English
As a reformulation of weak convergence, Tendsto f l (nhds A) is equivalent to the pointwise convergence of all inner products with any fixed pair of vectors.
Русский
Переформулировка слабой сходимости:u Tendsto f l (nhds A) эквивалентно покдажному сходству всех скалярных произведений с фиксированной парой векторов.
LaTeX
$$$ \\text{Tendsto}(f,i) \\leftrightarrow \\forall x,y,\n \\text{Tendsto}(a \\mapsto \\langle y, f(a) x \\rangle)\\ l\\ (\\mathcal{N}\\langle y, A x \\rangle)$$$
Lean4
/-- 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 tendsto_iff_forall_inner_apply_tendsto [CompleteSpace F] {α : 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, ← InnerProductSpace.toDual_apply]
exact .symm <| forall_congr' fun _ ↦ Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl
