AcceptedTheorem · Statement with omitted proof

Energy stability for symmetric hyperbolic systems

The L2 norm of a symmetric hyperbolic solution is bounded by the initial data and a time-integrated forcing norm.

Larsson & Thomée ↗
Theorem 11.5 · printed p. 178

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 L2 norm of a symmetric hyperbolic solution is bounded by the initial data and a time-integrated forcing norm.

\|u(t)\|_{L^2}\le C(T)\Bigl(\|v\|_{L^2}+\bigl(\int_0^T\|f(s)\|_{L^2}^2\,ds\bigr)^{1/2}\Bigr),\quad 0\le t\le T.

Assumptions & context

Symmetric principal matrices, smooth bounded coefficients and data, a nonnegative time horizon, and the stated decay at spatial infinity.

Source

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

Theorem 11.5 · printed p. 178

02 / LEAN REPRESENTATION

Formal statement

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

theorem energy_estimate (d N : ℕ)
    (A : Fin d → Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (B : Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (hAsymm : ∀ j p, (A j p).IsSymm)
    (hA : ∀ j a b, SmoothBounded (fun p => A j p a b))
    (hB : ∀ a b, SmoothBounded (fun p => B p a b))
    (T : ℝ) (hT : 0 ≤ T) :
    ∃ C : NNReal, ∀ (f : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N))
      (v : Euclidean d → EuclideanSpace ℝ (Fin N))
      (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N)),
      SmoothBounded f → SmoothBounded v →
      IsSolution11_21 A B f v u → SmallForLargeX T u →
      ∀ t ∈ Set.Icc (0 : ℝ) T,
        eLpNorm (fun x => u (x, t)) 2 volume ≤
          (C : ℝ≥0∞) * (eLpNorm v 2 volume +
            (∫⁻ s in Set.Icc (0 : ℝ) T,
              eLpNorm (fun x => f (x, s)) 2 volume ^ 2) ^ (1 / 2 : ℝ)) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm11_5

/-- "Depending smoothly and boundedly on its variables": smooth, with every derivative bounded (C_b^∞). -/
def SmoothBounded {E Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] (F : E → Y) : Prop :=
  ContDiff ℝ (⊤ : ℕ∞) F ∧ ∀ k : ℕ, ∃ M : ℝ, ∀ p, ‖iteratedFDeriv ℝ k F p‖ ≤ M

/-- Classical time derivative ∂u/∂t at (x,t). -/
def timeDeriv {d N : ℕ} (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N))
    (p : Euclidean d × ℝ) : EuclideanSpace ℝ (Fin N) :=
  fderiv ℝ u p (0, 1)

/-- Classical spatial partial derivative ∂u/∂x_j at (x,t). -/
def spaceDeriv {d N : ℕ} (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N)) (j : Fin d)
    (p : Euclidean d × ℝ) : EuclideanSpace ℝ (Fin N) :=
  fderiv ℝ u p (EuclideanSpace.single j 1, 0)

/-- u is a (classical) solution of (11.21):
∂u/∂t + Σ_j A_j ∂u/∂x_j + B u = f in ℝ^d × ℝ_+, u(·,0) = v in ℝ^d. -/
def IsSolution11_21 {d N : ℕ}
    (A : Fin d → Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (B : Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (f : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N))
    (v : Euclidean d → EuclideanSpace ℝ (Fin N))
    (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N)) : Prop :=
  ContinuousOn u (Set.univ ×ˢ Set.Ici 0) ∧
  ContDiffOn ℝ 1 u (Set.univ ×ˢ Set.Ioi 0) ∧
  (∀ x : Euclidean d, ∀ t : ℝ, 0 < t →
    timeDeriv u (x, t) + ∑ j, Matrix.toEuclideanLin (A j (x, t)) (spaceDeriv u j (x, t))
      + Matrix.toEuclideanLin (B (x, t)) (u (x, t)) = f (x, t)) ∧
  ∀ x : Euclidean d, u (x, 0) = v x

/-- Realization of "solutions are small for large |x| in such a way that the following
analysis is valid" on [0,T]: u and its first derivatives are dominated, uniformly in
t ∈ [0,T], by a fixed function in L²(ℝ^d). -/
def SmallForLargeX {d N : ℕ} (T : ℝ)
    (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N)) : Prop :=
  ∃ g : Euclidean d → ℝ, MemLp g 2 volume ∧ ∀ x : Euclidean d,
    (∀ t ∈ Set.Icc (0 : ℝ) T, ‖u (x, t)‖ ≤ g x) ∧
    (∀ t ∈ Set.Ioc (0 : ℝ) T,
      ‖timeDeriv u (x, t)‖ + ∑ j, ‖spaceDeriv u j (x, t)‖ ≤ g x)

/-- Theorem 11.5 (energy estimate for the symmetric hyperbolic system (11.21)).
For smooth bounded coefficients with A_j symmetric, and each T ≥ 0, there is C = C(T)
(depending also on the fixed coefficients A_j, B) such that every solution satisfies
‖u(t)‖ ≤ C(‖v‖ + (∫_0^T ‖f‖² ds)^{1/2}) for 0 ≤ t ≤ T, norms in L²(ℝ^d). Stated in ℝ≥0∞
so that an infinite right-hand side is not truncated. -/
theorem energy_estimate (d N : ℕ)
    (A : Fin d → Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (B : Euclidean d × ℝ → Matrix (Fin N) (Fin N) ℝ)
    (hAsymm : ∀ j p, (A j p).IsSymm)
    (hA : ∀ j a b, SmoothBounded (fun p => A j p a b))
    (hB : ∀ a b, SmoothBounded (fun p => B p a b))
    (T : ℝ) (hT : 0 ≤ T) :
    ∃ C : NNReal, ∀ (f : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N))
      (v : Euclidean d → EuclideanSpace ℝ (Fin N))
      (u : Euclidean d × ℝ → EuclideanSpace ℝ (Fin N)),
      SmoothBounded f → SmoothBounded v →
      IsSolution11_21 A B f v u → SmallForLargeX T u →
      ∀ t ∈ Set.Icc (0 : ℝ) T,
        eLpNorm (fun x => u (x, t)) 2 volume ≤
          (C : ℝ≥0∞) * (eLpNorm v 2 volume +
            (∫⁻ s in Set.Icc (0 : ℝ) T,
              eLpNorm (fun x => f (x, s)) 2 volume ^ 2) ^ (1 / 2 : ℝ)) := by
  sorry

end PDETextbook.LarssonThomee.Thm11_5

How to read the formalization

The constant is chosen for the coefficients and time horizon before the forcing and solution.

← Back to all statements