Constant forcing contributes only its elapsed-time budget

Proved

BianchiIX.norm_le_exp_of_norm_deriv_clock_forcing

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

bianchi-ix-era-statisticsdynamical-systems

Let $E$ be a real normed space, let $f:\mathbb R\to E$ and $z:\mathbb R\to\mathbb R$ have derivatives at every point of $[a,b]$ , and let $\varepsilon\geq0$ . Suppose $z(t)\geq z(a)$ and

\|f'(t)\|\leq z'(t)\|f(t)\|+\varepsilon\quad(t\in[a,b]).

Then throughout $[a,b]$ ,

\|f(t)\|\leq(\|f(a)\|+\varepsilon(t-a))\exp(z(t)-z(a)).

Preamble

import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Tactic.FunProp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Formal statement

theorem BianchiIX.norm_le_exp_of_norm_deriv_clock_forcing {f f' : ℝ → E} {z z' : ℝ → ℝ} {a b ε : ℝ}
    (hf : ∀ t ∈ Icc a b, HasDerivAt f (f' t) t)
    (hz : ∀ t ∈ Icc a b, HasDerivAt z (z' t) t)
    (hε : 0 ≤ ε) (hclock : ∀ t ∈ Icc a b, z a ≤ z t)
    (hbound : ∀ t ∈ Icc a b, ‖f' t‖ ≤ z' t * ‖f t‖ + ε) :
    ∀ t ∈ Icc a b, ‖f t‖ ≤ (‖f a‖ + ε * (t - a)) * Real.exp (z t - z a) := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/NormClockForcing.lean#L11-L49

View graph