Documentation

Mathlib.Analysis.InnerProductSpace.LaxMilgram

The Lax-Milgram Theorem #

We consider a 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 InnerProductSpace.continuousLinearMapOfBilin from Analysis.InnerProductSpace.Dual can be upgraded to a continuous equivalence IsCoercive.continuousLinearEquivOfBilin : V ≃L[ℝ] V.

References #

Tags #

dual, Lax-Milgram

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

Equations
Instances For
    @[simp]
    theorem IsCoercive.continuousLinearEquivOfBilin_apply {V : Type u} [NormedAddCommGroup V] [InnerProductSpace V] [CompleteSpace V] {B : V →L[] V →L[] } (coercive : IsCoercive B) (v : V) (w : V) :
    inner (coercive.continuousLinearEquivOfBilin v) w = (B v) w
    theorem IsCoercive.unique_continuousLinearEquivOfBilin {V : Type u} [NormedAddCommGroup V] [InnerProductSpace V] [CompleteSpace V] {B : V →L[] V →L[] } (coercive : IsCoercive B) {v : V} {f : V} (is_lax_milgram : ∀ (w : V), inner f w = (B v) w) :
    f = coercive.continuousLinearEquivOfBilin v