AcceptedTheorem · Statement with omitted proof

Backward Euler finite elements for interval transport

The fully discrete transport estimate separates first-order spatial and temporal errors.

Larsson & Thomée ↗
Theorem 13.4 · printed p. 207

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 fully discrete transport estimate separates first-order spatial and temporal errors.

\|U^n-u(t_n)\|\le Ch\Bigl(\|v\|_{H^1}+\int_0^{t_n}(\|u\|_{H^2}+\|u_t\|_{H^1})\,ds\Bigr)+Ck\int_0^{t_n}\|u_{tt}\|\,ds.

Assumptions & context

An interval partition, initial data with a weak derivative, a suitable finite-element initial value, positive time step, and the backward Euler transport equations.

Source

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

Theorem 13.4 · printed p. 207

02 / LEAN REPRESENTATION

Formal statement

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

theorem thm_13_4 :
    ∃ C : ℝ, ∀ (P : Partition01) (v vx : ℝ → ℝ), HasWeakDeriv01 v vx →
      ∃ vh : ℝ → ℝ, InSh P vh ∧
        ∀ k : ℝ, 0 < k →
        ∀ (u f ux uxx ut utx utt : ℝ → ℝ → ℝ),
          IsSolution136 u f v ux uxx ut utx utt →
          (∀ t, 0 < t → MemLp (fun x => f x t) 2 μ01) →
          ∀ U : ℕ → ℝ → ℝ, IsBackwardEuler P k f vh U →
          ∀ n : ℕ,
            L2norm01 (fun x => U n x - u x ((n : ℝ) * k)) ≤
              ENNReal.ofReal (C * meshWidth P) *
                (H1norm01 v vx +
                  ∫⁻ s in Ioc (0 : ℝ) ((n : ℝ) * k),
                    (H2norm01 (fun x => u x s) (fun x => ux x s) (fun x => uxx x s) +
                      H1norm01 (fun x => ut x s) (fun x => utx x s))) +
              ENNReal.ofReal (C * k) *
                ∫⁻ s in Ioc (0 : ℝ) ((n : ℝ) * k), L2norm01 (fun x => utt x s) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm13_4

open Set

/-- Partition `0 = x_0 < ... < x_M = 1` of `Ω = (0,1)`. -/
structure Partition01 where
  M : ℕ
  x : Fin (M + 1) → ℝ
  x_zero : x 0 = 0
  x_last : x (Fin.last M) = 1
  strictMono : StrictMono x

/-- `h = max_j (x_j - x_{j-1})`. -/
def meshWidth (P : Partition01) : ℝ :=
  ⨆ j : Fin P.M, (P.x j.succ - P.x j.castSucc)

/-- `S_h^-` of (13.7). -/
def InSh (P : Partition01) (χ : ℝ → ℝ) : Prop :=
  ContinuousOn χ (Icc 0 1) ∧
  (∀ j : Fin P.M, ∃ a b : ℝ, ∀ y ∈ Icc (P.x j.castSucc) (P.x j.succ), χ y = a * y + b) ∧
  χ 0 = 0

/-- `Ω = (0,1)` inside the base `Euclidean 1`. -/
def Ω1 : Set (Euclidean 1) := {y | y 0 ∈ Ioo (0 : ℝ) 1}

/-- `g` is a weak derivative of `w` on `(0,1)` (base `HasWeakPartial`). -/
def HasWeakDeriv01 (w g : ℝ → ℝ) : Prop :=
  HasWeakPartial Ω1 (fun y : Euclidean 1 => w (y 0)) 0 (fun y : Euclidean 1 => g (y 0))

abbrev μ01 : Measure ℝ := volume.restrict (Ioo (0 : ℝ) 1)

/-- `‖w‖` in `L_2(0,1)`. -/
def L2norm01 (w : ℝ → ℝ) : ℝ≥0∞ := eLpNorm w 2 μ01

/-- `‖w‖_1` with weak derivative `w'`. -/
def H1norm01 (w w' : ℝ → ℝ) : ℝ≥0∞ :=
  (L2norm01 w ^ 2 + L2norm01 w' ^ 2) ^ (1 / 2 : ℝ)

/-- `‖w‖_2` with weak derivatives `w', w''`. -/
def H2norm01 (w w' w'' : ℝ → ℝ) : ℝ≥0∞ :=
  (L2norm01 w ^ 2 + L2norm01 w' ^ 2 + L2norm01 w'' ^ 2) ^ (1 / 2 : ℝ)

/-- `u x t` solves (13.6): `u_t + u_x = f` in `Ω × (0,∞)`, `u(0,t) = 0`, `u(·,0) = v`. -/
def IsSolution136 (u f : ℝ → ℝ → ℝ) (v : ℝ → ℝ)
    (ux uxx ut utx utt : ℝ → ℝ → ℝ) : Prop :=
  ContinuousOn (fun p : ℝ × ℝ => u p.1 p.2) (Icc 0 1 ×ˢ Ici 0) ∧
  (∀ t, 0 < t → HasWeakDeriv01 (fun x => u x t) (fun x => ux x t)) ∧
  (∀ t, 0 < t → HasWeakDeriv01 (fun x => ux x t) (fun x => uxx x t)) ∧
  (∀ t, 0 < t → HasWeakDeriv01 (fun x => ut x t) (fun x => utx x t)) ∧
  (∀ x ∈ Ioo (0 : ℝ) 1, ∀ t, 0 < t →
    HasDerivAt (fun s => u x s) (ut x t) t ∧ HasDerivAt (fun s => ut x s) (utt x t) t) ∧
  (∀ x ∈ Ioo (0 : ℝ) 1, ∀ t, 0 < t → ut x t + ux x t = f x t) ∧
  (∀ t, 0 < t → u 0 t = 0) ∧
  (∀ x ∈ Ioo (0 : ℝ) 1, u x 0 = v x)

/-- Backward Euler scheme (13.10), `t_n = n k`, `∂̄_t U^n = (U^n - U^{n-1})/k`. -/
def IsBackwardEuler (P : Partition01) (k : ℝ) (f : ℝ → ℝ → ℝ) (vh : ℝ → ℝ)
    (U : ℕ → ℝ → ℝ) : Prop :=
  (∀ n, InSh P (U n)) ∧ (∀ x ∈ Icc (0 : ℝ) 1, U 0 x = vh x) ∧
  ∀ n : ℕ, 0 < n → ∀ χ, InSh P χ →
    (∫ x in (0 : ℝ)..1, (U n x - U (n - 1) x) / k * χ x) +
      (∫ x in (0 : ℝ)..1, deriv (U n) x * χ x) =
    ∫ x in (0 : ℝ)..1, f x ((n : ℝ) * k) * χ x

/-- Theorem 13.4 (Larsson–Thomée). With `v_h ∈ S_h^-` suitably chosen, for `n ≥ 0`,
`‖U^n - u(t_n)‖ ≤ Ch(‖v‖_1 + ∫_0^{t_n}(‖u‖_2 + ‖u_t‖_1) ds) + Ck ∫_0^{t_n} ‖u_tt‖ ds`. -/
theorem thm_13_4 :
    ∃ C : ℝ, ∀ (P : Partition01) (v vx : ℝ → ℝ), HasWeakDeriv01 v vx →
      ∃ vh : ℝ → ℝ, InSh P vh ∧
        ∀ k : ℝ, 0 < k →
        ∀ (u f ux uxx ut utx utt : ℝ → ℝ → ℝ),
          IsSolution136 u f v ux uxx ut utx utt →
          (∀ t, 0 < t → MemLp (fun x => f x t) 2 μ01) →
          ∀ U : ℕ → ℝ → ℝ, IsBackwardEuler P k f vh U →
          ∀ n : ℕ,
            L2norm01 (fun x => U n x - u x ((n : ℝ) * k)) ≤
              ENNReal.ofReal (C * meshWidth P) *
                (H1norm01 v vx +
                  ∫⁻ s in Ioc (0 : ℝ) ((n : ℝ) * k),
                    (H2norm01 (fun x => u x s) (fun x => ux x s) (fun x => uxx x s) +
                      H1norm01 (fun x => ut x s) (fun x => utx x s))) +
              ENNReal.ofReal (C * k) *
                ∫⁻ s in Ioc (0 : ℝ) ((n : ℝ) * k), L2norm01 (fun x => utt x s) := by
  sorry

end PDETextbook.LarssonThomee.Thm13_4

How to read the formalization

Weak spatial derivatives and time derivatives are supplied explicitly. The time error uses the integral of the second time derivative.

← Back to all statements