A necessary Fourier condition for maximum-norm stability

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm92

/-- The explicit difference operator of (9.8): `(E_k U)_j = ∑_p a_p U_{j-p}`.
The sum ranges over the finite index set `S`; the source states "the sum is finite".
The coefficients `a_p = a_p(λ)` are taken at the fixed value of `λ = k/h²` for this operator.
The source does not restrict `a_p` or the mesh functions to be real, and its proof of Theorem 9.2
uses the complex mesh function `v_j = e^{ijξ₀} ε`. So coefficients and mesh functions are
complex-valued here. Real coefficients and real data are the special case of real values in `ℂ`. -/
def Ek (S : Finset ℤ) (a : ℤ → ℂ) (U : ℤ → ℂ) : ℤ → ℂ :=
  fun j => ∑ p ∈ S, a p * U (j - p)

/-- A mesh function `v = (v_j)_{j ∈ ℤ}` with finite discrete maximum-norm. -/
def IsBoundedMesh (v : ℤ → ℂ) : Prop :=
  BddAbove (Set.range fun j => ‖v j‖)

/-- The discrete maximum-norm (9.5): `‖v‖_{∞,h} = sup_{j ∈ ℤ} |v_j|`, with `|·|` the complex
modulus. -/
def maxNormH (v : ℤ → ℂ) : ℝ :=
  ⨆ j : ℤ, ‖v j‖

/-- Stability of `E_k` with respect to the discrete maximum-norm, as in (9.6):
`‖E_k^n v‖_{∞,h} ≤ ‖v‖_{∞,h}` for all `n ≥ 0` and all mesh functions `v` with finite
maximum-norm. There is no constant factor; the l_{2,h} notion is defined "analogously to (9.6),
but allowing a constant factor C". -/
def IsMaxNormStable (S : Finset ℤ) (a : ℤ → ℂ) : Prop :=
  ∀ v : ℤ → ℂ, IsBoundedMesh v → ∀ n : ℕ, maxNormH ((Ek S a)^[n] v) ≤ maxNormH v

/-- The trigonometric polynomial (9.9) associated with `E_k`:
`Ẽ(ξ) = ∑_p a_p e^{-i p ξ}`. -/
def symbol (S : Finset ℤ) (a : ℤ → ℂ) (ξ : ℝ) : ℂ :=
  ∑ p ∈ S, a p * Complex.exp (-((p : ℂ) * (ξ : ℂ)) * Complex.I)

/-- Theorem 9.2: a necessary condition for stability of `E_k` in (9.8) with respect to the
discrete maximum-norm (9.5) is `|Ẽ(ξ)| ≤ 1` for all `ξ ∈ ℝ` (9.10). -/
theorem thm_9_2 (S : Finset ℤ) (a : ℤ → ℂ) (hstab : IsMaxNormStable S a) :
    ∀ ξ : ℝ, ‖symbol S a ξ‖ ≤ 1 := by
  sorry

end PDETextbook.LarssonThomee.Thm92