English
Let A,B be m×n matrices. For i,j∈{1,…,n}, the inner product of the i-th row of A and the j-th row of B equals the (i,j)-entry of the product A^H B.
Русский
Пусть A,B — матрицы размера m×n. Для i,j ∈ {1,…,n} скалярное произведение i-й строки A и j-й строки B равно элементу (i,j) произведения A^H B.
LaTeX
$$$\\\\langle A_i, B_j \\\\rangle = (A^{\\mathrm{H}} B)_{i j}.$$$
Lean4
/-- Given a sequence of continuous linear maps which converges pointwise and for which the
domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map
is a *continuous* linear map as well.
This actually works for any *countably generated* filter instead of `atTop : Filter ℕ`,
but the proof ultimately goes back to sequences. -/
protected def continuousLinearMapOfTendsto (hq : WithSeminorms q) [T2Space F] {l : Filter α} [l.IsCountablyGenerated]
[l.NeBot] (g : α → E →SL[σ₁₂] F) {f : E → F} (h : Tendsto (fun n x ↦ g n x) l (𝓝 f)) : E →SL[σ₁₂] F
where
toLinearMap := linearMapOfTendsto _ _ h
cont := by
-- Since the filter `l` is countably generated and nontrivial, we can find a sequence
-- `u : ℕ → α` that tends to `l`. By considering `g ∘ u` instead of `g`, we can thus assume
-- that `α = ℕ` and `l = atTop`
rcases l.exists_seq_tendsto with
⟨u, hu⟩
-- We claim that the limit is continuous because it's a limit of an equicontinuous family.
-- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness.
refine (h.comp hu).continuous_of_equicontinuous (hq.banach_steinhaus ?_).equicontinuous
intro k x
rw [tendsto_pi_nhds] at h
exact (((hq.continuous_seminorm k).tendsto _).comp <| (h x).comp hu).bddAbove_range
