The Lax-Milgram Theorem #
We consider a Hilbert space
equipped with a bounded bilinear form
B : V →L[ℝ] V →L[ℝ] ℝ.
Recall that a bilinear form
B : V →L[ℝ] V →L[ℝ] ℝ is coercive
∃ C, (0 < C) ∧ ∀ u, C * ‖u‖ * ‖u‖ ≤ B u u.
Under the hypothesis that
B is coercive we prove the Lax-Milgram theorem:
that is, the map
Analysis.InnerProductSpace.Dual can be upgraded to a continuous equivalence
IsCoercive.continuousLinearEquivOfBilin : V ≃L[ℝ] V.
- We follow the notes of Peter Howard's Spring 2020 M612: Partial Differential Equations lecture, see[howard]
The Lax-Milgram equivalence of a coercive bounded bilinear operator:
v : V,
continuousLinearEquivOfBilin B v is the unique element
continuousLinearEquivOfBilin B v, w⟫ = B v w.
The Lax-Milgram theorem states that this is a continuous equivalence.