Grönwall bounds in both time directions

Mathlib's gronwallBound controls a curve forward from the left endpoint. Here the initial point may be anywhere in a closed interval: an affine time change gives the exact same bound with elapsed time |t - t₀|. The derivative may be taken within the closed interval, so no extension beyond its endpoints is required. There are no completeness or sign assumptions.

Main results

• TauCeti.norm_le_gronwallBound_of_norm_derivWithin_le: a norm bound from any reference time.
• TauCeti.norm_sub_le_gronwallBound_of_linearODE: comparison of two linear trajectories.
• TauCeti.gronwallBound_zero_le_mul_exp: an explicit zero-initial-value estimate.

Formalization references: https://github.com/frenzymath/lean-eval-submissions and https://github.com/frenzymath/PoincareConjecture.

theorem TauCeti.norm_le_gronwallBound_of_norm_derivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → E} {a b t₀ δ K ε : ℝ} (ht₀ : t₀ ∈ Set.Icc a b) (hf' : ∀ t ∈ Set.Icc a b, HasDerivWithinAt f (f' t) (Set.Icc a b) t) (hinit : ‖f t₀‖ ≤ δ) (hbound : ∀ t ∈ Set.Icc a b, ‖f' t‖ ≤ K * ‖f t‖ + ε) (t : ℝ) : t ∈ Set.Icc a b → ‖f t‖ ≤ gronwallBound δ K ε |t - t₀|

A derivative norm bound on [a,b] controls the curve from any initial point t₀ ∈ [a,b] in both time directions. No sign assumptions on the three constants are needed for the exact Grönwall bound.

theorem TauCeti.norm_sub_le_gronwallBound_of_linearODE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A₁ A₂ : ℝ → E →L[ℝ] E} {Z₁ Z₂ : ℝ → E} {a b t₀ K η : ℝ} (ht₀ : t₀ ∈ Set.Icc a b) (hZ₁ : ∀ s ∈ Set.Icc a b, HasDerivWithinAt Z₁ ((A₁ s) (Z₁ s)) (Set.Icc a b) s) (hZ₂ : ∀ s ∈ Set.Icc a b, HasDerivWithinAt Z₂ ((A₂ s) (Z₂ s)) (Set.Icc a b) s) (hA₁ : ∀ s ∈ Set.Icc a b, ‖A₁ s‖ ≤ K) (hdiff : ∀ s ∈ Set.Icc a b, ‖(A₂ s - A₁ s) (Z₂ s)‖ ≤ η) (t : ℝ) : t ∈ Set.Icc a b → ‖Z₁ t - Z₂ t‖ ≤ gronwallBound ‖Z₁ t₀ - Z₂ t₀‖ K η |t - t₀|

Two actual linear trajectories on [a,b] satisfy a two-sided Grönwall comparison from any initial time t₀ in that interval. The operator bound is on A₁, and the forcing error is (A₂ - A₁) Z₂. No completeness or sign hypotheses are needed for this exact bound.

theorem TauCeti.gronwallBound_zero_le_mul_exp {K ε x : ℝ} (hK : 0 ≤ K) (hε : 0 ≤ ε) : gronwallBound 0 K ε x ≤ ε * x * Real.exp (K * x)

For nonnegative growth rate and error, the zero-initial-value Grönwall bound is at most ε * x * exp (K*x). This also includes growth rate zero.