AcceptedLemma · Statement with omitted proof

Pointwise control by the interval H1 norm

The first-order Sobolev norm bounds every point value of a continuously differentiable function on the unit interval.

Larsson & Thomée ↗
Lemma A.1 · printed p. 236

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 first-order Sobolev norm bounds every point value of a continuously differentiable function on the unit interval.

|v(x)|\le C\|v\|_{H^1(0,1)},\qquad x\in[0,1].

Assumptions & context

A continuously differentiable function on the closed unit interval.

Source

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

Lemma A.1 · printed p. 236

02 / LEAN REPRESENTATION

Formal statement

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

theorem lemma_A1 :
    ∃ C : ℝ, ∀ x ∈ OmegaBar, ∀ v : ℝ → ℝ, ContDiffOn ℝ 1 v OmegaBar →
      |v x| ≤ C * h1Norm v := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomeeLemA1

/-- The closed interval `Ω̄ = [0,1]` for `Ω = (0,1)`. -/
abbrev OmegaBar : Set ℝ := Set.Icc (0 : ℝ) 1

/-- The open interval `Ω = (0,1)`. -/
abbrev Omega : Set ℝ := Set.Ioo (0 : ℝ) 1

/-- The textbook's `H¹(Ω)` norm `‖v‖₁ = (‖v‖² + ‖v'‖²)^{1/2}`, with `L²(Ω)` norms
over `Ω = (0,1)` (book, Sect. A.2 and (2.18)). It is used here for `v ∈ C¹(Ω̄)`.
`v'` is the derivative of `v` within `Ω̄`, which agrees with the ordinary derivative
at interior points. -/
def h1Norm (v : ℝ → ℝ) : ℝ :=
  Real.sqrt ((∫ x in Omega, v x ^ 2) + ∫ x in Omega, (derivWithin v OmegaBar x) ^ 2)

/-- Lemma A.1 (Larsson–Thomée). Let `Ω = (0,1)`. Then there is a constant `C` such that
`|v(x)| ≤ C ‖v‖₁` for all `x ∈ Ω̄` and all `v ∈ C¹(Ω̄)`. -/
theorem lemma_A1 :
    ∃ C : ℝ, ∀ x ∈ OmegaBar, ∀ v : ℝ → ℝ, ContDiffOn ℝ 1 v OmegaBar →
      |v x| ≤ C * h1Norm v := by
  sorry

end PDETextbook.LarssonThomeeLemA1

How to read the formalization

The same constant works for every function and every evaluation point, including endpoints.

← Back to all statements