Extending weak continuity from a dense family of tests #
This is the density step in the weak-continuity argument for
prop:leray-hopf-limit.
theorem
CKN.Leray.continuousOn_inner_of_dense_tests
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{T M : ℝ}
(hM : 0 ≤ M)
(v : ℝ → E)
(D : Set E)
(hD : Dense D)
(hbound : ∀ t ∈ Set.Icc 0 T, ‖v t‖ ≤ M)
(hcont : ∀ w ∈ D, ContinuousOn (fun (t : ℝ) => inner ℝ (v t) w) (Set.Icc 0 T))
(w : E)
:
ContinuousOn (fun (t : ℝ) => inner ℝ (v t) w) (Set.Icc 0 T)
A uniform norm bound extends continuity of Hilbert pairings from a dense family of tests to every test.