Exponential comparison with a primitive of the signed row bound

Proved

BianchiIX.norm_le_exp_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 $f$ and $z$ be continuous on $[a,b]$ . For every $t\in[a,b)$ suppose

f'(t)=A(t)f(t),\qquad z'(t)=q(t),\qquad \sigma_i(A(t))\leq q(t)\quad(i\in\iota).

Then

\|f(t)\|_\infty\leq\|f(a)\|_\infty e^{z(t)-z(a)} \quad(t\in[a,b]).

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_le_exp_of_signedRowSum {f : ℝ → (ι → ℝ)}
    {A : ℝ → Matrix ι ι ℝ} {z z' : ℝ → ℝ} {a b : ℝ}
    (hf : ContinuousOn f (Icc a b))
    (hderiv : ∀ t ∈ Ico a b, HasDerivAt f ((A t).mulVec (f t)) t)
    (hz : ContinuousOn z (Icc a b))
    (hzderiv : ∀ t ∈ Ico a b, HasDerivAt z (z' t) t)
    (hA : ∀ t ∈ Ico a b, ∀ i, signedRowSum (A t) i ≤ z' t) :
    ∀ t ∈ Icc a b, ‖f t‖ ≤ ‖f a‖ * Real.exp (z t - z a) := by sorry

Source

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

View graph