Consistency and L2 convergence of heat difference schemes

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

namespace PDETextbook.LarssonThomee.Thm94

open Asymptotics

noncomputable section

/-- The explicit operator (9.13) on functions of `x ∈ ℝ`:
`(E_k U)(x) = ∑_p a_p U(x - x_p)` with `x_p = p h`. The coefficients
`a_p = a_p(λ)` form a finitely supported family indexed by `p ∈ ℤ`. For fixed
`λ = k/h²` they do not depend on `h`. -/
def schemeOp (a : ℤ →₀ ℝ) (h : ℝ) (U : ℝ → ℂ) : ℝ → ℂ :=
  fun x => a.sum (fun p c => (c : ℂ) * U (x - (p : ℝ) * h))

/-- Symbol `Ẽ(ξ) = ∑_p a_p e^{-ipξ}`. With the Fourier transform (9.14) this gives
`(E_k v)^(ξ) = Ẽ(hξ) v̂(ξ)`, as used in the proof of Theorem 9.4. -/
def symbol (a : ℤ →₀ ℝ) (ξ : ℝ) : ℂ :=
  a.sum (fun p c => (c : ℂ) * Complex.exp (-(Complex.I * (((p : ℝ) * ξ : ℝ) : ℂ))))

/-- (9.15): `E_k` is accurate of order `r` if
`Ẽ(ξ) = e^{-λξ²} + O(|ξ|^{r+2})` as `ξ → 0`. -/
def AccurateOfOrder (lam : ℝ) (a : ℤ →₀ ℝ) (r : ℕ) : Prop :=
  (fun ξ : ℝ => symbol a ξ - ((Real.exp (-lam * ξ ^ 2) : ℝ) : ℂ))
    =O[nhds (0 : ℝ)] (fun ξ : ℝ => |ξ| ^ (r + 2))

/-- Stability in `L₂ = L₂(ℝ)`: `‖E_k^n V‖ ≤ C ‖V‖` for all `n ≥ 0`, all `V ∈ L₂`
and all mesh widths `h > 0`. Here `λ` is held fixed. -/
def StableL2 (a : ℤ →₀ ℝ) : Prop :=
  ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ n : ℕ, ∀ V : ℝ → ℂ, MemLp V 2 volume →
    eLpNorm ((schemeOp a h)^[n] V) 2 volume ≤ ENNReal.ofReal C * eLpNorm V 2 volume

/-- Exact solution `u(x,t) = (E(t)v)(x)` of the pure initial value problem (9.1),
given by the heat-kernel representation for `t > 0`, with `u(·,0) = v`. -/
def heatSolution (v : ℝ → ℂ) (t : ℝ) (x : ℝ) : ℂ :=
  if t = 0 then v x else
    ∫ y : ℝ, (((Real.sqrt (4 * Real.pi * t))⁻¹ *
      Real.exp (-(x - y) ^ 2 / (4 * t)) : ℝ) : ℂ) * v y

/-- Seminorm `|v|_s = (∑_{|α| = s} ‖D^α v‖²)^{1/2}` on `ℝ`. In one dimension it
equals `‖v^{(s)}‖_{L₂(ℝ)}`. It is kept in `ℝ≥0∞` and may be infinite. -/
def sobolevSeminorm (s : ℕ) (v : ℝ → ℂ) : ℝ≥0∞ :=
  eLpNorm (iteratedDeriv s v) 2 volume

/-- Theorem 9.4. Assume `E_k` is defined by (9.13) with `λ = k/h²` constant.
Assume it is accurate of order `r` and stable in `L₂`. Then
`‖U^n - u^n‖ ≤ C t_n h^r |v|_{r+2}` for `t_n ≥ 0`.
Here `U^n = E_k^n v`, `u^n = u(·, t_n)`, `t_n = n k` and `k = λ h²`. -/
theorem thm_9_4 (lam : ℝ) (hlam : 0 < lam) (a : ℤ →₀ ℝ) (r : ℕ)
    (hacc : AccurateOfOrder lam a r) (hstab : StableL2 a) :
    ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ n : ℕ, ∀ v : ℝ → ℂ,
      ContDiff ℝ (⊤ : ℕ∞) v → (∃ M : ℝ, ∀ x, ‖v x‖ ≤ M) → MemLp v 2 volume →
      eLpNorm (fun x => (schemeOp a h)^[n] v x
          - heatSolution v ((n : ℝ) * (lam * h ^ 2)) x) 2 volume
        ≤ ENNReal.ofReal (C * ((n : ℝ) * (lam * h ^ 2)) * h ^ r)
          * sobolevSeminorm (r + 2) v := by
  sorry

end

end PDETextbook.LarssonThomee.Thm94