mathlib documentation


The Lax-Milgram Theorem #

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 #

Tags #

dual, Lax-Milgram

noncomputable def is_coercive.continuous_linear_equiv_of_bilin {V : Type u} [inner_product_space V] [complete_space V] {B : V →L[] 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.

theorem is_coercive.unique_continuous_linear_equiv_of_bilin {V : Type u} [inner_product_space V] [complete_space V] {B : V →L[] V →L[] } (coercive : is_coercive B) {v f : V} (is_lax_milgram : ∀ (w : V), has_inner.inner f w = (B v) w) :