A forcing primitive bounds a scalar solution with nonpositive damping

Proved

BianchiIX.abs_le_primitive_of_damping

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

bianchi-ix-era-statisticsdynamical-systems

Let $f,p$ be continuous on $[a,b]$ . Suppose for every $t\in[a,b)$ ,

f'(t)=d(t)f(t)+g(t),\qquad p'(t)=q(t),\qquad d(t)\leq0,\quad |g(t)|\leq q(t).

Then

|f(t)|\leq |f(a)|+p(t)-p(a)\qquad(t\in[a,b]).

Preamble

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

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter
open scoped Topology

Formal statement

theorem BianchiIX.abs_le_primitive_of_damping {f d g p p' : ℝ → ℝ} {a b : ℝ}
    (hf : ContinuousOn f (Icc a b))
    (hdf : ∀ t ∈ Ico a b, HasDerivAt f (d t * f t + g t) t)
    (hp : ContinuousOn p (Icc a b)) (hdp : ∀ t ∈ Ico a b, HasDerivAt p (p' t) t)
    (hd : ∀ t ∈ Ico a b, d t ≤ 0) (hg : ∀ t ∈ Ico a b, |g t| ≤ p' t) :
    ∀ t ∈ Icc a b, |f t| ≤ |f a| + (p t - p a) := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/DampedForcing.lean#L45-L57

View graph