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[howard]

Tags

dual, Lax-Milgram

theorem IsCoercive.bounded_below {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(InnerProductSpace.continuousLinearMapOfBilin B) v‖

theorem IsCoercive.antilipschitz {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : ∃ (C : NNReal), 0 < C ∧ AntilipschitzWith C ⇑(InnerProductSpace.continuousLinearMapOfBilin B)

theorem IsCoercive.ker_eq_bot {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : LinearMap.ker (InnerProductSpace.continuousLinearMapOfBilin B) = ⊥

theorem IsCoercive.isClosed_range {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : IsClosed ↑(LinearMap.range (InnerProductSpace.continuousLinearMapOfBilin B))

@[deprecated IsCoercive.isClosed_range]

theorem IsCoercive.closed_range {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : IsClosed ↑(LinearMap.range (InnerProductSpace.continuousLinearMapOfBilin B))

Alias of IsCoercive.isClosed_range.

theorem IsCoercive.range_eq_top {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : LinearMap.range (InnerProductSpace.continuousLinearMapOfBilin B) = ⊤

def IsCoercive.continuousLinearEquivOfBilin {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) : V ≃L[ℝ] V

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 = ContinuousLinearEquiv.ofBijective (InnerProductSpace.continuousLinearMapOfBilin B) ⋯ ⋯

@[simp]

theorem IsCoercive.continuousLinearEquivOfBilin_apply {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) (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 f : V} (is_lax_milgram : ∀ (w : V), inner f w = (B v) w) : f = coercive.continuousLinearEquivOfBilin v