Stampacchia's theorem

TheoremVariational inequality on the whole space reduces to an equation#✓fully proved

On the whole space, a variational-inequality solution satisfies A u = f.

theorem stampacchia_eq_of_univ (A : E →L[ℝ] E) (f : E) (u : E)
    (h : ∀ v ∈ (Set.univ : Set E), 0 ≤ ⟪A u - f, v - u⟫_ℝ) : A u = f

Used by 1

Used byCoercive bounded operators on a real Hilbert space are surjective

TheoremStampacchia's theorem, operator form#✓fully proved

For a coercive bounded linear operator A on a real Hilbert space, a nonempty closed convex set K, and f ∈ E, there is exactly one u ∈ K with ⟪A u - f, v - u⟫_ℝ ≥ 0 for all v ∈ K.

theorem exists_unique_stampacchia {K : Set E} (hKne : K.Nonempty)
    (hKclosed : IsClosed K) (hKconv : Convex ℝ K) (A : E →L[ℝ] E) {α : ℝ}
    (hα : 0 < α) (hcoer : ∀ u, α * ‖u‖ ^ 2 ≤ ⟪A u, u⟫_ℝ) (f : E) :
    ∃! u, u ∈ K ∧ ∀ v ∈ K, 0 ≤ ⟪A u - f, v - u⟫_ℝ

Uses 4 · Used by 2

Proof usesNearest-point projection onto a convex set · The convex projection lies in the set · Variational inequality for the convex projection · The convex projection is \(1\)-Lipschitz

Used byCoercive bounded operators on a real Hilbert space are surjective · Stampacchia's theorem, bilinear-form form

TheoremStampacchia's theorem, bilinear-form form#✓fully proved

For a coercive bounded bilinear form B on a real Hilbert space, a nonempty closed convex set K, and a continuous linear functional φ, there is exactly one u ∈ K with B u (v - u) ≥ φ (v - u) for all v ∈ K.

theorem exists_unique_stampacchia_bilinear {K : Set E} (hKne : K.Nonempty)
    (hKclosed : IsClosed K) (hKconv : Convex ℝ K)
    (B : E →L[ℝ] E →L[ℝ] ℝ) {α : ℝ} (hα : 0 < α)
    (hcoer : ∀ u, α * ‖u‖ ^ 2 ≤ B u u) (φ : E →L[ℝ] ℝ) :
    ∃! u, u ∈ K ∧ ∀ v ∈ K, φ (v - u) ≤ B u (v - u)

Uses 1

Proof usesStampacchia's theorem, operator form

TheoremCoercive bounded operators on a real Hilbert space are surjective#✓fully proved

A coercive bounded linear operator on a real Hilbert space is surjective. This is the whole-space case of Stampacchia's theorem (compare Mathlib's Lax–Milgram theorem, which is the analogous statement for bilinear forms).

theorem exists_eq_of_coercive (A : E →L[ℝ] E) {α : ℝ} (hα : 0 < α)
    (hcoer : ∀ u, α * ‖u‖ ^ 2 ≤ ⟪A u, u⟫_ℝ) (f : E) : ∃ u, A u = f

Uses 2

Proof usesStampacchia's theorem, operator form · Variational inequality on the whole space reduces to an equation

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.