# mathlib3documentation

analysis.inner_product_space.lax_milgram

# 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 V over ℝ equipped with a bounded bilinear form B : V →L[ℝ] V →L[ℝ] ℝ.

Recall that a bilinear form B : V →L[ℝ] V →L[ℝ] ℝ is coercive iff ∃ 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 inner_product_space.continuous_linear_map_of_bilin from analysis.inner_product_space.dual can be upgraded to a continuous equivalence is_coercive.continuous_linear_equiv_of_bilin : V ≃L[ℝ] V.

## References #

• We follow the notes of Peter Howard's Spring 2020 M612: Partial Differential Equations lecture, see[How]

## Tags #

dual, Lax-Milgram

theorem is_coercive.bounded_below {V : Type u} {B : V →L[] } (coercive : is_coercive B) :
(C : ), 0 < C (v : V),
theorem is_coercive.antilipschitz {V : Type u} {B : V →L[] } (coercive : is_coercive B) :
theorem is_coercive.ker_eq_bot {V : Type u} {B : V →L[] } (coercive : is_coercive B) :
theorem is_coercive.closed_range {V : Type u} {B : V →L[] } (coercive : is_coercive B) :
theorem is_coercive.range_eq_top {V : Type u} {B : V →L[] } (coercive : is_coercive B) :
noncomputable def is_coercive.continuous_linear_equiv_of_bilin {V : Type u} {B : V →L[] } (coercive : is_coercive B) :

The Lax-Milgram equivalence of a coercive bounded bilinear operator: for all v : V, continuous_linear_equiv_of_bilin B v is the unique element V such that ⟪continuous_linear_equiv_of_bilin B v, w⟫ = B v w. The Lax-Milgram theorem states that this is a continuous equivalence.

Equations
@[simp]
theorem is_coercive.unique_continuous_linear_equiv_of_bilin {V : Type u} {B : V →L[] } (coercive : is_coercive B) {v f : V} (is_lax_milgram : (w : V), = (B v) w) :