# 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 #

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

## Tags #

dual, Lax-Milgram

theorem IsCoercive.bounded_below {V : Type u} [] [] {B : V →L[] } (coercive : ) :
∃ (C : ), 0 < C ∀ (v : V),
theorem IsCoercive.antilipschitz {V : Type u} [] [] {B : V →L[] } (coercive : ) :
∃ (C : NNReal),
theorem IsCoercive.ker_eq_bot {V : Type u} [] [] {B : V →L[] } (coercive : ) :
theorem IsCoercive.isClosed_range {V : Type u} [] [] {B : V →L[] } (coercive : ) :
@[deprecated IsCoercive.isClosed_range]
theorem IsCoercive.closed_range {V : Type u} [] [] {B : V →L[] } (coercive : ) :

Alias of IsCoercive.isClosed_range.

theorem IsCoercive.range_eq_top {V : Type u} [] [] {B : V →L[] } (coercive : ) :
def IsCoercive.continuousLinearEquivOfBilin {V : Type u} [] [] {B : V →L[] } (coercive : ) :

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
• coercive.continuousLinearEquivOfBilin =
Instances For
@[simp]
theorem IsCoercive.continuousLinearEquivOfBilin_apply {V : Type u} [] [] {B : V →L[] } (coercive : ) (v : V) (w : V) :
coercive.continuousLinearEquivOfBilin v, w⟫_ = (B v) w
theorem IsCoercive.unique_continuousLinearEquivOfBilin {V : Type u} [] [] {B : V →L[] } (coercive : ) {v : V} {f : V} (is_lax_milgram : ∀ (w : V), f, w⟫_ = (B v) w) :
f = coercive.continuousLinearEquivOfBilin v