Weak lower semicontinuity of Hilbert norms #
This is the Hilbert-space lower-semicontinuity step used for the slice and
dissipation bounds in prop:leray-hopf-limit.
theorem
CKN.Leray.norm_le_of_tendsto_inner_and_uniform_bound
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{α : Type u_2}
{l : Filter α}
[l.NeBot]
{v : α → E}
{a : E}
{C : ℝ}
(hC : 0 ≤ C)
(hbound : ∀ᶠ (x : α) in l, ‖v x‖ ≤ C)
(hinner : Filter.Tendsto (fun (x : α) => inner ℝ (v x) a) l (nhds (‖a‖ ^ 2)))
:
A weakly convergent family with uniformly bounded norms has a limit with the same norm bound.