AcceptedTheorem · Statement with omitted proof

Supremum-norm estimate for a forced heat problem

Initial data, boundary data, and forcing control the solution throughout the space–time cylinder.

Larsson & Thomée ↗
Theorem 8.7 · printed p. 123

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Initial data, boundary data, and forcing control the solution throughout the space–time cylinder.

\|u\|_\infty\le\max\{\|g\|_\infty,\|v\|_\infty\}+\frac{r^2}{2d}\|f\|_\infty.

Assumptions & context

A solution of the stated heat initial-boundary problem on a bounded connected domain contained in a ball of positive radius.

Source

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

Theorem 8.7 · printed p. 123

02 / LEAN REPRESENTATION

Formal statement

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

theorem thm_8_7 {d : ℕ} (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω)
    (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (T : ℝ) (hT : 0 < T)
    (f g : Euclidean d → ℝ → ℝ) (v : Euclidean d → ℝ) (u : Euclidean d → ℝ → ℝ)
    (hu : IsSolution834 Ω T f g v u)
    (x₀ : Euclidean d) (r : ℝ) (hr : 0 < r) (hball : Ω ⊆ Metric.ball x₀ r) :
    supNormOn (closure Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => u p.1 p.2) ≤
      max (supNormOn (frontier Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => g p.1 p.2))
          (supNormOn (closure Ω) v) +
        ENNReal.ofReal (r ^ 2) / (2 * (d : ℝ≥0∞)) *
          supNormOn (closure Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => f p.1 p.2) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm87

/-- Classical spatial Laplacian `Δw(x) = ∑ᵢ ∂²w/∂xᵢ²`, via the second iterated Fréchet derivative. -/
def spatialLaplacian {d : ℕ} (w : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  ∑ i : Fin d, iteratedFDeriv ℝ 2 w x (fun _ => EuclideanSpace.single i (1 : ℝ))

/-- Maximum norm `‖φ‖_{C(S)} = sup_{p ∈ S} |φ p|`, valued in `ℝ≥0∞`. For continuous data on a
compact set this equals the usual (finite) maximum norm. -/
def supNormOn {α : Type*} (S : Set α) (φ : α → ℝ) : ℝ≥0∞ :=
  ⨆ p ∈ S, ENNReal.ofReal |φ p|

/-- `u` is a (classical) solution of (8.34) on `Ω̄ × Ī`, with `I = (0,T)` and `Γ = ∂Ω`:
`u_t - Δu = f` in `Ω × I`, `u = g` on `Γ × I`, `u(·,0) = v` in `Ω`. -/
def IsSolution834 {d : ℕ} (Ω : Set (Euclidean d)) (T : ℝ)
    (f g : Euclidean d → ℝ → ℝ) (v : Euclidean d → ℝ)
    (u : Euclidean d → ℝ → ℝ) : Prop :=
  ContinuousOn (fun p : Euclidean d × ℝ => u p.1 p.2) (closure Ω ×ˢ Set.Icc 0 T) ∧
  (∀ t ∈ Set.Ioo 0 T, ContDiffOn ℝ 2 (fun y => u y t) Ω) ∧
  (∀ x ∈ Ω, ∀ t ∈ Set.Ioo 0 T, DifferentiableAt ℝ (fun s => u x s) t) ∧
  (∀ x ∈ Ω, ∀ t ∈ Set.Ioo 0 T,
      deriv (fun s => u x s) t - spatialLaplacian (fun y => u y t) x = f x t) ∧
  (∀ x ∈ frontier Ω, ∀ t ∈ Set.Ioo 0 T, u x t = g x t) ∧
  (∀ x ∈ Ω, u x 0 = v x)

/-- Theorem 8.7 (Larsson–Thomée): the solution of (8.34) satisfies
`‖u‖_{C(Ω̄×Ī)} ≤ max{‖g‖_{C(Γ×Ī)}, ‖v‖_{C(Ω̄)}} + r²/(2d) ‖f‖_{C(Ω̄×Ī)}`,
where `r` is the radius of a ball containing `Ω`. Norms are maximum norms in `ℝ≥0∞`. -/
theorem thm_8_7 {d : ℕ} (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω)
    (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (T : ℝ) (hT : 0 < T)
    (f g : Euclidean d → ℝ → ℝ) (v : Euclidean d → ℝ) (u : Euclidean d → ℝ → ℝ)
    (hu : IsSolution834 Ω T f g v u)
    (x₀ : Euclidean d) (r : ℝ) (hr : 0 < r) (hball : Ω ⊆ Metric.ball x₀ r) :
    supNormOn (closure Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => u p.1 p.2) ≤
      max (supNormOn (frontier Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => g p.1 p.2))
          (supNormOn (closure Ω) v) +
        ENNReal.ofReal (r ^ 2) / (2 * (d : ℝ≥0∞)) *
          supNormOn (closure Ω ×ˢ Set.Icc 0 T) (fun p : Euclidean d × ℝ => f p.1 p.2) := by
  sorry

end PDETextbook.LarssonThomee.Thm87

How to read the formalization

The bound keeps the geometric radius and dimension explicit. The exact saved expression uses extended nonnegative norms, including its dimension-zero convention.

← Back to all statements