import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem12_1

/-- The symbol (trigonometric polynomial) `Ẽ(ξ) = ∑_β a_β e^{-iβ·ξ}` appearing in Lemma 12.1.
The finitely many indices `β ∈ ℤ^d` are the elements of `S`, and `βξ = ∑_j β_j ξ_j`.
The coefficient matrices `a_β` are real (the lemma calls them symmetric) and are
viewed as complex matrices because the symbol is complex-valued. -/
def symbol {d N : ℕ} (S : Finset (Fin d → ℤ))
    (a : (Fin d → ℤ) → Matrix (Fin N) (Fin N) ℝ) (ξ : Euclidean d) :
    Matrix (Fin N) (Fin N) ℂ :=
  ∑ β ∈ S,
    Complex.exp (-(Complex.I * (((∑ j : Fin d, (β j : ℝ) * ξ j : ℝ)) : ℂ))) •
      (a β).map (fun r : ℝ => (r : ℂ))

/-- `|M| ≤ 1` for the matrix norm subordinate to the Euclidean vector norm on `ℂ^N`:
`|M v|² ≤ |v|²` for every `v ∈ ℂ^N`. -/
def MatrixNormLeOne {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) : Prop :=
  ∀ v : Fin N → ℂ, (∑ i, ‖(M.mulVec v) i‖ ^ 2) ≤ ∑ i, ‖v i‖ ^ 2

/-- Lemma 12.1 (Larsson–Thomée). If the coefficient matrices `a_β` are symmetric and
positive semidefinite with `∑_β a_β = I`, then `|Ẽ(ξ)| ≤ 1` for all `ξ ∈ ℝ^d`. -/
theorem symbol_norm_le_one {d N : ℕ} (S : Finset (Fin d → ℤ))
    (a : (Fin d → ℤ) → Matrix (Fin N) (Fin N) ℝ)
    (hsymm : ∀ β ∈ S, (a β).IsSymm)
    (hpsd : ∀ β ∈ S, (a β).PosSemidef)
    (hsum : ∑ β ∈ S, a β = 1) :
    ∀ ξ : Euclidean d, MatrixNormLeOne (symbol S a ξ) := by
  sorry

end PDETextbook.LarssonThomee.Lem12_1