Statement.lean

-- Lax-Milgram theorem
-- Status: ✅ verified against Mathlib

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Topology.Algebra.Module.Basic

open InnerProductSpace

/-- A continuous coercive bilinear form on a Hilbert space. -/
structure IsCoerciveContinuousBilinForm
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (a : H →L[ℝ] H →L[ℝ] ℝ) : Prop where
  coercive : ∃ α : ℝ, 0 < α ∧ ∀ u : H, α * ‖u‖ ^ 2 ≤ a u u

/-- Lax-Milgram theorem: for a continuous coercive bilinear form a on a
real Hilbert space H and any f ∈ H*, there exists a unique u ∈ H
such that a(u, v) = f(v) for all v ∈ H. -/
theorem lax_milgram
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (a : H →L[ℝ] H →L[ℝ] ℝ)
    (ha : IsCoerciveContinuousBilinForm a)
    (f : H →L[ℝ] ℝ) :
    ∃! u : H, ∀ v : H, a u v = f v := by
  sorry