Grönwall bounds from interior derivatives

A curve continuous on a closed interval satisfies the exact Grönwall estimate from any reference point when its derivative satisfies the affine norm bound in the interior. There is no differentiability requirement at either endpoint, and no completeness or sign condition on the rate or error. Continuity transports the interior comparison to both endpoints.

Main results

• TauCeti.norm_le_gronwallBound_of_norm_deriv_le: exact bound from any reference time.
• TauCeti.norm_le_exp_of_affine_deriv_bound: a convenient exponential bound for nonnegative affine coefficients, including initial or terminal reference points.

These estimates apply to spatial coefficient bounds for ancient flows and their pointed limits.

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

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

Grönwall's exact bound from an arbitrary point of a closed interval. Derivatives are required only in the interior; continuity suffices at the endpoints.

theorem TauCeti.norm_le_exp_of_affine_deriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b t₀ C K D : ℝ} (ht₀ : t₀ ∈ Set.Icc a b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hC : 0 ≤ C) (hK : 0 ≤ K) (hinit : ‖f t₀‖ ≤ D) (hbound : ∀ t ∈ Set.Ioo a b, ‖deriv f t‖ ≤ C + K * ‖f t‖) (t : ℝ) : t ∈ Set.Icc a b → ‖f t‖ ≤ max D 1 * Real.exp ((C + K) * |t - t₀|)

Nonnegative affine coefficients give a simple exponential bound from any reference point of a closed interval, assuming differentiability only in the interior.