Signed row sums for supremum-norm comparison

Definition

BianchiIX_Analysis_SignedRowGrowth

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.

Definition code

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

noncomputable section

namespace BianchiIX

open Set Filter
open scoped Topology

variable {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]

/-- The diagonal keeps its sign in the logarithmic bound for the supremum norm. -/
def signedRowSum (A : Matrix ι ι ℝ) (i : ι) : ℝ :=
  A i i + ∑ j ∈ Finset.univ.erase i, |A i j|











end BianchiIX

Source

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

View graph