AcceptedTheorem · Statement with omitted proof

Existence and stability of a one-dimensional weak solution

The weak Dirichlet problem has a unique solution and an energy bound in terms of the forcing.

Larsson & Thomée ↗
Theorem 2.4 · printed p. 22

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The weak Dirichlet problem has a unique solution and an energy bound in terms of the forcing.

u\in H_0^1(0,1),\qquad \|u\|_{H^1}\le \frac{2}{a_0}\|f\|_{L^2}.

Assumptions & context

Square-integrable forcing and the coefficient coercivity condition in equation (2.12), encoded explicitly in the full Lean file.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 2.4 · printed p. 22

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem thm_2_4 (a b c : ℝ → ℝ) (a₀ : ℝ) (h212 : Assumption212 a b c a₀)
    (f : Euclidean 1 → ℝ) (hf : InL2 Ω1 f) :
    ∃ u : Euclidean 1 → ℝ, SolvesVariational a b c f u ∧
      (∀ v : Euclidean 1 → ℝ, SolvesVariational a b c f v →
        v =ᵐ[domainMeasure Ω1] u) ∧
      (∀ G : Fin 1 → Euclidean 1 → ℝ, HasH1Gradient Ω1 u G →
        H1Norm u (G 0) ≤ (2 / a₀) * L2Norm f) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm24

/-- The interval Ω = (0,1) from (2.11), realized inside one-dimensional Euclidean space. -/
def Ω1 : Set (Euclidean 1) := {x | 0 < x 0 ∧ x 0 < 1}

/-- Assumption (2.12), together with the standing Section 2.3 assumption that the
coefficients a, b, c are smooth. Smoothness is taken on Ω̄ = [0,1]. The conditions are
`a(x) ≥ a₀ > 0` and `c(x) - b'(x)/2 ≥ 0` for `x ∈ Ω̄ = [0,1]`. -/
def Assumption212 (a b c : ℝ → ℝ) (a₀ : ℝ) : Prop :=
  ContDiffOn ℝ (⊤ : ℕ∞) a (Set.Icc 0 1) ∧
  ContDiffOn ℝ (⊤ : ℕ∞) b (Set.Icc 0 1) ∧
  ContDiffOn ℝ (⊤ : ℕ∞) c (Set.Icc 0 1) ∧
  0 < a₀ ∧
  ∀ x ∈ Set.Icc (0 : ℝ) 1, a₀ ≤ a x ∧ 0 ≤ c x - derivWithin b (Set.Icc 0 1) x / 2

/-- Bilinear form of the variational formulation of (2.11). Multiplying
`-(a u')' + b u' + c u = f` by a test function and integrating by parts gives
`a(v,w) = ∫₀¹ (a v' w' + b v' w + c v w) dx`, where `v'` and `w'` are weak derivatives. -/
def bform (a b c : ℝ → ℝ) (v v' w w' : Euclidean 1 → ℝ) : ℝ :=
  ∫ x in Ω1, (a (x 0) * v' x * w' x + b (x 0) * v' x * w x + c (x 0) * v x * w x)

/-- `L(w) = (f,w) = ∫₀¹ f w dx`. -/
def Lform (f w : Euclidean 1 → ℝ) : ℝ :=
  ∫ x in Ω1, f x * w x

/-- `u ∈ H₀¹` is a solution of (2.16): `a(u,φ) = L(φ)` for all `φ ∈ H₀¹`.
H₀¹ is the closure of C₀¹, matching the source's density remark. -/
def SolvesVariational (a b c : ℝ → ℝ) (f u : Euclidean 1 → ℝ) : Prop :=
  InH10Closure Ω1 u ∧
  ∀ G : Fin 1 → Euclidean 1 → ℝ, HasH1Gradient Ω1 u G →
    ∀ φ : Euclidean 1 → ℝ, InH10Closure Ω1 φ →
      ∀ H : Fin 1 → Euclidean 1 → ℝ, HasH1Gradient Ω1 φ H →
        bform a b c u (G 0) φ (H 0) = Lform f φ

/-- `‖v‖₁ = (‖v‖² + ‖v'‖²)^{1/2}`, where `v'` is the weak derivative. -/
def H1Norm (v v' : Euclidean 1 → ℝ) : ℝ :=
  Real.sqrt ((∫ x in Ω1, v x ^ 2) + ∫ x in Ω1, v' x ^ 2)

/-- `‖f‖` in `L₂(Ω)`. -/
def L2Norm (f : Euclidean 1 → ℝ) : ℝ :=
  Real.sqrt (∫ x in Ω1, f x ^ 2)

/-- Theorem 2.4 (Larsson–Thomée). Assume (2.12) and `f ∈ L₂`. Then (2.16) has a unique
solution `u ∈ H₀¹`, unique as an a.e. class. This solution satisfies (2.20):
`‖u‖₁ ≤ C‖f‖` with `C = 2/a₀`. -/
theorem thm_2_4 (a b c : ℝ → ℝ) (a₀ : ℝ) (h212 : Assumption212 a b c a₀)
    (f : Euclidean 1 → ℝ) (hf : InL2 Ω1 f) :
    ∃ u : Euclidean 1 → ℝ, SolvesVariational a b c f u ∧
      (∀ v : Euclidean 1 → ℝ, SolvesVariational a b c f v →
        v =ᵐ[domainMeasure Ω1] u) ∧
      (∀ G : Fin 1 → Euclidean 1 → ℝ, HasH1Gradient Ω1 u G →
        H1Norm u (G 0) ≤ (2 / a₀) * L2Norm f) := by
  sorry

end PDETextbook.LarssonThomee.Thm24

How to read the formalization

Uniqueness is expressed as almost-everywhere equality, consistent with the Sobolev-space setting.

← Back to all statements