Theorems · Definition · functional analysis

IsCoercive.continuousLinearEquivOfBilin

• 1000+ list: Lax–Milgram theorem

{V : Type u} →
  [inst : NormedAddCommGroup V] →
    [inst_1 : InnerProductSpace ℝ V] → [CompleteSpace V] → {B : V →L[ℝ] V →L[ℝ] ℝ} → 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.

Defined in

Mathlib.Analysis.InnerProductSpace.LaxMilgram

Cited by

2 results in Mathlib

Foundations

Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace