import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm12_2

/-- The explicit finite difference operator of (12.11): `(E_k U)(x) = ∑_p a_p U(x - p h)`. -/
def schemeOp {𝕜 : Type*} [RCLike 𝕜] (coef : ℤ →₀ ℝ) (h : ℝ) (U : ℝ → 𝕜) : ℝ → 𝕜 :=
  fun x => coef.sum fun p c => ((c : ℝ) : 𝕜) * U (x - (p : ℝ) * h)

/-- Trigonometric polynomial of the scheme, `Ẽ(ξ) = ∑_p a_p e^{-i p ξ}`. -/
def symbol (coef : ℤ →₀ ℝ) (ξ : ℝ) : ℂ :=
  coef.sum fun p c => (c : ℂ) * Complex.exp (-(Complex.I * (p : ℂ) * (ξ : ℂ)))

/-- Accuracy of order `r` in the form (12.13): `Ẽ(ξ) = e^{i a λ ξ} + O(ξ^{r+1})` as `ξ → 0`. -/
def AccurateOfOrder (coef : ℤ →₀ ℝ) (a lam : ℝ) (r : ℕ) : Prop :=
  Asymptotics.IsBigO (nhds (0 : ℝ))
    (fun ξ : ℝ => symbol coef ξ - Complex.exp (Complex.I * ((a * lam * ξ : ℝ) : ℂ)))
    (fun ξ : ℝ => ξ ^ (r + 1))

/-- Stability in `L_2(ℝ)`: `‖E_k^n w‖ ≤ C ‖w‖` for all `n ≥ 0`, uniformly in `h`. -/
def StableL2 (𝕜 : Type*) [RCLike 𝕜] (coef : ℤ →₀ ℝ) : Prop :=
  ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ n : ℕ, ∀ w : ℝ → 𝕜, MemLp w 2 volume →
    eLpNorm ((schemeOp coef h)^[n] w) 2 volume ≤ ENNReal.ofReal C * eLpNorm w 2 volume

/-- Weak derivative on `ℝ`, tested against real compactly supported `C¹` functions. -/
def HasWeakDeriv {𝕜 : Type*} [RCLike 𝕜] (u g : ℝ → 𝕜) : Prop :=
  LocallyIntegrable u volume ∧ LocallyIntegrable g volume ∧
  ∀ φ : ℝ → ℝ, ContDiff ℝ 1 φ → HasCompactSupport φ →
    (∫ x, deriv φ x • u x) = -(∫ x, φ x • g x)

/-- `v ∈ H^k(ℝ)` with weak derivatives `g j = D^j v` (`j ≤ k`), all in `L_2(ℝ)`. -/
def IsSobolevChain {𝕜 : Type*} [RCLike 𝕜] (k : ℕ) (v : ℝ → 𝕜) (g : ℕ → ℝ → 𝕜) : Prop :=
  g 0 = v ∧ (∀ j ≤ k, MemLp (g j) 2 volume) ∧ ∀ j < k, HasWeakDeriv (g j) (g (j + 1))

/-- Exact solution of (12.1) via (12.2): `u(x,t) = v(x + a t)`. -/
def exactSol {𝕜 : Type*} [RCLike 𝕜] (a : ℝ) (v : ℝ → 𝕜) (t : ℝ) : ℝ → 𝕜 :=
  fun x => v (x + a * t)

/-- Theorem 12.2. With `k = λ h`, `t_n = n k`, `U^n = E_k^n v`, `u^n = u(·,t_n)`:
`‖U^n - u^n‖ ≤ C t_n h^r |v|_{r+1}` for `t_n ≥ 0`, where `|v|_{r+1} = ‖D^{r+1} v‖`. -/
theorem thm_12_2 {𝕜 : Type*} [RCLike 𝕜] (a lam : ℝ) (hlam : 0 < lam)
    (coef : ℤ →₀ ℝ) (r : ℕ)
    (hacc : AccurateOfOrder coef a lam r) (hstab : StableL2 𝕜 coef) :
    ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ v : ℝ → 𝕜, ∀ g : ℕ → ℝ → 𝕜, IsSobolevChain (r + 1) v g →
      ∀ n : ℕ,
        eLpNorm (fun x => (schemeOp coef h)^[n] v x - exactSol a v ((n : ℝ) * (lam * h)) x)
            2 volume
          ≤ ENNReal.ofReal (C * ((n : ℝ) * (lam * h)) * h ^ r) * eLpNorm (g (r + 1)) 2 volume := by
  sorry

end PDETextbook.LarssonThomee.Thm12_2