An Euler-step supremum-norm estimate from signed row sums

Proved

BianchiIX.norm_euler_le_of_signedRowSum

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For a finite index type $\iota$ , a real matrix $A=(A_{ij})$ , and $i\in\iota$ , define its signed row sum by

\sigma_i(A)=A_{ii}+\sum_{j\ne i}|A_{ij}|.

Vectors in $\mathbb R^\iota$ carry the supremum norm. Assume $\iota$ is nonempty. Let $h\geq0$ , $\sigma_i(A)\leq\rho$ , and $1+hA_{ii}\geq0$ for every $i$ . Then for every $x\in\mathbb R^\iota$ ,

\|x+hAx\|_\infty\leq(1+h\rho)\|x\|_\infty.

Preamble

import Definitions.Def_BianchiIX_Analysis_SignedRowGrowth
import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Data.Matrix.Mul
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.FunProp

noncomputable section
open BianchiIX
open Set Filter
open scoped Topology
variable {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]

Formal statement

theorem BianchiIX.norm_euler_le_of_signedRowSum {A : Matrix ι ι ℝ} {ρ h : ℝ}
    (hA : ∀ i, signedRowSum A i ≤ ρ) (hh : 0 ≤ h)
    (hdiag : ∀ i, 0 ≤ 1 + h * A i i) (x : ι → ℝ) :
    ‖x + h • A.mulVec x‖ ≤ (1 + h * ρ) * ‖x‖ := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/SignedRowGrowth.lean#L19-L50

View graph