Extension of bounded bilinear maps from dense linear cores #
A bilinear map bounded through two dense linear embeddings extends uniquely to a continuous bilinear map on the complete target spaces.
theorem
CKN.Leray.regularised_bilinear_dense_extension
{V : Type u_1}
{W : Type u_2}
{X : Type u_3}
{Y : Type u_4}
{Z : Type u_5}
[AddCommGroup V]
[Module ℂ V]
[AddCommGroup W]
[Module ℂ W]
[NormedAddCommGroup X]
[NormedSpace ℂ X]
[NormedAddCommGroup Y]
[NormedSpace ℂ Y]
[NormedAddCommGroup Z]
[NormedSpace ℂ Z]
[CompleteSpace Z]
(eV : V →ₗ[ℂ] X)
(eW : W →ₗ[ℂ] Y)
(heV : DenseRange ⇑eV)
(heW : DenseRange ⇑eW)
(B : V →ₗ[ℂ] W →ₗ[ℂ] Z)
(C : ℝ)
(hC : 0 ≤ C)
(hBound : ∀ (v : V) (w : W), ‖(B v) w‖ ≤ C * ‖eV v‖ * ‖eW w‖)
:
A bounded bilinear map on two dense linear cores has a continuous bilinear extension with the same norm bound.