A scalar damping term contributes no positive absolute-value slope

Proved

BianchiIX.abs_slope_right_le_of_damping

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

bianchi-ix-era-statisticsdynamical-systems

Suppose $f:\mathbb R\to\mathbb R$ has derivative $df(t)+g$ at $t$ , where $d\leq0$ and $|g|\leq B<R$ . For all $s>t$ sufficiently near $t$ ,

\frac{|f(s)|-|f(t)|}{s-t}<R.

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_slope_right_le_of_damping {f : ℝ → ℝ} {t d g B r : ℝ}
    (hf : HasDerivAt f (d * f t + g) t) (hd : d ≤ 0) (hg : |g| ≤ B) (hr : B < r) :
    ∀ᶠ s in 𝓝[>] t, (s - t)⁻¹ * (|f s| - |f t|) < r := by sorry

Source

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

View graph