The Lax-Milgram Theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We consider an 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.inner_product_space.dual can be upgraded to a continuous equivalence
is_coercive.continuous_linear_equiv_of_bilin : V ≃L[ℝ] V.
- We follow the notes of Peter Howard's Spring 2020 M612: Partial Differential Equations lecture, see[How]
The Lax-Milgram equivalence of a coercive bounded bilinear operator:
v : V,
continuous_linear_equiv_of_bilin B v is the unique element
⟪continuous_linear_equiv_of_bilin B v, w⟫ = B v w.
The Lax-Milgram theorem states that this is a continuous equivalence.