AcceptedTheorem · Statement with omitted proof

Supremum-norm stability in one dimension

An elliptic solution is controlled by its endpoint data and the size of its residual.

Larsson & Thomée ↗
Theorem 2.2 · printed p. 17

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

An elliptic solution is controlled by its endpoint data and the size of its residual.

\|u\|_{C([0,1])}\le\max\{|u(0)|,|u(1)|\}+C\|Au\|_{C([0,1])}.

Assumptions & context

Smooth coefficients with a uniformly positive leading term and nonnegative zero-order term; the function has two continuous derivatives.

Source

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

Theorem 2.2 · printed p. 17

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_2 (a b c : ℝ → ℝ) (a₀ : ℝ) (hcoef : CoeffHyp a b c a₀) :
    ∃ C : ℝ, ∀ u : ℝ → ℝ, ContDiffOn ℝ 2 u (Set.Icc 0 1) →
      maxNormC u ≤ max (|u 0|) (|u 1|) + C * opANormC a b c u := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm22

/-- The operator of (2.1): `𝒜u := -(a u')' + b u' + c u`, evaluated pointwise.
It is used only at interior points `x ∈ Ω = (0,1)`. -/
def opA (a b c u : ℝ → ℝ) (x : ℝ) : ℝ :=
  -deriv (fun y => a y * deriv u y) x + b x * deriv u x + c x * u x

/-- Maximum norm `‖v‖_𝒞 = max_{x ∈ [0,1]} |v(x)|` for `v` continuous on `[0,1]`. -/
def maxNormC (v : ℝ → ℝ) : ℝ :=
  sSup ((fun x => |v x|) '' Set.Icc (0 : ℝ) 1)

/-- The norm `‖𝒜u‖_𝒞`. For `u ∈ 𝒞²[0,1]`, `a ∈ 𝒞¹[0,1]`, `b, c ∈ 𝒞[0,1]`, the function `𝒜u` on `(0,1)`
extends continuously to `[0,1]`, and its maximum over `[0,1]` equals the supremum over `(0,1)`. -/
def opANormC (a b c u : ℝ → ℝ) : ℝ :=
  sSup ((fun x => |opA a b c u x|) '' Set.Ioo (0 : ℝ) 1)

/-- The coefficient hypotheses (2.2), together with the regularity making `𝒜u ∈ 𝒞` for `u ∈ 𝒞²`. -/
def CoeffHyp (a b c : ℝ → ℝ) (a₀ : ℝ) : Prop :=
  ContDiffOn ℝ 1 a (Set.Icc 0 1) ∧ ContinuousOn b (Set.Icc 0 1) ∧
    ContinuousOn c (Set.Icc 0 1) ∧ 0 < a₀ ∧
    ∀ x ∈ Set.Icc (0 : ℝ) 1, a₀ ≤ a x ∧ 0 ≤ c x

/-- Theorem 2.2 (Larsson–Thomée). Let `𝒜` be as in (2.1), (2.2). If `u ∈ 𝒞² = 𝒞²([0,1])`, then
`‖u‖_𝒞 ≤ max{|u(0)|, |u(1)|} + C ‖𝒜u‖_𝒞`, where `C` depends on the coefficients of `𝒜`
but not on `u` (hence `C` is chosen after `a, b, c, a₀` and before `u`). -/
theorem thm_2_2 (a b c : ℝ → ℝ) (a₀ : ℝ) (hcoef : CoeffHyp a b c a₀) :
    ∃ C : ℝ, ∀ u : ℝ → ℝ, ContDiffOn ℝ 2 u (Set.Icc 0 1) →
      maxNormC u ≤ max (|u 0|) (|u 1|) + C * opANormC a b c u := by
  sorry

end PDETextbook.LarssonThomee.Thm22

How to read the formalization

The constant is chosen before the function, so the bound is uniform over admissible inputs.

← Back to all statements