Lax–Milgram existence and energy bound

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

namespace PDETextbook
namespace LarssonThomeeA3

/-- A bilinear form `a` on a normed space `V` is bounded: there is a constant `M` with
`|a(v,w)| ≤ M ‖v‖_V ‖w‖_V` for all `v, w ∈ V`. -/
def IsBoundedBilinear {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (a : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : Prop :=
  ∃ M : ℝ, ∀ v w : V, |a v w| ≤ M * ‖v‖ * ‖w‖

/-- Coercivity (A.12): `a(v,v) ≥ α ‖v‖_V^2` for all `v ∈ V`, with `α > 0`. -/
def IsCoercive {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (a : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (α : ℝ) : Prop :=
  0 < α ∧ ∀ v : V, α * ‖v‖ ^ 2 ≤ a v v

/-- The variational problem (A.11): `a(u,v) = L(v)` for all `v ∈ V`. -/
def SolvesVariational {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (a : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (L : V →L[ℝ] ℝ) (u : V) : Prop :=
  ∀ v : V, a u v = L v

/-- Theorem A.3 (Lax–Milgram). If the bilinear form `a` is bounded and coercive (with
coercivity constant `α > 0`, as in (A.12)) in the Hilbert space `V`, and `L` is a bounded
linear form on `V`, then there exists a unique `u ∈ V` satisfying (A.11). Moreover the energy
estimate (A.13) `‖u‖_V ≤ C ‖L‖_{V*}` with `C = 1/α` holds. Here `‖L‖_{V*}` is the operator
(dual) norm. The paragraph introducing (A.11) also calls `a` symmetric, but Theorem A.3
assumes only boundedness and coercivity, so symmetry is not imposed here. -/
theorem lax_milgram
    {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
    (a : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (α : ℝ) (L : V →L[ℝ] ℝ)
    (ha_bdd : IsBoundedBilinear a) (ha_coer : IsCoercive a α) :
    (∃! u : V, SolvesVariational a L u) ∧
      ∀ u : V, SolvesVariational a L u → ‖u‖ ≤ (1 / α) * ‖L‖ := by
  sorry

end LarssonThomeeA3
end PDETextbook