AcceptedLemma · Statement with omitted proof

Contractive symbols from positive matrix weights

A finite matrix-valued stencil has a contractive Fourier symbol when its weights are positive semidefinite and sum to the identity.

Larsson & Thomée ↗
Lemma 12.1 · printed p. 194

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

A finite matrix-valued stencil has a contractive Fourier symbol when its weights are positive semidefinite and sum to the identity.

\sum_\beta a_\beta=I,\quad a_\beta\succeq0\quad\Longrightarrow\quad \Bigl\|\sum_\beta a_\beta e^{-i\beta\cdot\xi}\Bigr\|_2\le1.

Assumptions & context

Symmetric positive-semidefinite real matrix coefficients on a finite multidimensional stencil, with identity total weight.

Source

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

Lemma 12.1 · printed p. 194

02 / LEAN REPRESENTATION

Formal statement

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

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

Complete Lean file and local definitions

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

How to read the formalization

The symbol acts on complex vectors; the norm condition is an operator bound, not an entrywise bound.

← Back to all statements