Existence and uniqueness form of Lax--Milgram

Mathlib's Lax--Milgram theorem is packaged as IsCoercive.continuousLinearEquivOfBilin: a coercive continuous bilinear form B : V →L[ℝ] V →L[ℝ] ℝ induces a continuous linear equivalence V ≃L[ℝ] V sending u to the Riesz representative of the functional v ↦ B u v.

The PDE roadmap's energy-method lane needs the corresponding variational-solution API: given a represented forcing functional v ↦ ⟪F, v⟫, there is a unique u satisfying B u v = ⟪F, v⟫ for every test vector v. This file records that direct existence/uniqueness form without changing Mathlib's theorem or introducing any PDE-specific bundled structure.

Main declarations

• IsCoercive.solutionOfInner: the solution of the variational equation with forcing represented by F.
• IsCoercive.apply_self_nonneg: coercive forms have nonnegative diagonal.
• IsCoercive.apply_solutionOfInner_eq_inner: the defining variational identity.
• IsCoercive.eq_solutionOfInner: uniqueness of a vector satisfying the variational identity.
• IsCoercive.existsUnique_forall_eq_inner: the combined existence-and-uniqueness theorem.
• IsCoercive.solutionOfFunctional and IsCoercive.existsUnique_forall_eq: the same API for an arbitrary continuous linear functional, using Fréchet--Riesz representation.

The proof is a thin wrapper around Mathlib's IsCoercive.continuousLinearEquivOfBilin and its characteristic identity.

theorem IsCoercive.apply_self_nonneg {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (v : V) : 0 ≤ (B v) v

A coercive form has nonnegative diagonal.

noncomputable def IsCoercive.solutionOfInner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : V

The solution supplied by Lax--Milgram for a represented forcing functional.

For F : V, solutionOfInner hB F is the unique vector u satisfying B u v = ⟪F, v⟫ for every v.

Equations

• hB.solutionOfInner F = hB.continuousLinearEquivOfBilin.symm F

theorem IsCoercive.solutionOfInner_def {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : hB.solutionOfInner F = hB.continuousLinearEquivOfBilin.symm F

The represented-forcing solution is the inverse Lax--Milgram operator.

@[simp]

theorem IsCoercive.continuousLinearEquivOfBilin_solutionOfInner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : hB.continuousLinearEquivOfBilin (hB.solutionOfInner F) = F

Applying the Lax--Milgram equivalence to the represented-forcing solution returns the forcing vector.

@[simp]

theorem IsCoercive.solutionOfInner_continuousLinearEquivOfBilin {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (u : V) : hB.solutionOfInner (hB.continuousLinearEquivOfBilin u) = u

Solving against the forcing represented by a Lax--Milgram image recovers the original vector.

@[simp]

theorem IsCoercive.apply_solutionOfInner_eq_inner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F v : V) : (B (hB.solutionOfInner F)) v = inner ℝ F v

The Lax--Milgram solution satisfies the variational equation.

theorem IsCoercive.eq_solutionOfInner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {F u : V} (hu : ∀ (v : V), (B u) v = inner ℝ F v) : u = hB.solutionOfInner F

A vector satisfying the represented variational equation is the Lax--Milgram solution.

theorem IsCoercive.existsUnique_forall_eq_inner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : ∃! u : V, ∀ (v : V), (B u) v = inner ℝ F v

Lax--Milgram as an existence-and-uniqueness theorem for represented functionals.

If B is coercive, then for every F : V there is a unique u such that B u v = ⟪F, v⟫ for all test vectors v.

theorem IsCoercive.exists_forall_eq_inner {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : ∃ (u : V), ∀ (v : V), (B u) v = inner ℝ F v

Lax--Milgram as an existence theorem for represented functionals.

noncomputable def IsCoercive.solutionOfFunctional {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (ℓ : StrongDual ℝ V) : V

The Lax--Milgram solution for an arbitrary continuous linear functional.

This is solutionOfInner applied to the Fréchet--Riesz representative of the functional.

Equations

• hB.solutionOfFunctional ℓ = hB.solutionOfInner ((InnerProductSpace.toDual ℝ V).symm ℓ)

theorem IsCoercive.solutionOfFunctional_def {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (ℓ : StrongDual ℝ V) : hB.solutionOfFunctional ℓ = hB.solutionOfInner ((InnerProductSpace.toDual ℝ V).symm ℓ)

The functional solution is obtained by solving against the Fréchet--Riesz representative.

@[simp]

theorem IsCoercive.solutionOfFunctional_toDual {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (F : V) : hB.solutionOfFunctional ((InnerProductSpace.toDual ℝ V) F) = hB.solutionOfInner F

For represented functionals, the functional solution agrees with solutionOfInner.

@[simp]

theorem IsCoercive.apply_solutionOfFunctional_eq {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (ℓ : StrongDual ℝ V) (v : V) : (B (hB.solutionOfFunctional ℓ)) v = ℓ v

The Lax--Milgram solution for a continuous linear functional satisfies the variational equation.

theorem IsCoercive.eq_solutionOfFunctional {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {ℓ : StrongDual ℝ V} {u : V} (hu : ∀ (v : V), (B u) v = ℓ v) : u = hB.solutionOfFunctional ℓ

A vector satisfying the variational equation for a continuous linear functional is the Lax--Milgram solution for that functional.

theorem IsCoercive.existsUnique_forall_eq {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (ℓ : StrongDual ℝ V) : ∃! u : V, ∀ (v : V), (B u) v = ℓ v

Lax--Milgram as an existence-and-uniqueness theorem for arbitrary continuous linear functionals.

theorem IsCoercive.exists_forall_eq {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (ℓ : StrongDual ℝ V) : ∃ (u : V), ∀ (v : V), (B u) v = ℓ v

Lax--Milgram as an existence theorem for arbitrary continuous linear functionals.